Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem cvgcmp2lem 7124

Description: Lemma for cvgcmp2 7125.

Hypotheses

Ref	Expression
cvgcmp2.1
cvgcmp2.2
cvgcmp2.3
cvgcmp2.4
cvgcmp2.5
cvgcmp2.6
cvgcmp2.7
cvgcmp2.8
cvgcmp2lem.9
cvgcmp2lem.10
cvgcmp2lem.11

Assertion

Ref	Expression
cvgcmp2lem

Distinct variable groups:   ,   ,,   ,   ,   ,   ,

---

Proof of Theorem cvgcmp2lem

Step	Hyp	Ref	Expression
1		cvgcmp2.3	. . 3
2	1	ser1ref 6277	. 2
3		cvgcmp2.5	. . 3
4	1, 3	ser1mono 6282	. 2
5		cvgcmp2lem.9	. . . . 5
6		cvgcmp2.7	. . . . . . 7
7	2	seq1ublem 6856	. . . . . . 7
8	6, 7	ax-mp 7	. . . . . 6
9	8	suprcli 6016	. . . . 5
10	5, 9	eqeltr 1541	. . . 4
11		cvgcmp2.1	. . . . 5
12		cvgcmp2.2	. . . . . 6
13	12	ser1ref 6277	. . . . 5
14		cvgcmp2.6	. . . . 5
15	11, 13, 14	climfnrcl 7056	. . . 4
16	10, 15	readdcl 5314	. . 3
17	1	ser1recl 6276	. . . . 5
18		cvgcmp2lem.11	. . . . . 6
19	12	ser1recl 6276	. . . . . . 7
20		axaddrcl 5252	. . . . . . . 8
21	10, 20	mpan 694	. . . . . . 7
22	19, 21	syl 10	. . . . . 6
23	18, 22	eqeltrd 1545	. . . . 5
24	16	a1i 8	. . . . 5
25		cvgcmp2.4	. . . . . . . 8
26		cvgcmp2.8	. . . . . . . 8
27	12, 1, 25, 26, 5	ser1cmp2 7121	. . . . . . 7
28	6, 27	mpan2 695	. . . . . 6
29	28, 18	breqtrrd 2636	. . . . 5
30		oprex 3974	. . . . . 6
31		ffnfv 3819	. . . . . . 7
32		cvgcmp2lem.10	. . . . . . 7
33	23	rgen 1695	. . . . . . 7
34	31, 32, 33	mpbir2an 729	. . . . . 6
35	12, 25	ser1mono 6282	. . . . . . . 8
36		leadd2t 5608	. . . . . . . . . 10
37	10, 36	mp3an3 903	. . . . . . . . 9
38	12	ser1recl 6276	. . . . . . . . 9
39		peano2nn 5891	. . . . . . . . . 10
40	12	ser1recl 6276	. . . . . . . . . 10
41	39, 40	syl 10	. . . . . . . . 9
42	37, 38, 41	sylanc 471	. . . . . . . 8
43	35, 42	mpbid 195	. . . . . . 7
44		fveq2 3715	. . . . . . . . 9
45		fveq2 3715	. . . . . . . . . 10
46	45	opreq2d 3967	. . . . . . . . 9
47	44, 46	eqeq12d 1486	. . . . . . . 8
48	47, 18	vtoclga 1848	. . . . . . 7
49		fveq2 3715	. . . . . . . . . 10
50		fveq2 3715	. . . . . . . . . . 11
51	50	opreq2d 3967	. . . . . . . . . 10
52	49, 51	eqeq12d 1486	. . . . . . . . 9
53	52, 18	vtoclga 1848	. . . . . . . 8
54	39, 53	syl 10	. . . . . . 7
55	43, 48, 54	3brtr4d 2640	. . . . . 6
56	10	recn 5294	. . . . . . 7
57	19	recnd 5295	. . . . . . . 8
58	57, 18	jca 288	. . . . . . 7
59	56, 11, 14, 32, 58	climaddc 7076	. . . . . 6
60	30, 34, 55, 59	climub 7098	. . . . 5
61	17, 23, 24, 29, 60	letrd 5507	. . . 4
62	61	rgen 1695	. . 3
63		breq2 2618	. . . . 5
64	63	ralbidv 1660	. . . 4
65	64	rcla4ev 1873	. . 3
66	16, 62, 65	mp2an 696	. 2
67	2, 4, 66	climsup 7099	1

Colors of variables: wff set class

Syntax hints:   wi 3   wb 146   wa 223   w3a 774   wceq