Theorem cvgcmp2lem 7180

Description: Lemma for cvgcmp2 7181.

Hypotheses

Ref	Expression
cvgcmp2.1	|- A e. V
cvgcmp2.2	|- F:NN-->RR
cvgcmp2.3	|- G:NN-->RR
cvgcmp2.4	|- (x e. NN -> 0 <_ (F` x))
cvgcmp2.5	|- (x e. NN -> 0 <_ (G` x))
cvgcmp2.6	|- ( + seq1 F) ~~> A
cvgcmp2.7	|- B e. NN
cvgcmp2.8	|- ((x e. NN /\ B < x) -> (G` x) <_ (F` x))
cvgcmp2lem.9	|- S = sup(ran (( + seq1 G) |` {y e. NN | y <_ B}), RR, < )
cvgcmp2lem.10	|- H Fn NN
cvgcmp2lem.11	|- (x e. NN -> (H` x) = (S + (( + seq1 F)` x)))

Assertion

Ref	Expression
cvgcmp2lem	|- ( + seq1 G) ~~> sup(ran ( + seq1 G), RR, < )

Distinct variable groups:   x,A   x,y,B   x,F   x,G   x,S   x,H

Proof of Theorem cvgcmp2lem

Step	Hyp	Ref	Expression
1		cvgcmp2.3	. . 3 |- G:NN-->RR
2	1	ser1ref 6332	. 2 |- ( + seq1 G):NN-->RR
3		cvgcmp2.5	. . 3 |- (x e. NN -> 0 <_ (G` x))
4	1, 3	ser1mono 6337	. 2 |- (x e. NN -> (( + seq1 G)` x) <_ (( + seq1 G)` (x + 1)))
5		cvgcmp2lem.9	. . . . 5 |- S = sup(ran (( + seq1 G) |` {y e. NN | y <_ B}), RR, < )
6		cvgcmp2.7	. . . . . . 7 |- B e. NN
7	2	seq1ublem 6911	. . . . . . 7 |- (B e. NN -> (ran (( + seq1 G) |` {y e. NN | y <_ B}) (_ RR /\ ran (( + seq1 G) |` {y e. NN | y <_ B}) =/= (/) /\ E.z e. RR A.w e. ran (( + seq1 G) |` {y e. NN | y <_ B})w <_ z))
8	6, 7	ax-mp 7	. . . . . 6 |- (ran (( + seq1 G) |` {y e. NN | y <_ B}) (_ RR /\ ran (( + seq1 G) |` {y e. NN | y <_ B}) =/= (/) /\ E.z e. RR A.w e. ran (( + seq1 G) |` {y e. NN | y <_ B})w <_ z)
9	8	suprcli 6061	. . . . 5 |- sup(ran (( + seq1 G) |` {y e. NN | y <_ B}), RR, < ) e. RR
10	5, 9	eqeltr 1544	. . . 4 |- S e. RR
11		cvgcmp2.1	. . . . 5 |- A e. V
12		cvgcmp2.2	. . . . . 6 |- F:NN-->RR
13	12	ser1ref 6332	. . . . 5 |- ( + seq1 F):NN-->RR
14		cvgcmp2.6	. . . . 5 |- ( + seq1 F) ~~> A
15	11, 13, 14	climfnrcl 7111	. . . 4 |- A e. RR
16	10, 15	readdcl 5334	. . 3 |- (S + A) e. RR
17	1	ser1recl 6331	. . . . 5 |- (x e. NN -> (( + seq1 G)` x) e. RR)
18		cvgcmp2lem.11	. . . . . 6 |- (x e. NN -> (H` x) = (S + (( + seq1 F)` x)))
19	12	ser1recl 6331	. . . . . . 7 |- (x e. NN -> (( + seq1 F)` x) e. RR)
20		axaddrcl 5272	. . . . . . . 8 |- ((S e. RR /\ (( + seq1 F)` x) e. RR) -> (S + (( + seq1 F)` x)) e. RR)
21	10, 20	mpan 695	. . . . . . 7 |- ((( + seq1 F)` x) e. RR -> (S + (( + seq1 F)` x)) e. RR)
22	19, 21	syl 10	. . . . . 6 |- (x e. NN -> (S + (( + seq1 F)` x)) e. RR)
23	18, 22	eqeltrd 1548	. . . . 5 |- (x e. NN -> (H` x) e. RR)
24	16	a1i 8	. . . . 5 |- (x e. NN -> (S + A) e. RR)
25		cvgcmp2.4	. . . . . . . 8 |- (x e. NN -> 0 <_ (F` x))
26		cvgcmp2.8	. . . . . . . 8 |- ((x e. NN /\ B < x) -> (G` x) <_ (F` x))
27	12, 1, 25, 26, 5	ser1cmp2 7177	. . . . . . 7 |- ((x e. NN /\ B e. NN) -> (( + seq1 G)` x) <_ (S + (( + seq1 F)` x)))
28	6, 27	mpan2 696	. . . . . 6 |- (x e. NN -> (( + seq1 G)` x) <_ (S + (( + seq1 F)` x)))
29	28, 18	breqtrrd 2641	. . . . 5 |- (x e. NN -> (( + seq1 G)` x) <_ (H` x))
30		oprex 3983	. . . . . 6 |- (S + A) e. V
31		ffnfv 3828	. . . . . . 7 |- (H:NN-->RR <-> (H Fn NN /\ A.x e. NN (H` x) e. RR))
32		cvgcmp2lem.10	. . . . . . 7 |- H Fn NN
33	23	rgen 1698	. . . . . . 7 |- A.x e. NN (H` x) e. RR
34	31, 32, 33	mpbir2an 730	. . . . . 6 |- H:NN-->RR
35	12, 25	ser1mono 6337	. . . . . . . 8 |- (z e. NN -> (( + seq1 F)` z) <_ (( + seq1 F)` (z + 1)))
36		leadd2t 5626	. . . . . . . . . 10 |- (((( + seq1 F)` z) e. RR /\ (( + seq1 F)` (z + 1)) e. RR /\ S e. RR) -> ((( + seq1 F)` z) <_ (( + seq1 F)` (z + 1)) <-> (S + (( + seq1 F)` z)) <_ (S + (( + seq1 F)` (z + 1)))))
37	10, 36	mp3an3 905	. . . . . . . . 9 |- (((( + seq1 F)` z) e. RR /\ (( + seq1 F)` (z + 1)) e. RR) -> ((( + seq1 F)` z) <_ (( + seq1 F)` (z + 1)) <-> (S + (( + seq1 F)` z)) <_ (S + (( + seq1 F)` (z + 1)))))
38	12	ser1recl 6331	. . . . . . . . 9 |- (z e. NN -> (( + seq1 F)` z) e. RR)
39		peano2nn 5935	. . . . . . . . . 10 |- (z e. NN -> (z + 1) e. NN)
40	12	ser1recl 6331	. . . . . . . . . 10 |- ((z + 1) e. NN -> (( + seq1 F)` (z + 1)) e. RR)
41	39, 40	syl 10	. . . . . . . . 9 |- (z e. NN -> (( + seq1 F)` (z + 1)) e. RR)
42	37, 38, 41	sylanc 471	. . . . . . . 8 |- (z e. NN -> ((( + seq1 F)` z) <_ (( + seq1 F)` (z + 1)) <-> (S + (( + seq1 F)` z)) <_ (S + (( + seq1 F)` (z + 1)))))
43	35, 42	mpbid 195	. . . . . . 7 |- (z e. NN -> (S + (( + seq1 F)` z)) <_ (S + (( + seq1 F)` (z + 1))))
44		fveq2 3724	. . . . . . . . 9 |- (x = z -> (H` x) = (H` z))
45		fveq2 3724	. . . . . . . . . 10 |- (x = z -> (( + seq1 F)` x) = (( + seq1 F)` z))
46	45	opreq2d 3976	. . . . . . . . 9 |- (x = z -> (S + (( + seq1 F)` x)) = (S + (( + seq1 F)` z)))
47	44, 46	eqeq12d 1489	. . . . . . . 8 |- (x = z -> ((H` x) = (S + (( + seq1 F)` x)) <-> (H` z) = (S + (( + seq1 F)` z))))
48	47, 18	vtoclga 1852	. . . . . . 7 |- (z e. NN -> (H` z) = (S + (( + seq1 F)` z)))
49		fveq2 3724	. . . . . . . . . 10 |- (x = (z + 1) -> (H` x) = (H` (z + 1)))
50		fveq2 3724	. . . . . . . . . . 11 |- (x = (z + 1) -> (( + seq1 F)` x) = (( + seq1 F)` (z + 1)))
51	50	opreq2d 3976	. . . . . . . . . 10 |- (x = (z + 1) -> (S + (( + seq1 F)` x)) = (S + (( + seq1 F)` (z + 1))))
52	49, 51	eqeq12d 1489	. . . . . . . . 9 |- (x = (z + 1) -> ((H` x) = (S + (( + seq1 F)` x)) <-> (H` (z + 1)) = (S + (( + seq1 F)` (z + 1)))))
53	52, 18	vtoclga 1852	. . . . . . . 8 |- ((z + 1) e. NN -> (H` (z + 1)) = (S + (( + seq1 F)` (z + 1))))
54	39, 53	syl 10	. . . . . . 7 |- (z e. NN -> (H` (z + 1)) = (S + (( + seq1 F)` (z + 1))))
55	43, 48, 54	3brtr4d 2645	. . . . . 6 |- (z e. NN -> (H` z) <_ (H` (z + 1)))
56	10	recn 5314	. . . . . . 7 |- S e. CC
57	19	recnd 5315	. . . . . . . 8 |- (x e. NN -> (( + seq1 F)` x) e. CC)
58	57, 18	jca 288	. . . . . . 7 |- (x e. NN -> ((( + seq1 F)` x) e. CC /\ (H` x) = (S + (( + seq1 F)` x))))
59	56, 11, 14, 32, 58	climaddc 7132	. . . . . 6 |- H ~~> (S + A)
60	30, 34, 55, 59	climub 7154	. . . . 5 |- (x e. NN -> (H` x) <_ (S + A))
61	17, 23, 24, 29, 60	letrd 5526	. . . 4 |- (x e. NN -> (( + seq1 G)` x) <_ (S + A))
62	61	rgen 1698	. . 3 |- A.x e. NN (( + seq1 G)` x) <_ (S + A)
63		breq2 2623	. . . . 5 |- (z = (S + A) -> ((( + seq1 G)` x) <_ z <-> (( + seq1 G)` x) <_ (S + A)))
64	63	ralbidv 1663	. . . 4 |- (z = (S + A) -> (A.x e. NN (( + seq1 G)` x) <_ z <-> A.x e. NN (( + seq1 G)` x) <_ (S + A)))
65	64	rcla4ev 1877	. . 3 |- (((S + A) e. RR /\ A.x e. NN (( + seq1 G)` x) <_ (S + A)) -> E.z e. RR A.x e. NN (( + seq1 G)` x) <_ z)
66	16, 62, 65	mp2an 697	. 2 |- E.z e. RR A.x e. NN (( + seq1 G)` x) <_ z
67	2, 4, 66	climsup 7155	1 |- ( + seq1 G) ~~> sup(ran ( + seq1 G), RR, < )

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 775   = <