Theorem ser1cmp2 7121

Description: Comparison of partial sums of two infinite series of reals that excludes an initial segment.

Hypotheses

Ref	Expression
ser1cmp2.1	|- F:NN-->RR
ser1cmp2.2	|- G:NN-->RR
ser1cmp2.3	|- (x e. NN -> 0 <_ (F` x))
ser1cmp2.4	|- ((x e. NN /\ B < x) -> (G` x) <_ (F` x))
ser1cmp2.5	|- S = sup(ran (( + seq1 G) |` {y e. NN | y <_ B}), RR, < )

Assertion

Ref	Expression
ser1cmp2	|- ((A e. NN /\ B e. NN) -> (( + seq1 G)` A) <_ (S + (( + seq1 F)` A)))

Distinct variable groups:   x,y,B   x,F   x,G

Proof of Theorem ser1cmp2

Step	Hyp	Ref	Expression
1		fveq2 3715	. . . . 5 |- (z = 1 -> (( + seq1 G)` z) = (( + seq1 G)` 1))
2		fveq2 3715	. . . . . 6 |- (z = 1 -> (( + seq1 F)` z) = (( + seq1 F)` 1))
3	2	opreq2d 3967	. . . . 5 |- (z = 1 -> (S + (( + seq1 F)` z)) = (S + (( + seq1 F)` 1)))
4	1, 3	breq12d 2626	. . . 4 |- (z = 1 -> ((( + seq1 G)` z) <_ (S + (( + seq1 F)` z)) <-> (( + seq1 G)` 1) <_ (S + (( + seq1 F)` 1))))
5	4	imbi2d 611	. . 3 |- (z = 1 -> ((B e. NN -> (( + seq1 G)` z) <_ (S + (( + seq1 F)` z))) <-> (B e. NN -> (( + seq1 G)` 1) <_ (S + (( + seq1 F)` 1)))))
6		fveq2 3715	. . . . 5 |- (z = w -> (( + seq1 G)` z) = (( + seq1 G)` w))
7		fveq2 3715	. . . . . 6 |- (z = w -> (( + seq1 F)` z) = (( + seq1 F)` w))
8	7	opreq2d 3967	. . . . 5 |- (z = w -> (S + (( + seq1 F)` z)) = (S + (( + seq1 F)` w)))
9	6, 8	breq12d 2626	. . . 4 |- (z = w -> ((( + seq1 G)` z) <_ (S + (( + seq1 F)` z)) <-> (( + seq1 G)` w) <_ (S + (( + seq1 F)` w))))
10	9	imbi2d 611	. . 3 |- (z = w -> ((B e. NN -> (( + seq1 G)` z) <_ (S + (( + seq1 F)` z))) <-> (B e. NN -> (( + seq1 G)` w) <_ (S + (( + seq1 F)` w)))))
11		fveq2 3715	. . . . 5 |- (z = (w + 1) -> (( + seq1 G)` z) = (( + seq1 G)` (w + 1)))
12		fveq2 3715	. . . . . 6 |- (z = (w + 1) -> (( + seq1 F)` z) = (( + seq1 F)` (w + 1)))
13	12	opreq2d 3967	. . . . 5 |- (z = (w + 1) -> (S + (( + seq1 F)` z)) = (S + (( + seq1 F)` (w + 1))))
14	11, 13	breq12d 2626	. . . 4 |- (z = (w + 1) -> ((( + seq1 G)` z) <_ (S + (( + seq1 F)` z)) <-> (( + seq1 G)` (w + 1)) <_ (S + (( + seq1 F)` (w + 1)))))
15	14	imbi2d 611	. . 3 |- (z = (w + 1) -> ((B e. NN -> (( + seq1 G)` z) <_ (S + (( + seq1 F)` z))) <-> (B e. NN -> (( + seq1 G)` (w + 1)) <_ (S + (( + seq1 F)` (w + 1))))))
16		fveq2 3715	. . . . 5 |- (z = A -> (( + seq1 G)` z) = (( + seq1 G)` A))
17		fveq2 3715	. . . . . 6 |- (z = A -> (( + seq1 F)` z) = (( + seq1 F)` A))
18	17	opreq2d 3967	. . . . 5 |- (z = A -> (S + (( + seq1 F)` z)) = (S + (( + seq1 F)` A)))
19	16, 18	breq12d 2626	. . . 4 |- (z = A -> ((( + seq1 G)` z) <_ (S + (( + seq1 F)` z)) <-> (( + seq1 G)` A) <_ (S + (( + seq1 F)` A))))
20	19	imbi2d 611	. . 3 |- (z = A -> ((B e. NN -> (( + seq1 G)` z) <_ (S + (( + seq1 F)` z))) <-> (B e. NN -> (( + seq1 G)` A) <_ (S + (( + seq1 F)` A)))))
21		nnge1t 5899	. . . 4 |- (B e. NN -> 1 <_ B)
22		1nn 5890	. . . . 5 |- 1 e. NN
23		ser1cmp2.1	. . . . . 6 |- F:NN-->RR
24		ser1cmp2.2	. . . . . 6 |- G:NN-->RR
25		ser1cmp2.3	. . . . . 6 |- (x e. NN -> 0 <_ (F` x))
26		ser1cmp2.4	. . . . . 6 |- ((x e. NN /\ B < x) -> (G` x) <_ (F` x))
27		ser1cmp2.5	. . . . . 6 |- S = sup(ran (( + seq1 G) |` {y e. NN | y <_ B}), RR, < )
28	23, 24, 25, 26, 27	ser1cmp2lem 7120	. . . . 5 |- ((1 e. NN /\ B e. NN) -> (1 <_ B -> (( + seq1 G)` 1) <_ (S + (( + seq1 F)` 1))))
29	22, 28	mpan 694	. . . 4 |- (B e. NN -> (1 <_ B -> (( + seq1 G)` 1) <_ (S + (( + seq1 F)` 1))))
30	21, 29	mpd 26	. . 3 |- (B e. NN -> (( + seq1 G)` 1) <_ (S + (( + seq1 F)` 1)))
31		lelttrit 5604	. . . . . . 7 |- (((w + 1) e. RR /\ B e. RR) -> ((w + 1) <_ B \/ B < (w + 1)))
32		peano2nn 5891	. . . . . . . 8 |- (w e. NN -> (w + 1) e. NN)
33		nnret 5885	. . . . . . . 8 |- ((w + 1) e. NN -> (w + 1) e. RR)
34	32, 33	syl 10	. . . . . . 7 |- (w e. NN -> (w + 1) e. RR)
35		nnret 5885	. . . . . . 7 |- (B e. NN -> B e. RR)
36	31, 34, 35	syl2an 454	. . . . . 6 |- ((w e. NN /\ B e. NN) -> ((w + 1) <_ B \/ B < (w + 1)))
37	23, 24, 25, 26, 27	ser1cmp2lem 7120	. . . . . . . . 9 |- (((w + 1) e. NN /\ B e. NN) -> ((w + 1) <_ B -> (( + seq1 G)` (w + 1)) <_ (S + (( + seq1 F)` (w + 1)))))
38	37, 32	sylan 448	. . . . . . . 8 |- ((w e. NN /\ B e. NN) -> ((w + 1) <_ B -> (( + seq1 G)` (w + 1)) <_ (S + (( + seq1 F)` (w + 1)))))
39	38	a1dd 42	. . . . . . 7 |- ((w e. NN /\ B e. NN) -> ((w + 1) <_ B -> ((( + seq1 G)` w) <_ (S + (( + seq1 F)` w)) -> (( + seq1 G)` (w + 1)) <_ (S + (( + seq1 F)` (w + 1))))))
40		axaddrcl 5252	. . . . . . . . . . . . . 14 |- (((( + seq1 G)` w) e. RR /\ (G` (w + 1)) e. RR) -> ((( + seq1 G)` w) + (G` (w + 1))) e. RR)
41	24	ser1recl 6276	. . . . . . . . . . . . . 14 |- (w e. NN -> (( + seq1 G)` w) e. RR)
42	24	ffvelrni 3806	. . . . . . . . . . . . . . 15 |- ((w + 1) e. NN -> (G` (w + 1)) e. RR)
43	32, 42	syl 10	. . . . . . . . . . . . . 14 |- (w e. NN -> (G` (w + 1)) e. RR)
44	40, 41, 43	sylanc 471	. . . . . . . . . . . . 13 |- (w e. NN -> ((( + seq1 G)` w) + (G` (w + 1))) e. RR)
45	44	ad2antrr 404	. . . . . . . . . . . 12 |- (((w e. NN /\ (B e. NN /\ B < (w + 1))) /\ (( + seq1 G)` w) <_ (S + (( + seq1 F)` w))) -> ((( + seq1 G)` w) + (G` (w + 1))) e. RR)
46		axaddrcl 5252	. . . . . . . . . . . . . . 15 |- (((S + (( + seq1 F)` w)) e. RR /\ (G` (w + 1)) e. RR) -> ((S + (( + seq1 F)` w)) + (G` (w + 1))) e. RR)
47		axaddrcl 5252	. . . . . . . . . . . . . . . . 17 |- ((S e. RR /\ (( + seq1 F)` w) e. RR) -> (S + (( + seq1 F)` w)) e. RR)
48	24	ser1ref 6277	. . . . . . . . . . . . . . . . . . . 20 |- ( + seq1 G):NN-->RR
49	48	seq1ublem 6856	. . . . . . . . . . . . . . . . . . 19 |- (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))
50		suprcl 6010	. . . . . . . . . . . . . . . . . . 19 |- ((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) -> sup(ran (( + seq1 G) |` {y e. NN | y <_ B}), RR, < ) e. RR)
51	49, 50	syl 10	. . . . . . . . . . . . . . . . . 18 |- (B e. NN -> sup(ran (( + seq1 G) |` {y e. NN | y <_ B}), RR, < )