mbfi1fseqlem6 - Metamath Proof Explorer

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

Theorem mbfi1fseqlem6 22757

Description: Lemma for mbfi1fseq 22758. 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 22755	. 2
6	1, 2, 3, 4	mbfi1fseqlem5 22756	. . 3 $/\$ $/\$
7	6	ralrimiva 2809	. 2 $/\$
8		simpr 468	. . . . . . . 8 $/\$
9	8	recnd 9687	. . . . . . 7 $/\$
10	9	abscld 13575	. . . . . 6 $/\$
11	2	ffvelrnda 6037	. . . . . . . 8 $/\$
12		elrege0 11764	. . . . . . . 8 $/\$
13	11, 12	sylib 201	. . . . . . 7 $/\$ $/\$
14	13	simpld 466	. . . . . 6 $/\$
15	10, 14	readdcld 9688	. . . . 5 $/\$
16		arch 10890	. . . . 5
17	15, 16	syl 17	. . . 4 $/\$
18		eqid 2471	. . . . 5
19		nnz 10983	. . . . . 6
20	19	ad2antrl 742	. . . . 5 $/\$ $/\$ $/\$
21		nnuz 11218	. . . . . . . 8
22		1zzd 10992	. . . . . . . 8 $/\$
23		halfcn 10852	. . . . . . . . . 10
24	23	a1i 11	. . . . . . . . 9 $/\$
25		halfre 10851	. . . . . . . . . . . 12
26		0re 9661	. . . . . . . . . . . . 13
27		halfgt0 10853	. . . . . . . . . . . . 13
28	26, 25, 27	ltleii 9775	. . . . . . . . . . . 12
29		absid 13436	. . . . . . . . . . . 12 $/\$
30	25, 28, 29	mp2an 686	. . . . . . . . . . 11
31		halflt1 10854	. . . . . . . . . . 11
32	30, 31	eqbrtri 4415	. . . . . . . . . 10
33	32	a1i 11	. . . . . . . . 9 $/\$
34	24, 33	expcnv 13999	. . . . . . . 8 $/\$
35	14	recnd 9687	. . . . . . . 8 $/\$
36		nnex 10637	. . . . . . . . . 10
37	36	mptex 6152	. . . . . . . . 9
38	37	a1i 11	. . . . . . . 8 $/\$
39		nnnn0 10900	. . . . . . . . . . 11
40	39	adantl 473	. . . . . . . . . 10 $/\$ $/\$
41		oveq2 6316	. . . . . . . . . . 11
42		eqid 2471	. . . . . . . . . . 11
43		ovex 6336	. . . . . . . . . . 11
44	41, 42, 43	fvmpt 5963	. . . . . . . . . 10
45	40, 44	syl 17	. . . . . . . . 9 $/\$ $/\$
46		expcl 12328	. . . . . . . . . 10 $/\$
47	23, 40, 46	sylancr 676	. . . . . . . . 9 $/\$ $/\$
48	45, 47	eqeltrd 2549	. . . . . . . 8 $/\$ $/\$
49	41	oveq2d 6324	. . . . . . . . . . 11
50		eqid 2471	. . . . . . . . . . 11
51		ovex 6336	. . . . . . . . . . 11
52	49, 50, 51	fvmpt 5963	. . . . . . . . . 10
53	52	adantl 473	. . . . . . . . 9 $/\$ $/\$
54	45	oveq2d 6324	. . . . . . . . 9 $/\$ $/\$
55	53, 54	eqtr4d 2508	. . . . . . . 8 $/\$ $/\$
56	21, 22, 34, 35, 38, 48, 55	climsubc2 13779	. . . . . . 7 $/\$
57	35	subid1d 9994	. . . . . . 7 $/\$
58	56, 57	breqtrd 4420	. . . . . 6 $/\$
59	58	adantr 472	. . . . 5 $/\$ $/\$ $/\$
60	36	mptex 6152	. . . . . 6
61	60	a1i 11	. . . . 5 $/\$ $/\$ $/\$
62		simprl 772	. . . . . . . 8 $/\$ $/\$ $/\$
63		eluznn 11252	. . . . . . . 8 $/\$
64	62, 63	sylan 479	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
65	64, 52	syl 17	. . . . . 6 $/\$ $/\$ $/\$ $/\$
66	14	ad2antrr 740	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
67	64, 39	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
68		reexpcl 12327	. . . . . . . 8 $/\$
69	25, 67, 68	sylancr 676	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
70	66, 69	resubcld 10068	. . . . . 6 $/\$ $/\$ $/\$ $/\$
71	65, 70	eqeltrd 2549	. . . . 5 $/\$ $/\$ $/\$ $/\$
72		fveq2 5879	. . . . . . . . 9
73	72	fveq1d 5881	. . . . . . . 8
74		eqid 2471	. . . . . . . 8
75		fvex 5889	. . . . . . . 8
76	73, 74, 75	fvmpt 5963	. . . . . . 7
77	64, 76	syl 17	. . . . . 6 $/\$ $/\$ $/\$ $/\$
78	5	ad3antrrr 744	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
79	78, 64	ffvelrnd 6038	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
80		i1ff 22713	. . . . . . . 8
81	79, 80	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
82	8	ad2antrr 740	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
83	81, 82	ffvelrnd 6038	. . . . . 6 $/\$ $/\$ $/\$ $/\$
84	77, 83	eqeltrd 2549	. . . . 5 $/\$ $/\$ $/\$ $/\$
85	35	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
86		2nn 10790	. . . . . . . . . . . . . 14
87		nnexpcl 12323	. . . . . . . . . . . . . 14 $/\$
88	86, 67, 87	sylancr 676	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
89	88	nnred 10646	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
90	89	recnd 9687	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	88	nnne0d 10676	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
92	85, 90, 91	divcan4d 10411	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
93	92	eqcomd 2477	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
94		2cnd 10704	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
95		2ne0 10724	. . . . . . . . . . 11
96	95	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
97		eluzelz 11192	. . . . . . . . . . 11
98	97	adantl 473	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
99	94, 96, 98	exprecd 12462	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
100	93, 99	oveq12d 6326	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
101	66, 89	remulcld 9689	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
102	101	recnd 9687	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
103		1cnd 9677	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
104	102, 103, 90, 91	divsubdird 10444	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
105	100, 104	eqtr4d 2508	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
106		fllep1 12070	. . . . . . . . . 10
107	101, 106	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
108		1red 9676	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
109		reflcl 12065	. . . . . . . . . . 11
110	101, 109	syl 17	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
111	101, 108, 110	lesubaddd 10231	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
112	107, 111	mpbird 240	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
113		peano2rem 9961	. . . . . . . . . 10
114	101, 113	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
115	88	nngt0d 10675	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
116		lediv1 10492	. . . . . . . . 9 $/\$ $/\$ $/\$
117	114, 110, 89, 115, 116	syl112anc 1296	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
118	112, 117	mpbid 215	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
119	105, 118	eqbrtrd 4416	. . . . . 6 $/\$ $/\$ $/\$ $/\$
120	1, 2, 3, 4	mbfi1fseqlem2 22753	. . . . . . . . . 10
121	64, 120	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
122	121	fveq1d 5881	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
123		ovex 6336	. . . . . . . . . . 11
124		vex 3034	. . . . . . . . . . 11
125	123, 124	ifex 3940	. . . . . . . . . 10
126		c0ex 9655	. . . . . . . . . 10
127	125, 126	ifex 3940	. . . . . . . . 9
128		eqid 2471	. . . . . . . . . 10
129	128	fvmpt2 5972	. . . . . . . . 9 $/\$
130	82, 127, 129	sylancl 675	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
131	77, 122, 130	3eqtrd 2509	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
132	10	ad2antrr 740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
133	15	ad2antrr 740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
134	64	nnred 10646	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
135	11	ad2antrr 740	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
136	135, 12	sylib 201	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
137	136	simprd 470	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
138	132, 66	addge01d 10222	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
139	137, 138	mpbid 215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
140	62	adantr 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
141	140	nnred 10646	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
142		simplrr 779	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
143	133, 141, 142	ltled 9800	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
144		eluzle 11195	. . . . . . . . . . . . . 14
145	144	adantl 473	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
146	133, 141, 134, 143, 145	letrd 9809	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
147	132, 133, 134, 139, 146	letrd 9809	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
148	82, 134	absled 13569	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
149	147, 148	mpbid 215	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
150	149	simpld 466	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
151	149	simprd 470	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
152	134	renegcld 10067	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
153		elicc2 11724	. . . . . . . . . 10 $/\$ $/\$ $/\$
154	152, 134, 153	syl2anc 673	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
155	82, 150, 151, 154	mpbir3and 1213	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
156	155	iftrued 3880	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
157		simpr 468	. . . . . . . . . . . . . . . 16 $/\$
158	157	fveq2d 5883	. . . . . . . . . . . . . . 15 $/\$
159		simpl 464	. . . . . . . . . . . . . . . 16 $/\$
160	159	oveq2d 6324	. . . . . . . . . . . . . . 15 $/\$
161	158, 160	oveq12d 6326	. . . . . . . . . . . . . 14 $/\$
162	161	fveq2d 5883	. . . . . . . . . . . . 13 $/\$
163	162, 160	oveq12d 6326	. . . . . . . . . . . 12 $/\$
164		ovex 6336	. . . . . . . . . . . 12
165	163, 3, 164	ovmpt2a 6446	. . . . . . . . . . 11 $/\$
166	64, 82, 165	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
167	110, 88	nndivred 10680	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
168		flle 12068	. . . . . . . . . . . . 13
169	101, 168	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
170		ledivmul2 10506	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
171	110, 66, 89, 115, 170	syl112anc 1296	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
172	169, 171	mpbird 240	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
173	9	ad2antrr 740	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
174	173	absge0d 13583	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
175	66, 132	addge02d 10223	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
176	174, 175	mpbid 215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
177	66, 133, 134, 176, 146	letrd 9809	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
178	167, 66, 134, 172, 177	letrd 9809	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
179	166, 178	eqbrtrd 4416	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
180	179	iftrued 3880	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
181	180, 166	eqtrd 2505	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
182	131, 156, 181	3eqtrd 2509	. . . . . 6 $/\$ $/\$ $/\$ $/\$
183	119, 65, 182	3brtr4d 4426	. . . . 5 $/\$ $/\$ $/\$ $/\$
184	182, 172	eqbrtrd 4416	. . . . 5 $/\$ $/\$ $/\$ $/\$
185	18, 20, 59, 61, 71, 84, 183, 184	climsqz 13781	. . . 4 $/\$ $/\$ $/\$
186	17, 185	rexlimddv 2875	. . 3 $/\$
187	186	ralrimiva 2809	. 2
188	36	mptex 6152	. . . 4
189	4, 188	eqeltri 2545	. . 3
190		feq1 5720	. . . 4
191		fveq1 5878	. . . . . . 7
192	191	breq2d 4407	. . . . . 6
193		fveq1 5878	. . . . . . 7
194	191, 193	breq12d 4408	. . . . . 6
195	192, 194	anbi12d 725	. . . . 5 $/\$ $/\$
196	195	ralbidv 2829	. . . 4 $/\$ $/\$
197	191	fveq1d 5881	. . . . . . 7
198	197	mpteq2dv 4483	. . . . . 6
199	198	breq1d 4405	. . . . 5
200	199	ralbidv 2829	. . . 4
201	190, 196, 200	3anbi123d 1365	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
202	189, 201	spcev 3127	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
203	5, 7, 187, 202	syl3anc 1292	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wex 1671

wcel 1904

wne 2641

wral 2756

wrex 2757

cvv 3031

cif 3872 class class class wbr 4395

cmpt 4454

cdm 4839

wf 5585

cfv 5589 (class class class)co 6308

cmpt2 6310

cofr 6549

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

cpnf 9690

clt 9693

cle 9694

cmin 9880

cneg 9881

cdiv 10291

cn 10631

c2 10681

cn0 10893

cz 10961

cuz 11182

cico 11662

cicc 11663

cfl 12059

cexp 12310

cabs 13374

cli 13625 MblFncmbf 22651

citg1 22652

c0p 22706

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-ofr 6551 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-seq 12252 df-exp 12311 df-hash 12554 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-clim 13629 df-rlim 13630 df-sum 13830 df-rest 15399 df-topgen 15420 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-top 19998 df-bases 19999 df-topon 20000 df-cmp 20479 df-ovol 22494 df-vol 22496 df-mbf 22656 df-itg1 22657 df-0p 22707

This theorem is referenced by: mbfi1fseq 22758

W3C validator