mbfi1fseqlem3 - Metamath Proof Explorer

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

Theorem mbfi1fseqlem3 22416

Description: Lemma for mbfi1fseq 22420. (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		rge0ssre 11682	. . . . . . . . . . . . . . . . . . 19
2		mbfi1fseq.2	. . . . . . . . . . . . . . . . . . . 20
3		simpr 459	. . . . . . . . . . . . . . . . . . . 20 $/\$
4		ffvelrn 6007	. . . . . . . . . . . . . . . . . . . 20 $/\$
5	2, 3, 4	syl2an 475	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
6	1, 5	sseldi 3440	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
7		2nn 10734	. . . . . . . . . . . . . . . . . . . . 21
8		nnnn0 10843	. . . . . . . . . . . . . . . . . . . . 21
9		nnexpcl 12223	. . . . . . . . . . . . . . . . . . . . 21 $/\$
10	7, 8, 9	sylancr 661	. . . . . . . . . . . . . . . . . . . 20
11	10	ad2antrl 726	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
12	11	nnred 10591	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
13	6, 12	remulcld 9654	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
14		reflcl 11970	. . . . . . . . . . . . . . . . 17
15	13, 14	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
16	15, 11	nndivred 10625	. . . . . . . . . . . . . . 15 $/\$ $/\$
17	16	ralrimivva 2825	. . . . . . . . . . . . . 14
18		mbfi1fseq.3	. . . . . . . . . . . . . . 15
19	18	fmpt2 6851	. . . . . . . . . . . . . 14
20	17, 19	sylib 196	. . . . . . . . . . . . 13
21		fovrn 6426	. . . . . . . . . . . . 13 $/\$ $/\$
22	20, 21	syl3an1 1263	. . . . . . . . . . . 12 $/\$ $/\$
23	22	3expa 1197	. . . . . . . . . . 11 $/\$ $/\$
24		nnre 10583	. . . . . . . . . . . 12
25	24	ad2antlr 725	. . . . . . . . . . 11 $/\$ $/\$
26		nnnn0 10843	. . . . . . . . . . . . . 14
27		nnexpcl 12223	. . . . . . . . . . . . . 14 $/\$
28	7, 26, 27	sylancr 661	. . . . . . . . . . . . 13
29	28	ad2antlr 725	. . . . . . . . . . . 12 $/\$ $/\$
30		nnre 10583	. . . . . . . . . . . . 13
31		nngt0 10605	. . . . . . . . . . . . 13
32	30, 31	jca 530	. . . . . . . . . . . 12 $/\$
33	29, 32	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
34		lemul1 10435	. . . . . . . . . . 11 $/\$ $/\$ $/\$
35	23, 25, 33, 34	syl3anc 1230	. . . . . . . . . 10 $/\$ $/\$
36	35	biimpa 482	. . . . . . . . 9 $/\$ $/\$ $/\$
37		simplr 754	. . . . . . . . . . . . . . . 16 $/\$ $/\$
38	37	adantr 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
39		simplr 754	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
40		simpr 459	. . . . . . . . . . . . . . . . . . . 20 $/\$
41	40	fveq2d 5853	. . . . . . . . . . . . . . . . . . 19 $/\$
42		simpl 455	. . . . . . . . . . . . . . . . . . . 20 $/\$
43	42	oveq2d 6294	. . . . . . . . . . . . . . . . . . 19 $/\$
44	41, 43	oveq12d 6296	. . . . . . . . . . . . . . . . . 18 $/\$
45	44	fveq2d 5853	. . . . . . . . . . . . . . . . 17 $/\$
46	45, 43	oveq12d 6296	. . . . . . . . . . . . . . . 16 $/\$
47		ovex 6306	. . . . . . . . . . . . . . . 16
48	46, 18, 47	ovmpt2a 6414	. . . . . . . . . . . . . . 15 $/\$
49	38, 39, 48	syl2anc 659	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
50	49	oveq1d 6293	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
51	2	adantr 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$
52	51	ffvelrnda 6009	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
53		elrege0 11681	. . . . . . . . . . . . . . . . . . . 20 $/\$
54	52, 53	sylib 196	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
55	54	simpld 457	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
56	29	nnred 10591	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
57	55, 56	remulcld 9654	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
58	29	nnnn0d 10893	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
59	58	nn0ge0d 10896	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
60		mulge0 10111	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
61	54, 56, 59, 60	syl12anc 1228	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
62		flge0nn0 11992	. . . . . . . . . . . . . . . . 17 $/\$
63	57, 61, 62	syl2anc 659	. . . . . . . . . . . . . . . 16 $/\$ $/\$
64	63	adantr 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
65	64	nn0cnd 10895	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
66	29	adantr 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
67	66	nncnd 10592	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
68	66	nnne0d 10621	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
69	65, 67, 68	divcan1d 10362	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
70	50, 69	eqtrd 2443	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
71	70, 64	eqeltrd 2490	. . . . . . . . . . 11 $/\$ $/\$ $/\$
72		nn0uz 11161	. . . . . . . . . . 11
73	71, 72	syl6eleq 2500	. . . . . . . . . 10 $/\$ $/\$ $/\$
74		nnmulcl 10599	. . . . . . . . . . . . . 14 $/\$
75	28, 74	mpdan 666	. . . . . . . . . . . . 13
76	75	ad2antlr 725	. . . . . . . . . . . 12 $/\$ $/\$
77	76	adantr 463	. . . . . . . . . . 11 $/\$ $/\$ $/\$
78	77	nnzd 11007	. . . . . . . . . 10 $/\$ $/\$ $/\$
79		elfz5 11734	. . . . . . . . . 10 $/\$
80	73, 78, 79	syl2anc 659	. . . . . . . . 9 $/\$ $/\$ $/\$
81	36, 80	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$
82		oveq1 6285	. . . . . . . . 9
83		eqid 2402	. . . . . . . . 9
84		ovex 6306	. . . . . . . . 9
85	82, 83, 84	fvmpt 5932	. . . . . . . 8
86	81, 85	syl 17	. . . . . . 7 $/\$ $/\$ $/\$
87	23	adantr 463	. . . . . . . . 9 $/\$ $/\$ $/\$
88	87	recnd 9652	. . . . . . . 8 $/\$ $/\$ $/\$
89	88, 67, 68	divcan4d 10367	. . . . . . 7 $/\$ $/\$ $/\$
90	86, 89	eqtrd 2443	. . . . . 6 $/\$ $/\$ $/\$
91		elfznn0 11826	. . . . . . . . . . . . 13
92	91	nn0red 10894	. . . . . . . . . . . 12
93	28	adantl 464	. . . . . . . . . . . 12 $/\$
94		nndivre 10612	. . . . . . . . . . . 12 $/\$
95	92, 93, 94	syl2anr 476	. . . . . . . . . . 11 $/\$ $/\$
96	95, 83	fmptd 6033	. . . . . . . . . 10 $/\$
97		ffn 5714	. . . . . . . . . 10
98	96, 97	syl 17	. . . . . . . . 9 $/\$
99	98	adantr 463	. . . . . . . 8 $/\$ $/\$
100	99	adantr 463	. . . . . . 7 $/\$ $/\$ $/\$
101		fnfvelrn 6006	. . . . . . 7 $/\$
102	100, 81, 101	syl2anc 659	. . . . . 6 $/\$ $/\$ $/\$
103	90, 102	eqeltrrd 2491	. . . . 5 $/\$ $/\$ $/\$
104	76	nnnn0d 10893	. . . . . . . . . . 11 $/\$ $/\$
105	104, 72	syl6eleq 2500	. . . . . . . . . 10 $/\$ $/\$
106		eluzfz2 11748	. . . . . . . . . 10
107	105, 106	syl 17	. . . . . . . . 9 $/\$ $/\$
108		oveq1 6285	. . . . . . . . . 10
109		ovex 6306	. . . . . . . . . 10
110	108, 83, 109	fvmpt 5932	. . . . . . . . 9
111	107, 110	syl 17	. . . . . . . 8 $/\$ $/\$
112	25	recnd 9652	. . . . . . . . 9 $/\$ $/\$
113	29	nncnd 10592	. . . . . . . . 9 $/\$ $/\$
114	29	nnne0d 10621	. . . . . . . . 9 $/\$ $/\$
115	112, 113, 114	divcan4d 10367	. . . . . . . 8 $/\$ $/\$
116	111, 115	eqtrd 2443	. . . . . . 7 $/\$ $/\$
117		fnfvelrn 6006	. . . . . . . 8 $/\$
118	99, 107, 117	syl2anc 659	. . . . . . 7 $/\$ $/\$
119	116, 118	eqeltrrd 2491	. . . . . 6 $/\$ $/\$
120	119	adantr 463	. . . . 5 $/\$ $/\$ $/\$
121	103, 120	ifclda 3917	. . . 4 $/\$ $/\$
122		eluzfz1 11747	. . . . . . . 8
123	105, 122	syl 17	. . . . . . 7 $/\$ $/\$
124		oveq1 6285	. . . . . . . 8
125		ovex 6306	. . . . . . . 8
126	124, 83, 125	fvmpt 5932	. . . . . . 7
127	123, 126	syl 17	. . . . . 6 $/\$ $/\$
128		nncn 10584	. . . . . . . 8
129		nnne0 10609	. . . . . . . 8
130	128, 129	div0d 10360	. . . . . . 7
131	29, 130	syl 17	. . . . . 6 $/\$ $/\$
132	127, 131	eqtrd 2443	. . . . 5 $/\$ $/\$
133		fnfvelrn 6006	. . . . . 6 $/\$
134	99, 123, 133	syl2anc 659	. . . . 5 $/\$ $/\$
135	132, 134	eqeltrrd 2491	. . . 4 $/\$ $/\$
136	121, 135	ifcld 3928	. . 3 $/\$ $/\$
137		eqid 2402	. . 3
138	136, 137	fmptd 6033	. 2 $/\$
139		mbfi1fseq.1	. . . . 5 MblFn
140		mbfi1fseq.4	. . . . 5
141	139, 2, 18, 140	mbfi1fseqlem2 22415	. . . 4
142	141	adantl 464	. . 3 $/\$
143	142	feq1d 5700	. 2 $/\$
144	138, 143	mpbird 232	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367

wceq 1405

wcel 1842

wral 2754

cif 3885 class class class wbr 4395

cmpt 4453

cxp 4821

crn 4824

wfn 5564

wf 5565

cfv 5569 (class class class)co 6278

cmpt2 6280

cr 9521

cc0 9522

cmul 9527

cpnf 9655

clt 9658

cle 9659

cneg 9842

cdiv 10247

cn 10576

c2 10626

cn0 10836

cz 10905

cuz 11127

cico 11584

cicc 11585

cfz 11726

cfl 11964

cexp 12210 MblFncmbf 22315

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4507 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574 ax-cnex 9578 ax-resscn 9579 ax-1cn 9580 ax-icn 9581 ax-addcl 9582 ax-addrcl 9583 ax-mulcl 9584 ax-mulrcl 9585 ax-mulcom 9586 ax-addass 9587 ax-mulass 9588 ax-distr 9589 ax-i2m1 9590 ax-1ne0 9591 ax-1rid 9592 ax-rnegex 9593 ax-rrecex 9594 ax-cnre 9595 ax-pre-lttri 9596 ax-pre-lttrn 9597 ax-pre-ltadd 9598 ax-pre-mulgt0 9599 ax-pre-sup 9600

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2759 df-rex 2760 df-reu 2761 df-rmo 2762 df-rab 2763 df-v 3061 df-sbc 3278 df-csb 3374 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-pss 3430 df-nul 3739 df-if 3886 df-pw 3957 df-sn 3973 df-pr 3975 df-tp 3977 df-op 3979 df-uni 4192 df-iun 4273 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4490 df-eprel 4734 df-id 4738 df-po 4744 df-so 4745 df-fr 4782 df-we 4784 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-pred 5367 df-ord 5413 df-on 5414 df-lim 5415 df-suc 5416 df-iota 5533 df-fun 5571 df-fn 5572 df-f 5573 df-f1 5574 df-fo 5575 df-f1o 5576 df-fv 5577 df-riota 6240 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-om 6684 df-1st 6784 df-2nd 6785 df-wrecs 7013 df-recs 7075 df-rdg 7113 df-er 7348 df-en 7555 df-dom 7556 df-sdom 7557 df-sup 7935 df-pnf 9660 df-mnf 9661 df-xr 9662 df-ltxr 9663 df-le 9664 df-sub 9843 df-neg 9844 df-div 10248 df-nn 10577 df-2 10635 df-n0 10837 df-z 10906 df-uz 11128 df-ico 11588 df-fz 11727 df-fl 11966 df-seq 12152 df-exp 12211

This theorem is referenced by: mbfi1fseqlem4 22417

W3C validator