Theorem ser1cmp 7174

Description: Comparison of partial sums of two infinite series of reals.

Hypotheses

Ref	Expression
ser1cmp.1	|- F:NN-->RR
ser1cmp.2	|- G:NN-->RR
ser1cmp.3	|- (x e. NN -> (G` x) <_ (F` x))

Assertion

Ref	Expression
ser1cmp	|- (A e. NN -> (( + seq1 G)` A) <_ (( + seq1 F)` A))

Distinct variable groups:   x,F   x,G

Proof of Theorem ser1cmp

Step	Hyp	Ref	Expression
1		fveq2 3724	. . 3 |- (y = 1 -> (( + seq1 G)` y) = (( + seq1 G)` 1))
2		fveq2 3724	. . 3 |- (y = 1 -> (( + seq1 F)` y) = (( + seq1 F)` 1))
3	1, 2	breq12d 2631	. 2 |- (y = 1 -> ((( + seq1 G)` y) <_ (( + seq1 F)` y) <-> (( + seq1 G)` 1) <_ (( + seq1 F)` 1)))
4		fveq2 3724	. . 3 |- (y = z -> (( + seq1 G)` y) = (( + seq1 G)` z))
5		fveq2 3724	. . 3 |- (y = z -> (( + seq1 F)` y) = (( + seq1 F)` z))
6	4, 5	breq12d 2631	. 2 |- (y = z -> ((( + seq1 G)` y) <_ (( + seq1 F)` y) <-> (( + seq1 G)` z) <_ (( + seq1 F)` z)))
7		fveq2 3724	. . 3 |- (y = (z + 1) -> (( + seq1 G)` y) = (( + seq1 G)` (z + 1)))
8		fveq2 3724	. . 3 |- (y = (z + 1) -> (( + seq1 F)` y) = (( + seq1 F)` (z + 1)))
9	7, 8	breq12d 2631	. 2 |- (y = (z + 1) -> ((( + seq1 G)` y) <_ (( + seq1 F)` y) <-> (( + seq1 G)` (z + 1)) <_ (( + seq1 F)` (z + 1))))
10		fveq2 3724	. . 3 |- (y = A -> (( + seq1 G)` y) = (( + seq1 G)` A))
11		fveq2 3724	. . 3 |- (y = A -> (( + seq1 F)` y) = (( + seq1 F)` A))
12	10, 11	breq12d 2631	. 2 |- (y = A -> ((( + seq1 G)` y) <_ (( + seq1 F)` y) <-> (( + seq1 G)` A) <_ (( + seq1 F)` A)))
13		1nn 5934	. . . 4 |- 1 e. NN
14		fveq2 3724	. . . . . 6 |- (x = 1 -> (G` x) = (G` 1))
15		fveq2 3724	. . . . . 6 |- (x = 1 -> (F` x) = (F` 1))
16	14, 15	breq12d 2631	. . . . 5 |- (x = 1 -> ((G` x) <_ (F` x) <-> (G` 1) <_ (F` 1)))
17		ser1cmp.3	. . . . 5 |- (x e. NN -> (G` x) <_ (F` x))
18	16, 17	vtoclga 1852	. . . 4 |- (1 e. NN -> (G` 1) <_ (F` 1))
19	13, 18	ax-mp 7	. . 3 |- (G` 1) <_ (F` 1)
20		addex 5317	. . . 4 |- + e. V
21		ser1cmp.2	. . . . 5 |- G:NN-->RR
22		nnex 5933	. . . . 5 |- NN e. V
23		fex 3652	. . . . 5 |- ((G:NN-->RR /\ NN e. V) -> G e. V)
24	21, 22, 23	mp2an 697	. . . 4 |- G e. V
25	20, 24	seq11 6317	. . 3 |- (( + seq1 G)` 1) = (G` 1)
26		ser1cmp.1	. . . . 5 |- F:NN-->RR
27		fex 3652	. . . . 5 |- ((F:NN-->RR /\ NN e. V) -> F e. V)
28	26, 22, 27	mp2an 697	. . . 4 |- F e. V
29	20, 28	seq11 6317	. . 3 |- (( + seq1 F)` 1) = (F` 1)
30	19, 25, 29	3brtr4 2643	. 2 |- (( + seq1 G)` 1) <_ (( + seq1 F)` 1)
31		axaddrcl 5272	. . . . . . 7 |- (((( + seq1 G)` z) e. RR /\ (G` (z + 1)) e. RR) -> ((( + seq1 G)` z) + (G` (z + 1))) e. RR)
32	21	ser1recl 6331	. . . . . . 7 |- (z e. NN -> (( + seq1 G)` z) e. RR)
33		peano2nn 5935	. . . . . . . 8 |- (z e. NN -> (z + 1) e. NN)
34	21	ffvelrni 3815	. . . . . . . 8 |- ((z + 1) e. NN -> (G` (z + 1)) e. RR)
35	33, 34	syl 10	. . . . . . 7 |- (z e. NN -> (G` (z + 1)) e. RR)
36	31, 32, 35	sylanc 471	. . . . . 6 |- (z e. NN -> ((( + seq1 G)` z) + (G` (z + 1))) e. RR)
37	36	adantr 389	. . . . 5 |- ((z e. NN /\ (( + seq1 G)` z) <_ (( + seq1 F)` z)) -> ((( + seq1 G)` z) + (G` (z + 1))) e. RR)
38		axaddrcl 5272	. . . . . . 7 |- (((( + seq1 F)` z) e. RR /\ (G` (z + 1)) e. RR) -> ((( + seq1 F)` z) + (G` (z + 1))) e. RR)
39	26	ser1recl 6331	. . . . . . 7 |- (z e. NN -> (( + seq1 F)` z) e. RR)
40	38, 39, 35	sylanc 471	. . . . . 6 |- (z e. NN -> ((( + seq1 F)` z) + (G` (z + 1))) e. RR)
41	40	adantr 389	. . . . 5 |- ((z e. NN /\ (( + seq1 G)` z) <_ (( + seq1 F)` z)) -> ((( + seq1 F)` z) + (G` (z + 1))) e. RR)
42		axaddrcl 5272	. . . . . . 7 |- (((( + seq1 F)` z) e. RR /\ (F` (z + 1)) e. RR) -> ((( + seq1 F)` z) + (F` (z + 1))) e. RR)
43	26	ffvelrni 3815	. . . . . . . 8 |- ((z + 1) e. NN -> (F` (z + 1)) e. RR)
44	33, 43	syl 10	. . . . . . 7 |- (z e. NN -> (F` (z + 1)) e. RR)
45	42, 39, 44	sylanc 471	. . . . . 6 |- (z e. NN -> ((( + seq1 F)` z) + (F` (z + 1))) e. RR)
46	45	adantr 389	. . . . 5 |- ((z e. NN /\ (( + seq1 G)` z) <_ (( + seq1 F)` z)) -> ((( + seq1 F)` z) + (F` (z + 1))) e. RR)
47		leadd1t 5625	. . . . . . 7 |- (((( + seq1 G)` z) e. RR /\ (( + seq1 F)` z) e. RR /\ (G` (z + 1)) e. RR) -> ((( + seq1 G)` z) <_ (( + seq1 F)` z) <-> ((( + seq1 G)` z) + (G` (z + 1))) <_ ((( + seq1 F)` z) + (G` (z + 1)))))
48	47, 32, 39, 35	syl3anc 858	. . . . . 6 |- (z e. NN -> ((( + seq1 G)` z) <_ (( + seq1 F)` z) <-> ((( + seq1 G)` z) + (G` (z + 1))) <_ ((( + seq1 F)` z) + (G` (z + 1)))))
49	48	biimpa 416	. . . . 5 |- ((z e. NN /\ (( + seq1 G)` z) <_ (( + seq1 F)` z)) -> ((( + seq1 G)` z) + (G` (z + 1))) <_ ((( + seq1 F)` z) + (G` (z + 1))))
50		fveq2 3724	. . . . . . . . . 10 |- (x = (z + 1) -> (G` x) = (G` (z + 1)))
51		fveq2 3724	. . . . . . . . . 10 |- (x = (z + 1) -> (F` x) = (F` (z + 1)))
52	50, 51	breq12d 2631	. . . . . . . . 9 |- (x = (z + 1) -> ((G` x) <_ (F` x) <-> (G` (z + 1)) <_ (F` (z + 1))))
53	52, 17	vtoclga 1852	. . . . . . . 8 |- ((z + 1) e. NN -> (G` (z + 1)) <_ (F` (z + 1)))
54	33, 53	syl 10	. . . . . . 7 |- (z e. NN -> (G` (z + 1)) <_ (F` (z + 1)))
55		leadd2t 5626	. . . . . . . 8 |- (((G` (z + 1)) e. RR /\ (F` (z + 1)) e. RR /\ (( + seq1 F)` z) e. RR) -> ((G` (z + 1)) <_ (F` (z + 1)) <-> ((( + seq1 F)` z) + (G` (z + 1))) <_ ((( + seq1 F)` z) + (F` (z + 1)))))
56	55, 35, 44, 39	syl3anc 858	. . . . . . 7 |- (z e. NN -> ((G` (z + 1)) <_ (F` (z + 1)) <-> ((( + seq1 F)` z) + (G` (z + 1))) <_ ((( + seq1 F)` z) + (F` (z + 1)))))
57	54, 56	mpbid 195	. . . . . 6 |- (z e. NN -> ((( + seq1 F)` z) + (G` (z + 1))) <_ ((( + seq1 F)` z) + (F` (z + 1))))
58	57	adantr 389	. . . . 5 |- ((z e. NN /\ (( + seq1 G)` z) <_ (( + seq1 F)` z)) -> ((( + seq1 F)` z) + (G` (z + 1))) <_ ((( + seq1 F)` z) + (F` (z + 1))))
59	37, 41, 46, 49, 58	letrd 5526	. . . 4 |- ((z e. NN /\ (( + seq1 G)` z) <_ (( + seq1 F)` z)) -> ((( + seq1 G)` z) + (G` (z + 1))) <_ ((( + seq1 F)` z) + (F` (z +