mbfi1fseqlem6 - Metamath Proof Explorer

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

Theorem mbfi1fseqlem6 21040

Description: Lemma for mbfi1fseq 21041. 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 21038	. 2
6	1, 2, 3, 4	mbfi1fseqlem5 21039	. . 3 $/\$ $/\$
7	6	ralrimiva 2789	. 2 $/\$
8		simpr 458	. . . . . . . 8 $/\$
9	8	recnd 9400	. . . . . . 7 $/\$
10	9	abscld 12906	. . . . . 6 $/\$
11	2	ffvelrnda 5831	. . . . . . . 8 $/\$
12		elrege0 11380	. . . . . . . 8 $/\$
13	11, 12	sylib 196	. . . . . . 7 $/\$ $/\$
14	13	simpld 456	. . . . . 6 $/\$
15	10, 14	readdcld 9401	. . . . 5 $/\$
16		arch 10564	. . . . 5
17	15, 16	syl 16	. . . 4 $/\$
18		eqid 2433	. . . . 5
19		nnz 10656	. . . . . 6
20	19	ad2antrl 720	. . . . 5 $/\$ $/\$ $/\$
21		nnuz 10884	. . . . . . . 8
22		1zzd 10665	. . . . . . . 8 $/\$
23		halfcn 10529	. . . . . . . . . 10
24	23	a1i 11	. . . . . . . . 9 $/\$
25		halfre 10528	. . . . . . . . . . . 12
26		0re 9374	. . . . . . . . . . . . 13
27		halfgt0 10530	. . . . . . . . . . . . 13
28	26, 25, 27	ltleii 9485	. . . . . . . . . . . 12
29		absid 12769	. . . . . . . . . . . 12 $/\$
30	25, 28, 29	mp2an 665	. . . . . . . . . . 11
31		halflt1 10531	. . . . . . . . . . 11
32	30, 31	eqbrtri 4299	. . . . . . . . . 10
33	32	a1i 11	. . . . . . . . 9 $/\$
34	24, 33	expcnv 13309	. . . . . . . 8 $/\$
35	14	recnd 9400	. . . . . . . 8 $/\$
36		nnex 10316	. . . . . . . . . 10
37	36	mptex 5935	. . . . . . . . 9
38	37	a1i 11	. . . . . . . 8 $/\$
39		nnnn0 10574	. . . . . . . . . . 11
40	39	adantl 463	. . . . . . . . . 10 $/\$ $/\$
41		oveq2 6088	. . . . . . . . . . 11
42		eqid 2433	. . . . . . . . . . 11
43		ovex 6105	. . . . . . . . . . 11
44	41, 42, 43	fvmpt 5762	. . . . . . . . . 10
45	40, 44	syl 16	. . . . . . . . 9 $/\$ $/\$
46		expcl 11867	. . . . . . . . . 10 $/\$
47	23, 40, 46	sylancr 656	. . . . . . . . 9 $/\$ $/\$
48	45, 47	eqeltrd 2507	. . . . . . . 8 $/\$ $/\$
49	41	oveq2d 6096	. . . . . . . . . . 11
50		eqid 2433	. . . . . . . . . . 11
51		ovex 6105	. . . . . . . . . . 11
52	49, 50, 51	fvmpt 5762	. . . . . . . . . 10
53	52	adantl 463	. . . . . . . . 9 $/\$ $/\$
54	45	oveq2d 6096	. . . . . . . . 9 $/\$ $/\$
55	53, 54	eqtr4d 2468	. . . . . . . 8 $/\$ $/\$
56	21, 22, 34, 35, 38, 48, 55	climsubc2 13100	. . . . . . 7 $/\$
57	35	subid1d 9696	. . . . . . 7 $/\$
58	56, 57	breqtrd 4304	. . . . . 6 $/\$
59	58	adantr 462	. . . . 5 $/\$ $/\$ $/\$
60	36	mptex 5935	. . . . . 6
61	60	a1i 11	. . . . 5 $/\$ $/\$ $/\$
62		simprl 748	. . . . . . . 8 $/\$ $/\$ $/\$
63		eluznn 10913	. . . . . . . 8 $/\$
64	62, 63	sylan 468	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
65	64, 52	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$
66	14	ad2antrr 718	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
67	64, 39	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
68		reexpcl 11866	. . . . . . . 8 $/\$
69	25, 67, 68	sylancr 656	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
70	66, 69	resubcld 9764	. . . . . 6 $/\$ $/\$ $/\$ $/\$
71	65, 70	eqeltrd 2507	. . . . 5 $/\$ $/\$ $/\$ $/\$
72		fveq2 5679	. . . . . . . . 9
73	72	fveq1d 5681	. . . . . . . 8
74		eqid 2433	. . . . . . . 8
75		fvex 5689	. . . . . . . 8
76	73, 74, 75	fvmpt 5762	. . . . . . 7
77	64, 76	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$
78	5	ad3antrrr 722	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
79	78, 64	ffvelrnd 5832	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
80		i1ff 20996	. . . . . . . 8
81	79, 80	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
82	8	ad2antrr 718	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
83	81, 82	ffvelrnd 5832	. . . . . 6 $/\$ $/\$ $/\$ $/\$
84	77, 83	eqeltrd 2507	. . . . 5 $/\$ $/\$ $/\$ $/\$
85	35	ad2antrr 718	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
86		2nn 10467	. . . . . . . . . . . . . 14
87		nnexpcl 11862	. . . . . . . . . . . . . 14 $/\$
88	86, 67, 87	sylancr 656	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
89	88	nnred 10325	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
90	89	recnd 9400	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	88	nnne0d 10354	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
92	85, 90, 91	divcan4d 10101	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
93	92	eqcomd 2438	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
94		2cnd 10382	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
95		2ne0 10402	. . . . . . . . . . 11
96	95	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
97		eluzelz 10858	. . . . . . . . . . 11
98	97	adantl 463	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
99	94, 96, 98	exprecd 12000	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
100	93, 99	oveq12d 6098	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
101	66, 89	remulcld 9402	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
102	101	recnd 9400	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
103		1cnd 9390	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
104	102, 103, 90, 91	divsubdird 10134	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
105	100, 104	eqtr4d 2468	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
106		fllep1 11635	. . . . . . . . . 10
107	101, 106	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
108		1red 9389	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
109		reflcl 11630	. . . . . . . . . . 11
110	101, 109	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
111	101, 108, 110	lesubaddd 9924	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
112	107, 111	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
113		peano2rem 9663	. . . . . . . . . 10
114	101, 113	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
115	88	nngt0d 10353	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
116		lediv1 10182	. . . . . . . . 9 $/\$ $/\$ $/\$
117	114, 110, 89, 115, 116	syl112anc 1215	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
118	112, 117	mpbid 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
119	105, 118	eqbrtrd 4300	. . . . . 6 $/\$ $/\$ $/\$ $/\$
120	1, 2, 3, 4	mbfi1fseqlem2 21036	. . . . . . . . . 10
121	64, 120	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
122	121	fveq1d 5681	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
123		ovex 6105	. . . . . . . . . . 11
124		vex 2965	. . . . . . . . . . 11
125	123, 124	ifex 3846	. . . . . . . . . 10
126		c0ex 9368	. . . . . . . . . 10
127	125, 126	ifex 3846	. . . . . . . . 9
128		eqid 2433	. . . . . . . . . 10
129	128	fvmpt2 5769	. . . . . . . . 9 $/\$
130	82, 127, 129	sylancl 655	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
131	77, 122, 130	3eqtrd 2469	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
132	10	ad2antrr 718	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
133	15	ad2antrr 718	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
134	64	nnred 10325	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
135	11	ad2antrr 718	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
136	135, 12	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
137	136	simprd 460	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
138	132, 66	addge01d 9915	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
139	137, 138	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
140	62	adantr 462	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
141	140	nnred 10325	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
142		simplrr 753	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
143	133, 141, 142	ltled 9510	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
144		eluzle 10861	. . . . . . . . . . . . . 14
145	144	adantl 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
146	133, 141, 134, 143, 145	letrd 9516	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
147	132, 133, 134, 139, 146	letrd 9516	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
148	82, 134	absled 12901	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
149	147, 148	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
150	149	simpld 456	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
151	149	simprd 460	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
152	134	renegcld 9763	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
153		elicc2 11348	. . . . . . . . . 10 $/\$ $/\$ $/\$
154	152, 134, 153	syl2anc 654	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
155	82, 150, 151, 154	mpbir3and 1164	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
156		iftrue 3785	. . . . . . . 8
157	155, 156	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
158		simpr 458	. . . . . . . . . . . . . . . 16 $/\$
159	158	fveq2d 5683	. . . . . . . . . . . . . . 15 $/\$
160		simpl 454	. . . . . . . . . . . . . . . 16 $/\$
161	160	oveq2d 6096	. . . . . . . . . . . . . . 15 $/\$
162	159, 161	oveq12d 6098	. . . . . . . . . . . . . 14 $/\$
163	162	fveq2d 5683	. . . . . . . . . . . . 13 $/\$
164	163, 161	oveq12d 6098	. . . . . . . . . . . 12 $/\$
165		ovex 6105	. . . . . . . . . . . 12
166	164, 3, 165	ovmpt2a 6210	. . . . . . . . . . 11 $/\$
167	64, 82, 166	syl2anc 654	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
168	110, 88	nndivred 10358	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
169		flle 11633	. . . . . . . . . . . . 13
170	101, 169	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
171		ledivmul2 10197	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
172	110, 66, 89, 115, 171	syl112anc 1215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
173	170, 172	mpbird 232	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
174	9	ad2antrr 718	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
175	174	absge0d 12914	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
176	66, 132	addge02d 9916	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
177	175, 176	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
178	66, 133, 134, 177, 146	letrd 9516	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
179	168, 66, 134, 173, 178	letrd 9516	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
180	167, 179	eqbrtrd 4300	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
181		iftrue 3785	. . . . . . . . 9
182	180, 181	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
183	182, 167	eqtrd 2465	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
184	131, 157, 183	3eqtrd 2469	. . . . . 6 $/\$ $/\$ $/\$ $/\$
185	119, 65, 184	3brtr4d 4310	. . . . 5 $/\$ $/\$ $/\$ $/\$
186	184, 173	eqbrtrd 4300	. . . . 5 $/\$ $/\$ $/\$ $/\$
187	18, 20, 59, 61, 71, 84, 185, 186	climsqz 13102	. . . 4 $/\$ $/\$ $/\$
188	17, 187	rexlimddv 2835	. . 3 $/\$
189	188	ralrimiva 2789	. 2
190	36	mptex 5935	. . . 4
191	4, 190	eqeltri 2503	. . 3
192		feq1 5530	. . . 4
193		fveq1 5678	. . . . . . 7
194	193	breq2d 4292	. . . . . 6
195		fveq1 5678	. . . . . . 7
196	193, 195	breq12d 4293	. . . . . 6
197	194, 196	anbi12d 703	. . . . 5 $/\$ $/\$
198	197	ralbidv 2725	. . . 4 $/\$ $/\$
199	193	fveq1d 5681	. . . . . . 7
200	199	mpteq2dv 4367	. . . . . 6
201	200	breq1d 4290	. . . . 5
202	201	ralbidv 2725	. . . 4
203	192, 198, 202	3anbi123d 1282	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
204	191, 203	spcev 3053	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
205	5, 7, 189, 204	syl3anc 1211	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1362

wex 1589

wcel 1755

wne 2596

wral 2705

wrex 2706

cvv 2962

cif 3779 class class class wbr 4280

cmpt 4338

cdm 4827

wf 5402

cfv 5406 (class class class)co 6080

cmpt2 6082

cofr 6308

cc 9268

cr 9269

cc0 9270

c1 9271

caddc 9273

cmul 9275

cpnf 9403

clt 9406

cle 9407

cmin 9583

cneg 9584

cdiv 9981

cn 10310

c2 10359

cn0 10567

cz 10634

cuz 10849

cico 11290

cicc 11291

cfl 11624

cexp 11849

cabs 12707

cli 12946 MblFncmbf 20936

citg1 20937

c0p 20989

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-inf2 7835 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346 ax-pre-mulgt0 9347 ax-pre-sup 9348

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-fal 1368 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-se 4667 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-isom 5415 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-of 6309 df-ofr 6310 df-om 6466 df-1st 6566 df-2nd 6567 df-recs 6818 df-rdg 6852 df-1o 6908 df-2o 6909 df-oadd 6912 df-er 7089 df-map 7204 df-pm 7205 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-fi 7649 df-sup 7679 df-oi 7712 df-card 8097 df-cda 8325 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-sub 9585 df-neg 9586 df-div 9982 df-nn 10311 df-2 10368 df-3 10369 df-n0 10568 df-z 10635 df-uz 10850 df-q 10942 df-rp 10980 df-xneg 11077 df-xadd 11078 df-xmul 11079 df-ioo 11292 df-ico 11294 df-icc 11295 df-fz 11425 df-fzo 11533 df-fl 11626 df-seq 11791 df-exp 11850 df-hash 12088 df-cj 12572 df-re 12573 df-im 12574 df-sqr 12708 df-abs 12709 df-clim 12950 df-rlim 12951 df-sum 13148 df-rest 14344 df-topgen 14365 df-psmet 17653 df-xmet 17654 df-met 17655 df-bl 17656 df-mopn 17657 df-top 18345 df-bases 18347 df-topon 18348 df-cmp 18832 df-ovol 20790 df-vol 20791 df-mbf 20941 df-itg1 20942 df-0p 20990

This theorem is referenced by: mbfi1fseq 21041

W3C validator