mbfi1fseqlem3 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mbfi1fseqlem3		Structured version Unicode version

Theorem mbfi1fseqlem3 21323

Description: Lemma for mbfi1fseq 21327. (Contributed by Mario Carneiro, 16-Aug-2014.)

**Hypotheses**
Ref	Expression
mbfi1fseq.1	MblFn
mbfi1fseq.2
mbfi1fseq.3
mbfi1fseq.4

**Assertion**
Ref	Expression
mbfi1fseqlem3	$/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

**Proof of Theorem mbfi1fseqlem3**
Step	Hyp	Ref	Expression
1		0re 9492	. . . . . . . . . . . . . . . . . . . 20
2		pnfxr 11198	. . . . . . . . . . . . . . . . . . . 20
3		icossre 11482	. . . . . . . . . . . . . . . . . . . 20 $/\$
4	1, 2, 3	mp2an 672	. . . . . . . . . . . . . . . . . . 19
5		mbfi1fseq.2	. . . . . . . . . . . . . . . . . . . 20
6		simpr 461	. . . . . . . . . . . . . . . . . . . 20 $/\$
7		ffvelrn 5945	. . . . . . . . . . . . . . . . . . . 20 $/\$
8	5, 6, 7	syl2an 477	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
9	4, 8	sseldi 3457	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
10		2nn 10585	. . . . . . . . . . . . . . . . . . . . 21
11		nnnn0 10692	. . . . . . . . . . . . . . . . . . . . 21
12		nnexpcl 11990	. . . . . . . . . . . . . . . . . . . . 21 $/\$
13	10, 11, 12	sylancr 663	. . . . . . . . . . . . . . . . . . . 20
14	13	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
15	14	nnred 10443	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
16	9, 15	remulcld 9520	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
17		reflcl 11758	. . . . . . . . . . . . . . . . 17
18	16, 17	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
19	18, 14	nndivred 10476	. . . . . . . . . . . . . . 15 $/\$ $/\$
20	19	ralrimivva 2908	. . . . . . . . . . . . . 14
21		mbfi1fseq.3	. . . . . . . . . . . . . . 15
22	21	fmpt2 6746	. . . . . . . . . . . . . 14
23	20, 22	sylib 196	. . . . . . . . . . . . 13
24		fovrn 6338	. . . . . . . . . . . . 13 $/\$ $/\$
25	23, 24	syl3an1 1252	. . . . . . . . . . . 12 $/\$ $/\$
26	25	3expa 1188	. . . . . . . . . . 11 $/\$ $/\$
27		nnre 10435	. . . . . . . . . . . 12
28	27	ad2antlr 726	. . . . . . . . . . 11 $/\$ $/\$
29		nnnn0 10692	. . . . . . . . . . . . . 14
30		nnexpcl 11990	. . . . . . . . . . . . . 14 $/\$
31	10, 29, 30	sylancr 663	. . . . . . . . . . . . 13
32	31	ad2antlr 726	. . . . . . . . . . . 12 $/\$ $/\$
33		nnre 10435	. . . . . . . . . . . . 13
34		nngt0 10457	. . . . . . . . . . . . 13
35	33, 34	jca 532	. . . . . . . . . . . 12 $/\$
36	32, 35	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$
37		lemul1 10287	. . . . . . . . . . 11 $/\$ $/\$ $/\$
38	26, 28, 36, 37	syl3anc 1219	. . . . . . . . . 10 $/\$ $/\$
39	38	biimpa 484	. . . . . . . . 9 $/\$ $/\$ $/\$
40		simplr 754	. . . . . . . . . . . . . . . 16 $/\$ $/\$
41	40	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
42		simplr 754	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
43		simpr 461	. . . . . . . . . . . . . . . . . . . 20 $/\$
44	43	fveq2d 5798	. . . . . . . . . . . . . . . . . . 19 $/\$
45		simpl 457	. . . . . . . . . . . . . . . . . . . 20 $/\$
46	45	oveq2d 6211	. . . . . . . . . . . . . . . . . . 19 $/\$
47	44, 46	oveq12d 6213	. . . . . . . . . . . . . . . . . 18 $/\$
48	47	fveq2d 5798	. . . . . . . . . . . . . . . . 17 $/\$
49	48, 46	oveq12d 6213	. . . . . . . . . . . . . . . 16 $/\$
50		ovex 6220	. . . . . . . . . . . . . . . 16
51	49, 21, 50	ovmpt2a 6326	. . . . . . . . . . . . . . 15 $/\$
52	41, 42, 51	syl2anc 661	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
53	52	oveq1d 6210	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
54	5	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$
55	54	ffvelrnda 5947	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
56		elrege0 11504	. . . . . . . . . . . . . . . . . . . 20 $/\$
57	55, 56	sylib 196	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
58	57	simpld 459	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
59	32	nnred 10443	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
60	58, 59	remulcld 9520	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
61	32	nnnn0d 10742	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
62	61	nn0ge0d 10745	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
63		mulge0 9963	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
64	57, 59, 62, 63	syl12anc 1217	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
65		flge0nn0 11778	. . . . . . . . . . . . . . . . 17 $/\$
66	60, 64, 65	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ $/\$
67	66	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
68	67	nn0cnd 10744	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
69	32	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
70	69	nncnd 10444	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
71	69	nnne0d 10472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
72	68, 70, 71	divcan1d 10214	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
73	53, 72	eqtrd 2493	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
74	73, 67	eqeltrd 2540	. . . . . . . . . . 11 $/\$ $/\$ $/\$
75		nn0uz 11001	. . . . . . . . . . 11
76	74, 75	syl6eleq 2550	. . . . . . . . . 10 $/\$ $/\$ $/\$
77		nnmulcl 10451	. . . . . . . . . . . . . 14 $/\$
78	31, 77	mpdan 668	. . . . . . . . . . . . 13
79	78	ad2antlr 726	. . . . . . . . . . . 12 $/\$ $/\$
80	79	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$
81	80	nnzd 10852	. . . . . . . . . 10 $/\$ $/\$ $/\$
82		elfz5 11557	. . . . . . . . . 10 $/\$
83	76, 81, 82	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
84	39, 83	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$
85		oveq1 6202	. . . . . . . . 9
86		eqid 2452	. . . . . . . . 9
87		ovex 6220	. . . . . . . . 9
88	85, 86, 87	fvmpt 5878	. . . . . . . 8
89	84, 88	syl 16	. . . . . . 7 $/\$ $/\$ $/\$
90	26	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$
91	90	recnd 9518	. . . . . . . 8 $/\$ $/\$ $/\$
92	91, 70, 71	divcan4d 10219	. . . . . . 7 $/\$ $/\$ $/\$
93	89, 92	eqtrd 2493	. . . . . 6 $/\$ $/\$ $/\$
94		elfznn0 11593	. . . . . . . . . . . . 13
95	94	nn0red 10743	. . . . . . . . . . . 12
96	31	adantl 466	. . . . . . . . . . . 12 $/\$
97		nndivre 10463	. . . . . . . . . . . 12 $/\$
98	95, 96, 97	syl2anr 478	. . . . . . . . . . 11 $/\$ $/\$
99	98, 86	fmptd 5971	. . . . . . . . . 10 $/\$
100		ffn 5662	. . . . . . . . . 10
101	99, 100	syl 16	. . . . . . . . 9 $/\$
102	101	adantr 465	. . . . . . . 8 $/\$ $/\$
103	102	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$
104		fnfvelrn 5944	. . . . . . 7 $/\$
105	103, 84, 104	syl2anc 661	. . . . . 6 $/\$ $/\$ $/\$
106	93, 105	eqeltrrd 2541	. . . . 5 $/\$ $/\$ $/\$
107	79	nnnn0d 10742	. . . . . . . . . . 11 $/\$ $/\$
108	107, 75	syl6eleq 2550	. . . . . . . . . 10 $/\$ $/\$
109		eluzfz2 11571	. . . . . . . . . 10
110	108, 109	syl 16	. . . . . . . . 9 $/\$ $/\$
111		oveq1 6202	. . . . . . . . . 10
112		ovex 6220	. . . . . . . . . 10
113	111, 86, 112	fvmpt 5878	. . . . . . . . 9
114	110, 113	syl 16	. . . . . . . 8 $/\$ $/\$
115	28	recnd 9518	. . . . . . . . 9 $/\$ $/\$
116	32	nncnd 10444	. . . . . . . . 9 $/\$ $/\$
117	32	nnne0d 10472	. . . . . . . . 9 $/\$ $/\$
118	115, 116, 117	divcan4d 10219	. . . . . . . 8 $/\$ $/\$
119	114, 118	eqtrd 2493	. . . . . . 7 $/\$ $/\$
120		fnfvelrn 5944	. . . . . . . 8 $/\$
121	102, 110, 120	syl2anc 661	. . . . . . 7 $/\$ $/\$
122	119, 121	eqeltrrd 2541	. . . . . 6 $/\$ $/\$
123	122	adantr 465	. . . . 5 $/\$ $/\$ $/\$
124	106, 123	ifclda 3924	. . . 4 $/\$ $/\$
125		eluzfz1 11570	. . . . . . . 8
126	108, 125	syl 16	. . . . . . 7 $/\$ $/\$
127		oveq1 6202	. . . . . . . 8
128		ovex 6220	. . . . . . . 8
129	127, 86, 128	fvmpt 5878	. . . . . . 7
130	126, 129	syl 16	. . . . . 6 $/\$ $/\$
131		nncn 10436	. . . . . . . 8
132		nnne0 10460	. . . . . . . 8
133	131, 132	div0d 10212	. . . . . . 7
134	32, 133	syl 16	. . . . . 6 $/\$ $/\$
135	130, 134	eqtrd 2493	. . . . 5 $/\$ $/\$
136		fnfvelrn 5944	. . . . . 6 $/\$
137	102, 126, 136	syl2anc 661	. . . . 5 $/\$ $/\$
138	135, 137	eqeltrrd 2541	. . . 4 $/\$ $/\$
139		ifcl 3934	. . . 4 $/\$
140	124, 138, 139	syl2anc 661	. . 3 $/\$ $/\$
141		eqid 2452	. . 3
142	140, 141	fmptd 5971	. 2 $/\$
143		mbfi1fseq.1	. . . . 5 MblFn
144		mbfi1fseq.4	. . . . 5
145	143, 5, 21, 144	mbfi1fseqlem2 21322	. . . 4
146	145	adantl 466	. . 3 $/\$
147	146	feq1d 5649	. 2 $/\$
148	142, 147	mpbird 232	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369

wceq 1370

wcel 1758

wral 2796

wss 3431

cif 3894 class class class wbr 4395

cmpt 4453

cxp 4941

crn 4944

wfn 5516

wf 5517

cfv 5521 (class class class)co 6195

cmpt2 6197

cr 9387

cc0 9388

cmul 9393

cpnf 9521

cxr 9523

clt 9524

cle 9525

cneg 9702

cdiv 10099

cn 10428

c2 10477

cn0 10685

cz 10752

cuz 10967

cico 11408

cicc 11409

cfz 11549

cfl 11752

cexp 11977 MblFncmbf 21222

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4573 ax-pr 4634 ax-un 6477 ax-cnex 9444 ax-resscn 9445 ax-1cn 9446 ax-icn 9447 ax-addcl 9448 ax-addrcl 9449 ax-mulcl 9450 ax-mulrcl 9451 ax-mulcom 9452 ax-addass 9453 ax-mulass 9454 ax-distr 9455 ax-i2m1 9456 ax-1ne0 9457 ax-1rid 9458 ax-rnegex 9459 ax-rrecex 9460 ax-cnre 9461 ax-pre-lttri 9462 ax-pre-lttrn 9463 ax-pre-ltadd 9464 ax-pre-mulgt0 9465 ax-pre-sup 9466

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2265 df-mo 2266 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-ne 2647 df-nel 2648 df-ral 2801 df-rex 2802 df-reu 2803 df-rmo 2804 df-rab 2805 df-v 3074 df-sbc 3289 df-csb 3391 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-pss 3447 df-nul 3741 df-if 3895 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4195 df-iun 4276 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4489 df-eprel 4735 df-id 4739 df-po 4744 df-so 4745 df-fr 4782 df-we 4784 df-ord 4825 df-on 4826 df-lim 4827 df-suc 4828 df-xp 4949 df-rel 4950 df-cnv 4951 df-co 4952 df-dm 4953 df-rn 4954 df-res 4955 df-ima 4956 df-iota 5484 df-fun 5523 df-fn 5524 df-f 5525 df-f1 5526 df-fo 5527 df-f1o 5528 df-fv 5529 df-riota 6156 df-ov 6198 df-oprab 6199 df-mpt2 6200 df-om 6582 df-1st 6682 df-2nd 6683 df-recs 6937 df-rdg 6971 df-er 7206 df-en 7416 df-dom 7417 df-sdom 7418 df-sup 7797 df-pnf 9526 df-mnf 9527 df-xr 9528 df-ltxr 9529 df-le 9530 df-sub 9703 df-neg 9704 df-div 10100 df-nn 10429 df-2 10486 df-n0 10686 df-z 10753 df-uz 10968 df-ico 11412 df-fz 11550 df-fl 11754 df-seq 11919 df-exp 11978

This theorem is referenced by: mbfi1fseqlem4 21324

W3C validator