mbfi1fseqlem3 - Metamath Proof Explorer

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

Theorem mbfi1fseqlem3 19562

Description: Lemma for mbfi1fseq 19566. (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 9047	. . . . . . . . . . . . . . . . . . . 20
2		pnfxr 10669	. . . . . . . . . . . . . . . . . . . 20
3		icossre 10947	. . . . . . . . . . . . . . . . . . . 20 $/\$
4	1, 2, 3	mp2an 654	. . . . . . . . . . . . . . . . . . 19
5		mbfi1fseq.2	. . . . . . . . . . . . . . . . . . . 20
6		simpr 448	. . . . . . . . . . . . . . . . . . . 20 $/\$
7		ffvelrn 5827	. . . . . . . . . . . . . . . . . . . 20 $/\$
8	5, 6, 7	syl2an 464	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
9	4, 8	sseldi 3306	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
10		2nn 10089	. . . . . . . . . . . . . . . . . . . . 21
11		nnnn0 10184	. . . . . . . . . . . . . . . . . . . . 21
12		nnexpcl 11349	. . . . . . . . . . . . . . . . . . . . 21 $/\$
13	10, 11, 12	sylancr 645	. . . . . . . . . . . . . . . . . . . 20
14	13	ad2antrl 709	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
15	14	nnred 9971	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
16	9, 15	remulcld 9072	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
17		reflcl 11160	. . . . . . . . . . . . . . . . 17
18	16, 17	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
19	18, 14	nndivred 10004	. . . . . . . . . . . . . . 15 $/\$ $/\$
20	19	ralrimivva 2758	. . . . . . . . . . . . . 14
21		mbfi1fseq.3	. . . . . . . . . . . . . . 15
22	21	fmpt2 6377	. . . . . . . . . . . . . 14
23	20, 22	sylib 189	. . . . . . . . . . . . 13
24		fovrn 6175	. . . . . . . . . . . . 13 $/\$ $/\$
25	23, 24	syl3an1 1217	. . . . . . . . . . . 12 $/\$ $/\$
26	25	3expa 1153	. . . . . . . . . . 11 $/\$ $/\$
27		nnre 9963	. . . . . . . . . . . 12
28	27	ad2antlr 708	. . . . . . . . . . 11 $/\$ $/\$
29		nnnn0 10184	. . . . . . . . . . . . . 14
30		nnexpcl 11349	. . . . . . . . . . . . . 14 $/\$
31	10, 29, 30	sylancr 645	. . . . . . . . . . . . 13
32	31	ad2antlr 708	. . . . . . . . . . . 12 $/\$ $/\$
33		nnre 9963	. . . . . . . . . . . . 13
34		nngt0 9985	. . . . . . . . . . . . 13
35	33, 34	jca 519	. . . . . . . . . . . 12 $/\$
36	32, 35	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$
37		lemul1 9818	. . . . . . . . . . 11 $/\$ $/\$ $/\$
38	26, 28, 36, 37	syl3anc 1184	. . . . . . . . . 10 $/\$ $/\$
39	38	biimpa 471	. . . . . . . . 9 $/\$ $/\$ $/\$
40		simplr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$
41	40	adantr 452	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
42		simplr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
43		simpr 448	. . . . . . . . . . . . . . . . . . . 20 $/\$
44	43	fveq2d 5691	. . . . . . . . . . . . . . . . . . 19 $/\$
45		simpl 444	. . . . . . . . . . . . . . . . . . . 20 $/\$
46	45	oveq2d 6056	. . . . . . . . . . . . . . . . . . 19 $/\$
47	44, 46	oveq12d 6058	. . . . . . . . . . . . . . . . . 18 $/\$
48	47	fveq2d 5691	. . . . . . . . . . . . . . . . 17 $/\$
49	48, 46	oveq12d 6058	. . . . . . . . . . . . . . . 16 $/\$
50		ovex 6065	. . . . . . . . . . . . . . . 16
51	49, 21, 50	ovmpt2a 6163	. . . . . . . . . . . . . . 15 $/\$
52	41, 42, 51	syl2anc 643	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
53	52	oveq1d 6055	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
54	5	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 $/\$
55	54	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
56		elrege0 10963	. . . . . . . . . . . . . . . . . . . 20 $/\$
57	55, 56	sylib 189	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
58	57	simpld 446	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
59	32	nnred 9971	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
60	58, 59	remulcld 9072	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
61	32	nnnn0d 10230	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
62	61	nn0ge0d 10233	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
63		mulge0 9501	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
64	57, 59, 62, 63	syl12anc 1182	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
65		flge0nn0 11180	. . . . . . . . . . . . . . . . 17 $/\$
66	60, 64, 65	syl2anc 643	. . . . . . . . . . . . . . . 16 $/\$ $/\$
67	66	adantr 452	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
68	67	nn0cnd 10232	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
69	32	adantr 452	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
70	69	nncnd 9972	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
71	69	nnne0d 10000	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
72	68, 70, 71	divcan1d 9747	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
73	53, 72	eqtrd 2436	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
74	73, 67	eqeltrd 2478	. . . . . . . . . . 11 $/\$ $/\$ $/\$
75		nn0uz 10476	. . . . . . . . . . 11
76	74, 75	syl6eleq 2494	. . . . . . . . . 10 $/\$ $/\$ $/\$
77		nnmulcl 9979	. . . . . . . . . . . . . 14 $/\$
78	31, 77	mpdan 650	. . . . . . . . . . . . 13
79	78	ad2antlr 708	. . . . . . . . . . . 12 $/\$ $/\$
80	79	adantr 452	. . . . . . . . . . 11 $/\$ $/\$ $/\$
81	80	nnzd 10330	. . . . . . . . . 10 $/\$ $/\$ $/\$
82		elfz5 11007	. . . . . . . . . 10 $/\$
83	76, 81, 82	syl2anc 643	. . . . . . . . 9 $/\$ $/\$ $/\$
84	39, 83	mpbird 224	. . . . . . . 8 $/\$ $/\$ $/\$
85		oveq1 6047	. . . . . . . . 9
86		eqid 2404	. . . . . . . . 9
87		ovex 6065	. . . . . . . . 9
88	85, 86, 87	fvmpt 5765	. . . . . . . 8
89	84, 88	syl 16	. . . . . . 7 $/\$ $/\$ $/\$
90	26	adantr 452	. . . . . . . . 9 $/\$ $/\$ $/\$
91	90	recnd 9070	. . . . . . . 8 $/\$ $/\$ $/\$
92	91, 70, 71	divcan4d 9752	. . . . . . 7 $/\$ $/\$ $/\$
93	89, 92	eqtrd 2436	. . . . . 6 $/\$ $/\$ $/\$
94		elfznn0 11039	. . . . . . . . . . . . 13
95	94	nn0red 10231	. . . . . . . . . . . 12
96	31	adantl 453	. . . . . . . . . . . 12 $/\$
97		nndivre 9991	. . . . . . . . . . . 12 $/\$
98	95, 96, 97	syl2anr 465	. . . . . . . . . . 11 $/\$ $/\$
99	98, 86	fmptd 5852	. . . . . . . . . 10 $/\$
100		ffn 5550	. . . . . . . . . 10
101	99, 100	syl 16	. . . . . . . . 9 $/\$
102	101	adantr 452	. . . . . . . 8 $/\$ $/\$
103	102	adantr 452	. . . . . . 7 $/\$ $/\$ $/\$
104		fnfvelrn 5826	. . . . . . 7 $/\$
105	103, 84, 104	syl2anc 643	. . . . . 6 $/\$ $/\$ $/\$
106	93, 105	eqeltrrd 2479	. . . . 5 $/\$ $/\$ $/\$
107	79	nnnn0d 10230	. . . . . . . . . . 11 $/\$ $/\$
108	107, 75	syl6eleq 2494	. . . . . . . . . 10 $/\$ $/\$
109		eluzfz2 11021	. . . . . . . . . 10
110	108, 109	syl 16	. . . . . . . . 9 $/\$ $/\$
111		oveq1 6047	. . . . . . . . . 10
112		ovex 6065	. . . . . . . . . 10
113	111, 86, 112	fvmpt 5765	. . . . . . . . 9
114	110, 113	syl 16	. . . . . . . 8 $/\$ $/\$
115	28	recnd 9070	. . . . . . . . 9 $/\$ $/\$
116	32	nncnd 9972	. . . . . . . . 9 $/\$ $/\$
117	32	nnne0d 10000	. . . . . . . . 9 $/\$ $/\$
118	115, 116, 117	divcan4d 9752	. . . . . . . 8 $/\$ $/\$
119	114, 118	eqtrd 2436	. . . . . . 7 $/\$ $/\$
120		fnfvelrn 5826	. . . . . . . 8 $/\$
121	102, 110, 120	syl2anc 643	. . . . . . 7 $/\$ $/\$
122	119, 121	eqeltrrd 2479	. . . . . 6 $/\$ $/\$
123	122	adantr 452	. . . . 5 $/\$ $/\$ $/\$
124	106, 123	ifclda 3726	. . . 4 $/\$ $/\$
125		eluzfz1 11020	. . . . . . . 8
126	108, 125	syl 16	. . . . . . 7 $/\$ $/\$
127		oveq1 6047	. . . . . . . 8
128		ovex 6065	. . . . . . . 8
129	127, 86, 128	fvmpt 5765	. . . . . . 7
130	126, 129	syl 16	. . . . . 6 $/\$ $/\$
131		nncn 9964	. . . . . . . 8
132		nnne0 9988	. . . . . . . 8
133	131, 132	div0d 9745	. . . . . . 7
134	32, 133	syl 16	. . . . . 6 $/\$ $/\$
135	130, 134	eqtrd 2436	. . . . 5 $/\$ $/\$
136		fnfvelrn 5826	. . . . . 6 $/\$
137	102, 126, 136	syl2anc 643	. . . . 5 $/\$ $/\$
138	135, 137	eqeltrrd 2479	. . . 4 $/\$ $/\$
139		ifcl 3735	. . . 4 $/\$
140	124, 138, 139	syl2anc 643	. . 3 $/\$ $/\$
141		eqid 2404	. . 3
142	140, 141	fmptd 5852	. 2 $/\$
143		mbfi1fseq.1	. . . . 5 MblFn
144		mbfi1fseq.4	. . . . 5
145	143, 5, 21, 144	mbfi1fseqlem2 19561	. . . 4
146	145	adantl 453	. . 3 $/\$
147	146	feq1d 5539	. 2 $/\$
148	142, 147	mpbird 224	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359

wceq 1649

wcel 1721

wral 2666

wss 3280

cif 3699 class class class wbr 4172

cmpt 4226

cxp 4835

crn 4838

wfn 5408

wf 5409

cfv 5413 (class class class)co 6040

cmpt2 6042

cr 8945

cc0 8946

cmul 8951

cpnf 9073

cxr 9075

clt 9076

cle 9077

cneg 9248

cdiv 9633

cn 9956

c2 10005

cn0 10177

cz 10238

cuz 10444

cico 10874

cicc 10875

cfz 10999

cfl 11156

cexp 11337 MblFncmbf 19459

This theorem is referenced by: mbfi1fseqlem4 19563

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-er 6864 df-en 7069 df-dom 7070 df-sdom 7071 df-sup 7404 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-n0 10178 df-z 10239 df-uz 10445 df-ico 10878 df-fz 11000 df-fl 11157 df-seq 11279 df-exp 11338

W3C validator