mbfi1fseqlem6 - Metamath Proof Explorer

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

Theorem mbfi1fseqlem6 21862

Description: Lemma for mbfi1fseq 21863. 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 21860	. 2
6	1, 2, 3, 4	mbfi1fseqlem5 21861	. . 3 $/\$ $/\$
7	6	ralrimiva 2878	. 2 $/\$
8		simpr 461	. . . . . . . 8 $/\$
9	8	recnd 9618	. . . . . . 7 $/\$
10	9	abscld 13226	. . . . . 6 $/\$
11	2	ffvelrnda 6019	. . . . . . . 8 $/\$
12		elrege0 11623	. . . . . . . 8 $/\$
13	11, 12	sylib 196	. . . . . . 7 $/\$ $/\$
14	13	simpld 459	. . . . . 6 $/\$
15	10, 14	readdcld 9619	. . . . 5 $/\$
16		arch 10788	. . . . 5
17	15, 16	syl 16	. . . 4 $/\$
18		eqid 2467	. . . . 5
19		nnz 10882	. . . . . 6
20	19	ad2antrl 727	. . . . 5 $/\$ $/\$ $/\$
21		nnuz 11113	. . . . . . . 8
22		1zzd 10891	. . . . . . . 8 $/\$
23		halfcn 10751	. . . . . . . . . 10
24	23	a1i 11	. . . . . . . . 9 $/\$
25		halfre 10750	. . . . . . . . . . . 12
26		0re 9592	. . . . . . . . . . . . 13
27		halfgt0 10752	. . . . . . . . . . . . 13
28	26, 25, 27	ltleii 9703	. . . . . . . . . . . 12
29		absid 13088	. . . . . . . . . . . 12 $/\$
30	25, 28, 29	mp2an 672	. . . . . . . . . . 11
31		halflt1 10753	. . . . . . . . . . 11
32	30, 31	eqbrtri 4466	. . . . . . . . . 10
33	32	a1i 11	. . . . . . . . 9 $/\$
34	24, 33	expcnv 13634	. . . . . . . 8 $/\$
35	14	recnd 9618	. . . . . . . 8 $/\$
36		nnex 10538	. . . . . . . . . 10
37	36	mptex 6129	. . . . . . . . 9
38	37	a1i 11	. . . . . . . 8 $/\$
39		nnnn0 10798	. . . . . . . . . . 11
40	39	adantl 466	. . . . . . . . . 10 $/\$ $/\$
41		oveq2 6290	. . . . . . . . . . 11
42		eqid 2467	. . . . . . . . . . 11
43		ovex 6307	. . . . . . . . . . 11
44	41, 42, 43	fvmpt 5948	. . . . . . . . . 10
45	40, 44	syl 16	. . . . . . . . 9 $/\$ $/\$
46		expcl 12148	. . . . . . . . . 10 $/\$
47	23, 40, 46	sylancr 663	. . . . . . . . 9 $/\$ $/\$
48	45, 47	eqeltrd 2555	. . . . . . . 8 $/\$ $/\$
49	41	oveq2d 6298	. . . . . . . . . . 11
50		eqid 2467	. . . . . . . . . . 11
51		ovex 6307	. . . . . . . . . . 11
52	49, 50, 51	fvmpt 5948	. . . . . . . . . 10
53	52	adantl 466	. . . . . . . . 9 $/\$ $/\$
54	45	oveq2d 6298	. . . . . . . . 9 $/\$ $/\$
55	53, 54	eqtr4d 2511	. . . . . . . 8 $/\$ $/\$
56	21, 22, 34, 35, 38, 48, 55	climsubc2 13420	. . . . . . 7 $/\$
57	35	subid1d 9915	. . . . . . 7 $/\$
58	56, 57	breqtrd 4471	. . . . . 6 $/\$
59	58	adantr 465	. . . . 5 $/\$ $/\$ $/\$
60	36	mptex 6129	. . . . . 6
61	60	a1i 11	. . . . 5 $/\$ $/\$ $/\$
62		simprl 755	. . . . . . . 8 $/\$ $/\$ $/\$
63		eluznn 11148	. . . . . . . 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 12147	. . . . . . . 8 $/\$
69	25, 67, 68	sylancr 663	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
70	66, 69	resubcld 9983	. . . . . 6 $/\$ $/\$ $/\$ $/\$
71	65, 70	eqeltrd 2555	. . . . 5 $/\$ $/\$ $/\$ $/\$
72		fveq2 5864	. . . . . . . . 9
73	72	fveq1d 5866	. . . . . . . 8
74		eqid 2467	. . . . . . . 8
75		fvex 5874	. . . . . . . 8
76	73, 74, 75	fvmpt 5948	. . . . . . 7
77	64, 76	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$
78	5	ad3antrrr 729	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
79	78, 64	ffvelrnd 6020	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
80		i1ff 21818	. . . . . . . 8
81	79, 80	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
82	8	ad2antrr 725	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
83	81, 82	ffvelrnd 6020	. . . . . 6 $/\$ $/\$ $/\$ $/\$
84	77, 83	eqeltrd 2555	. . . . 5 $/\$ $/\$ $/\$ $/\$
85	35	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
86		2nn 10689	. . . . . . . . . . . . . 14
87		nnexpcl 12143	. . . . . . . . . . . . . 14 $/\$
88	86, 67, 87	sylancr 663	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
89	88	nnred 10547	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
90	89	recnd 9618	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	88	nnne0d 10576	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
92	85, 90, 91	divcan4d 10322	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
93	92	eqcomd 2475	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
94		2cnd 10604	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
95		2ne0 10624	. . . . . . . . . . 11
96	95	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
97		eluzelz 11087	. . . . . . . . . . 11
98	97	adantl 466	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
99	94, 96, 98	exprecd 12282	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
100	93, 99	oveq12d 6300	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
101	66, 89	remulcld 9620	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
102	101	recnd 9618	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
103		1cnd 9608	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
104	102, 103, 90, 91	divsubdird 10355	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
105	100, 104	eqtr4d 2511	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
106		fllep1 11902	. . . . . . . . . 10
107	101, 106	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
108		1red 9607	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
109		reflcl 11897	. . . . . . . . . . 11
110	101, 109	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
111	101, 108, 110	lesubaddd 10145	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
112	107, 111	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
113		peano2rem 9882	. . . . . . . . . 10
114	101, 113	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
115	88	nngt0d 10575	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
116		lediv1 10403	. . . . . . . . 9 $/\$ $/\$ $/\$
117	114, 110, 89, 115, 116	syl112anc 1232	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
118	112, 117	mpbid 210	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
119	105, 118	eqbrtrd 4467	. . . . . 6 $/\$ $/\$ $/\$ $/\$
120	1, 2, 3, 4	mbfi1fseqlem2 21858	. . . . . . . . . 10
121	64, 120	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
122	121	fveq1d 5866	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
123		ovex 6307	. . . . . . . . . . 11
124		vex 3116	. . . . . . . . . . 11
125	123, 124	ifex 4008	. . . . . . . . . 10
126		c0ex 9586	. . . . . . . . . 10
127	125, 126	ifex 4008	. . . . . . . . 9
128		eqid 2467	. . . . . . . . . 10
129	128	fvmpt2 5955	. . . . . . . . 9 $/\$
130	82, 127, 129	sylancl 662	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
131	77, 122, 130	3eqtrd 2512	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
132	10	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
133	15	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
134	64	nnred 10547	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
135	11	ad2antrr 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
136	135, 12	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
137	136	simprd 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
138	132, 66	addge01d 10136	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
139	137, 138	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
140	62	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
141	140	nnred 10547	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
142		simplrr 760	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
143	133, 141, 142	ltled 9728	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
144		eluzle 11090	. . . . . . . . . . . . . 14
145	144	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
146	133, 141, 134, 143, 145	letrd 9734	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
147	132, 133, 134, 139, 146	letrd 9734	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
148	82, 134	absled 13221	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
149	147, 148	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
150	149	simpld 459	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
151	149	simprd 463	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
152	134	renegcld 9982	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
153		elicc2 11585	. . . . . . . . . 10 $/\$ $/\$ $/\$
154	152, 134, 153	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
155	82, 150, 151, 154	mpbir3and 1179	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
156		iftrue 3945	. . . . . . . 8
157	155, 156	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
158		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
159	158	fveq2d 5868	. . . . . . . . . . . . . . 15 $/\$
160		simpl 457	. . . . . . . . . . . . . . . 16 $/\$
161	160	oveq2d 6298	. . . . . . . . . . . . . . 15 $/\$
162	159, 161	oveq12d 6300	. . . . . . . . . . . . . 14 $/\$
163	162	fveq2d 5868	. . . . . . . . . . . . 13 $/\$
164	163, 161	oveq12d 6300	. . . . . . . . . . . 12 $/\$
165		ovex 6307	. . . . . . . . . . . 12
166	164, 3, 165	ovmpt2a 6415	. . . . . . . . . . 11 $/\$
167	64, 82, 166	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
168	110, 88	nndivred 10580	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
169		flle 11900	. . . . . . . . . . . . 13
170	101, 169	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
171		ledivmul2 10418	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
172	110, 66, 89, 115, 171	syl112anc 1232	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
173	170, 172	mpbird 232	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
174	9	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
175	174	absge0d 13234	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
176	66, 132	addge02d 10137	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
177	175, 176	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
178	66, 133, 134, 177, 146	letrd 9734	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
179	168, 66, 134, 173, 178	letrd 9734	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
180	167, 179	eqbrtrd 4467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
181		iftrue 3945	. . . . . . . . 9
182	180, 181	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
183	182, 167	eqtrd 2508	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
184	131, 157, 183	3eqtrd 2512	. . . . . 6 $/\$ $/\$ $/\$ $/\$
185	119, 65, 184	3brtr4d 4477	. . . . 5 $/\$ $/\$ $/\$ $/\$
186	184, 173	eqbrtrd 4467	. . . . 5 $/\$ $/\$ $/\$ $/\$
187	18, 20, 59, 61, 71, 84, 185, 186	climsqz 13422	. . . 4 $/\$ $/\$ $/\$
188	17, 187	rexlimddv 2959	. . 3 $/\$
189	188	ralrimiva 2878	. 2
190	36	mptex 6129	. . . 4
191	4, 190	eqeltri 2551	. . 3
192		feq1 5711	. . . 4
193		fveq1 5863	. . . . . . 7
194	193	breq2d 4459	. . . . . 6
195		fveq1 5863	. . . . . . 7
196	193, 195	breq12d 4460	. . . . . 6
197	194, 196	anbi12d 710	. . . . 5 $/\$ $/\$
198	197	ralbidv 2903	. . . 4 $/\$ $/\$
199	193	fveq1d 5866	. . . . . . 7
200	199	mpteq2dv 4534	. . . . . 6
201	200	breq1d 4457	. . . . 5
202	201	ralbidv 2903	. . . 4
203	192, 198, 202	3anbi123d 1299	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
204	191, 203	spcev 3205	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
205	5, 7, 189, 204	syl3anc 1228	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1379

wex 1596

wcel 1767

wne 2662

wral 2814

wrex 2815

cvv 3113

cif 3939 class class class wbr 4447

cmpt 4505

cdm 4999

wf 5582

cfv 5586 (class class class)co 6282

cmpt2 6284

cofr 6521

cc 9486

cr 9487

cc0 9488

c1 9489

caddc 9491

cmul 9493

cpnf 9621

clt 9624

cle 9625

cmin 9801

cneg 9802

cdiv 10202

cn 10532

c2 10581

cn0 10791

cz 10860

cuz 11078

cico 11527

cicc 11528

cfl 11891

cexp 12130

cabs 13026

cli 13266 MblFncmbf 21758

citg1 21759

c0p 21811

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-ofr 6523 df-om 6679 df-1st 6781 df-2nd 6782 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-er 7308 df-map 7419 df-pm 7420 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-fi 7867 df-sup 7897 df-oi 7931 df-card 8316 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-n0 10792 df-z 10861 df-uz 11079 df-q 11179 df-rp 11217 df-xneg 11314 df-xadd 11315 df-xmul 11316 df-ioo 11529 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-fl 11893 df-seq 12072 df-exp 12131 df-hash 12370 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-clim 13270 df-rlim 13271 df-sum 13468 df-rest 14674 df-topgen 14695 df-psmet 18182 df-xmet 18183 df-met 18184 df-bl 18185 df-mopn 18186 df-top 19166 df-bases 19168 df-topon 19169 df-cmp 19653 df-ovol 21611 df-vol 21612 df-mbf 21763 df-itg1 21764 df-0p 21812

This theorem is referenced by: mbfi1fseq 21863

W3C validator