mbfi1fseqlem6 - Metamath Proof Explorer

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

Theorem mbfi1fseqlem6 21201

Description: Lemma for mbfi1fseq 21202. Verify that

converges pointwise to

, and wrap up the existence quantifier. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)

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

**Assertion**
Ref	Expression
mbfi1fseqlem6	$/\$ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

Proof of Theorem mbfi1fseqlem6 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mbfi1fseq.1	. . 3 MblFn
2		mbfi1fseq.2	. . 3
3		mbfi1fseq.3	. . 3
4		mbfi1fseq.4	. . 3
5	1, 2, 3, 4	mbfi1fseqlem4 21199	. 2
6	1, 2, 3, 4	mbfi1fseqlem5 21200	. . 3 $/\$ $/\$
7	6	ralrimiva 2802	. 2 $/\$
8		simpr 461	. . . . . . . 8 $/\$
9	8	recnd 9415	. . . . . . 7 $/\$
10	9	abscld 12925	. . . . . 6 $/\$
11	2	ffvelrnda 5846	. . . . . . . 8 $/\$
12		elrege0 11395	. . . . . . . 8 $/\$
13	11, 12	sylib 196	. . . . . . 7 $/\$ $/\$
14	13	simpld 459	. . . . . 6 $/\$
15	10, 14	readdcld 9416	. . . . 5 $/\$
16		arch 10579	. . . . 5
17	15, 16	syl 16	. . . 4 $/\$
18		eqid 2443	. . . . 5
19		nnz 10671	. . . . . 6
20	19	ad2antrl 727	. . . . 5 $/\$ $/\$ $/\$
21		nnuz 10899	. . . . . . . 8
22		1zzd 10680	. . . . . . . 8 $/\$
23		halfcn 10544	. . . . . . . . . 10
24	23	a1i 11	. . . . . . . . 9 $/\$
25		halfre 10543	. . . . . . . . . . . 12
26		0re 9389	. . . . . . . . . . . . 13
27		halfgt0 10545	. . . . . . . . . . . . 13
28	26, 25, 27	ltleii 9500	. . . . . . . . . . . 12
29		absid 12788	. . . . . . . . . . . 12 $/\$
30	25, 28, 29	mp2an 672	. . . . . . . . . . 11
31		halflt1 10546	. . . . . . . . . . 11
32	30, 31	eqbrtri 4314	. . . . . . . . . 10
33	32	a1i 11	. . . . . . . . 9 $/\$
34	24, 33	expcnv 13329	. . . . . . . 8 $/\$
35	14	recnd 9415	. . . . . . . 8 $/\$
36		nnex 10331	. . . . . . . . . 10
37	36	mptex 5951	. . . . . . . . 9
38	37	a1i 11	. . . . . . . 8 $/\$
39		nnnn0 10589	. . . . . . . . . . 11
40	39	adantl 466	. . . . . . . . . 10 $/\$ $/\$
41		oveq2 6102	. . . . . . . . . . 11
42		eqid 2443	. . . . . . . . . . 11
43		ovex 6119	. . . . . . . . . . 11
44	41, 42, 43	fvmpt 5777	. . . . . . . . . 10
45	40, 44	syl 16	. . . . . . . . 9 $/\$ $/\$
46		expcl 11886	. . . . . . . . . 10 $/\$
47	23, 40, 46	sylancr 663	. . . . . . . . 9 $/\$ $/\$
48	45, 47	eqeltrd 2517	. . . . . . . 8 $/\$ $/\$
49	41	oveq2d 6110	. . . . . . . . . . 11
50		eqid 2443	. . . . . . . . . . 11
51		ovex 6119	. . . . . . . . . . 11
52	49, 50, 51	fvmpt 5777	. . . . . . . . . 10
53	52	adantl 466	. . . . . . . . 9 $/\$ $/\$
54	45	oveq2d 6110	. . . . . . . . 9 $/\$ $/\$
55	53, 54	eqtr4d 2478	. . . . . . . 8 $/\$ $/\$
56	21, 22, 34, 35, 38, 48, 55	climsubc2 13119	. . . . . . 7 $/\$
57	35	subid1d 9711	. . . . . . 7 $/\$
58	56, 57	breqtrd 4319	. . . . . 6 $/\$
59	58	adantr 465	. . . . 5 $/\$ $/\$ $/\$
60	36	mptex 5951	. . . . . 6
61	60	a1i 11	. . . . 5 $/\$ $/\$ $/\$
62		simprl 755	. . . . . . . 8 $/\$ $/\$ $/\$
63		eluznn 10928	. . . . . . . 8 $/\$
64	62, 63	sylan 471	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
65	64, 52	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$
66	14	ad2antrr 725	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
67	64, 39	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
68		reexpcl 11885	. . . . . . . 8 $/\$
69	25, 67, 68	sylancr 663	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
70	66, 69	resubcld 9779	. . . . . 6 $/\$ $/\$ $/\$ $/\$
71	65, 70	eqeltrd 2517	. . . . 5 $/\$ $/\$ $/\$ $/\$
72		fveq2 5694	. . . . . . . . 9
73	72	fveq1d 5696	. . . . . . . 8
74		eqid 2443	. . . . . . . 8
75		fvex 5704	. . . . . . . 8
76	73, 74, 75	fvmpt 5777	. . . . . . 7
77	64, 76	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$
78	5	ad3antrrr 729	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
79	78, 64	ffvelrnd 5847	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
80		i1ff 21157	. . . . . . . 8
81	79, 80	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
82	8	ad2antrr 725	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
83	81, 82	ffvelrnd 5847	. . . . . 6 $/\$ $/\$ $/\$ $/\$
84	77, 83	eqeltrd 2517	. . . . 5 $/\$ $/\$ $/\$ $/\$
85	35	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
86		2nn 10482	. . . . . . . . . . . . . 14
87		nnexpcl 11881	. . . . . . . . . . . . . 14 $/\$
88	86, 67, 87	sylancr 663	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
89	88	nnred 10340	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
90	89	recnd 9415	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	88	nnne0d 10369	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
92	85, 90, 91	divcan4d 10116	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
93	92	eqcomd 2448	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
94		2cnd 10397	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
95		2ne0 10417	. . . . . . . . . . 11
96	95	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
97		eluzelz 10873	. . . . . . . . . . 11
98	97	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
99	94, 96, 98	exprecd 12019	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
100	93, 99	oveq12d 6112	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
101	66, 89	remulcld 9417	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
102	101	recnd 9415	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
103		1cnd 9405	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
104	102, 103, 90, 91	divsubdird 10149	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
105	100, 104	eqtr4d 2478	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
106		fllep1 11654	. . . . . . . . . 10
107	101, 106	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
108		1red 9404	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
109		reflcl 11649	. . . . . . . . . . 11
110	101, 109	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
111	101, 108, 110	lesubaddd 9939	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
112	107, 111	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
113		peano2rem 9678	. . . . . . . . . 10
114	101, 113	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
115	88	nngt0d 10368	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
116		lediv1 10197	. . . . . . . . 9 $/\$ $/\$ $/\$
117	114, 110, 89, 115, 116	syl112anc 1222	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
118	112, 117	mpbid 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
119	105, 118	eqbrtrd 4315	. . . . . 6 $/\$ $/\$ $/\$ $/\$
120	1, 2, 3, 4	mbfi1fseqlem2 21197	. . . . . . . . . 10
121	64, 120	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
122	121	fveq1d 5696	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
123		ovex 6119	. . . . . . . . . . 11
124		vex 2978	. . . . . . . . . . 11
125	123, 124	ifex 3861	. . . . . . . . . 10
126		c0ex 9383	. . . . . . . . . 10
127	125, 126	ifex 3861	. . . . . . . . 9
128		eqid 2443	. . . . . . . . . 10
129	128	fvmpt2 5784	. . . . . . . . 9 $/\$
130	82, 127, 129	sylancl 662	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
131	77, 122, 130	3eqtrd 2479	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
132	10	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
133	15	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
134	64	nnred 10340	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
135	11	ad2antrr 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
136	135, 12	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
137	136	simprd 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
138	132, 66	addge01d 9930	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
139	137, 138	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
140	62	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
141	140	nnred 10340	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
142		simplrr 760	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
143	133, 141, 142	ltled 9525	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
144		eluzle 10876	. . . . . . . . . . . . . 14
145	144	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
146	133, 141, 134, 143, 145	letrd 9531	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
147	132, 133, 134, 139, 146	letrd 9531	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
148	82, 134	absled 12920	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
149	147, 148	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
150	149	simpld 459	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
151	149	simprd 463	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
152	134	renegcld 9778	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
153		elicc2 11363	. . . . . . . . . 10 $/\$ $/\$ $/\$
154	152, 134, 153	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
155	82, 150, 151, 154	mpbir3and 1171	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
156		iftrue 3800	. . . . . . . 8
157	155, 156	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
158		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
159	158	fveq2d 5698	. . . . . . . . . . . . . . 15 $/\$
160		simpl 457	. . . . . . . . . . . . . . . 16 $/\$
161	160	oveq2d 6110	. . . . . . . . . . . . . . 15 $/\$
162	159, 161	oveq12d 6112	. . . . . . . . . . . . . 14 $/\$
163	162	fveq2d 5698	. . . . . . . . . . . . 13 $/\$
164	163, 161	oveq12d 6112	. . . . . . . . . . . 12 $/\$
165		ovex 6119	. . . . . . . . . . . 12
166	164, 3, 165	ovmpt2a 6224	. . . . . . . . . . 11 $/\$
167	64, 82, 166	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
168	110, 88	nndivred 10373	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
169		flle 11652	. . . . . . . . . . . . 13
170	101, 169	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
171		ledivmul2 10212	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
172	110, 66, 89, 115, 171	syl112anc 1222	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
173	170, 172	mpbird 232	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
174	9	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
175	174	absge0d 12933	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
176	66, 132	addge02d 9931	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
177	175, 176	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
178	66, 133, 134, 177, 146	letrd 9531	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
179	168, 66, 134, 173, 178	letrd 9531	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
180	167, 179	eqbrtrd 4315	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
181		iftrue 3800	. . . . . . . . 9
182	180, 181	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
183	182, 167	eqtrd 2475	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
184	131, 157, 183	3eqtrd 2479	. . . . . 6 $/\$ $/\$ $/\$ $/\$
185	119, 65, 184	3brtr4d 4325	. . . . 5 $/\$ $/\$ $/\$ $/\$
186	184, 173	eqbrtrd 4315	. . . . 5 $/\$ $/\$ $/\$ $/\$
187	18, 20, 59, 61, 71, 84, 185, 186	climsqz 13121	. . . 4 $/\$ $/\$ $/\$
188	17, 187	rexlimddv 2848	. . 3 $/\$
189	188	ralrimiva 2802	. 2
190	36	mptex 5951	. . . 4
191	4, 190	eqeltri 2513	. . 3
192		feq1 5545	. . . 4
193		fveq1 5693	. . . . . . 7
194	193	breq2d 4307	. . . . . 6
195		fveq1 5693	. . . . . . 7
196	193, 195	breq12d 4308	. . . . . 6
197	194, 196	anbi12d 710	. . . . 5 $/\$ $/\$
198	197	ralbidv 2738	. . . 4 $/\$ $/\$
199	193	fveq1d 5696	. . . . . . 7
200	199	mpteq2dv 4382	. . . . . 6
201	200	breq1d 4305	. . . . 5
202	201	ralbidv 2738	. . . 4
203	192, 198, 202	3anbi123d 1289	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
204	191, 203	spcev 3067	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
205	5, 7, 189, 204	syl3anc 1218	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wex 1586

wcel 1756

wne 2609

wral 2718

wrex 2719

cvv 2975

cif 3794 class class class wbr 4295

cmpt 4353

cdm 4843

wf 5417

cfv 5421 (class class class)co 6094

cmpt2 6096

cofr 6322

cc 9283

cr 9284

cc0 9285

c1 9286

caddc 9288

cmul 9290

cpnf 9418

clt 9421

cle 9422

cmin 9598

cneg 9599

cdiv 9996

cn 10325

c2 10374

cn0 10582

cz 10649

cuz 10864

cico 11305

cicc 11306

cfl 11643

cexp 11868

cabs 12726

cli 12965 MblFncmbf 21097

citg1 21098

c0p 21150

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4406 ax-sep 4416 ax-nul 4424 ax-pow 4473 ax-pr 4534 ax-un 6375 ax-inf2 7850 ax-cnex 9341 ax-resscn 9342 ax-1cn 9343 ax-icn 9344 ax-addcl 9345 ax-addrcl 9346 ax-mulcl 9347 ax-mulrcl 9348 ax-mulcom 9349 ax-addass 9350 ax-mulass 9351 ax-distr 9352 ax-i2m1 9353 ax-1ne0 9354 ax-1rid 9355 ax-rnegex 9356 ax-rrecex 9357 ax-cnre 9358 ax-pre-lttri 9359 ax-pre-lttrn 9360 ax-pre-ltadd 9361 ax-pre-mulgt0 9362 ax-pre-sup 9363

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2571 df-ne 2611 df-nel 2612 df-ral 2723 df-rex 2724 df-reu 2725 df-rmo 2726 df-rab 2727 df-v 2977 df-sbc 3190 df-csb 3292 df-dif 3334 df-un 3336 df-in 3338 df-ss 3345 df-pss 3347 df-nul 3641 df-if 3795 df-pw 3865 df-sn 3881 df-pr 3883 df-tp 3885 df-op 3887 df-uni 4095 df-int 4132 df-iun 4176 df-br 4296 df-opab 4354 df-mpt 4355 df-tr 4389 df-eprel 4635 df-id 4639 df-po 4644 df-so 4645 df-fr 4682 df-se 4683 df-we 4684 df-ord 4725 df-on 4726 df-lim 4727 df-suc 4728 df-xp 4849 df-rel 4850 df-cnv 4851 df-co 4852 df-dm 4853 df-rn 4854 df-res 4855 df-ima 4856 df-iota 5384 df-fun 5423 df-fn 5424 df-f 5425 df-f1 5426 df-fo 5427 df-f1o 5428 df-fv 5429 df-isom 5430 df-riota 6055 df-ov 6097 df-oprab 6098 df-mpt2 6099 df-of 6323 df-ofr 6324 df-om 6480 df-1st 6580 df-2nd 6581 df-recs 6835 df-rdg 6869 df-1o 6923 df-2o 6924 df-oadd 6927 df-er 7104 df-map 7219 df-pm 7220 df-en 7314 df-dom 7315 df-sdom 7316 df-fin 7317 df-fi 7664 df-sup 7694 df-oi 7727 df-card 8112 df-cda 8340 df-pnf 9423 df-mnf 9424 df-xr 9425 df-ltxr 9426 df-le 9427 df-sub 9600 df-neg 9601 df-div 9997 df-nn 10326 df-2 10383 df-3 10384 df-n0 10583 df-z 10650 df-uz 10865 df-q 10957 df-rp 10995 df-xneg 11092 df-xadd 11093 df-xmul 11094 df-ioo 11307 df-ico 11309 df-icc 11310 df-fz 11441 df-fzo 11552 df-fl 11645 df-seq 11810 df-exp 11869 df-hash 12107 df-cj 12591 df-re 12592 df-im 12593 df-sqr 12727 df-abs 12728 df-clim 12969 df-rlim 12970 df-sum 13167 df-rest 14364 df-topgen 14385 df-psmet 17812 df-xmet 17813 df-met 17814 df-bl 17815 df-mopn 17816 df-top 18506 df-bases 18508 df-topon 18509 df-cmp 18993 df-ovol 20951 df-vol 20952 df-mbf 21102 df-itg1 21103 df-0p 21151

This theorem is referenced by: mbfi1fseq 21202

W3C validator