Theorem climserzle 7147

Description: The partial sums of a converging infinite series with nonnegative terms are bounded by its limit.

Hypotheses

Ref	Expression
climserzle.1	|- F e. V
climserzle.2	|- A e. V
climserzle.3	|- (<.M, + >. seq F) ~~> A
climserzle.4	|- F:(ZZ>` M)-->RR

Assertion

Ref	Expression
climserzle	|- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)0 <_ (F` k)) -> ((<.M, + >. seq F)` N) <_ A)

Distinct variable groups:   k,F   k,M   k,N

Proof of Theorem climserzle

Step	Hyp	Ref	Expression
1		oprex 3983	. . . 4 |- (A - ((<.M, + >. seq F)` N)) e. V
2	1	climge0 7112	. . 3 |- (((N + 1) e. ZZ /\ (<.(N + 1), + >. seq F) ~~> (A - ((<.M, + >. seq F)` N)) /\ A.j e. (ZZ>` (N + 1))(((<.(N + 1), + >. seq F)` j) e. RR /\ 0 <_ ((<.(N + 1), + >. seq F)` j))) -> 0 <_ (A - ((<.M, + >. seq F)` N)))
3		eluzelz 6423	. . . . 5 |- (N e. (ZZ>` M) -> N e. ZZ)
4	3	peano2zd 6167	. . . 4 |- (N e. (ZZ>` M) -> (N + 1) e. ZZ)
5	4	adantr 389	. . 3 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)0 <_ (F` k)) -> (N + 1) e. ZZ)
6		climserzle.1	. . . . 5 |- F e. V
7		climserzle.2	. . . . 5 |- A e. V
8		climserzle.3	. . . . 5 |- (<.M, + >. seq F) ~~> A
9		climserzle.4	. . . . . 6 |- F:(ZZ>` M)-->RR
10		axresscn 5268	. . . . . 6 |- RR (_ CC
11		fss 3635	. . . . . 6 |- ((F:(ZZ>` M)-->RR /\ RR (_ CC) -> F:(ZZ>` M)-->CC)
12	9, 10, 11	mp2an 697	. . . . 5 |- F:(ZZ>` M)-->CC
13	6, 7, 8, 12	clim2serz 7145	. . . 4 |- (N e. (ZZ>` M) -> (<.(N + 1), + >. seq F) ~~> (A - ((<.M, + >. seq F)` N)))
14	13	adantr 389	. . 3 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)0 <_ (F` k)) -> (<.(N + 1), + >. seq F) ~~> (A - ((<.M, + >. seq F)` N)))
15	6	serzreclt 7050	. . . . . . 7 |- ((j e. (ZZ>` (N + 1)) /\ A.k e. ((N + 1)...j)(F` k) e. RR) -> ((<.(N + 1), + >. seq F)` j) e. RR)
16		pm3.27 323	. . . . . . 7 |- ((N e. (ZZ>` M) /\ j e. (ZZ>` (N + 1))) -> j e. (ZZ>` (N + 1)))
17		uztrn 6428	. . . . . . . . . . . 12 |- ((k e. (ZZ>` (N + 1)) /\ (N + 1) e. (ZZ>` M)) -> k e. (ZZ>` M))
18	17	ancoms 436	. . . . . . . . . . 11 |- (((N + 1) e. (ZZ>` M) /\ k e. (ZZ>` (N + 1))) -> k e. (ZZ>` M))
19		peano2uz 6447	. . . . . . . . . . 11 |- (N e. (ZZ>` M) -> (N + 1) e. (ZZ>` M))
20		elfzuzt 6488	. . . . . . . . . . 11 |- (k e. ((N + 1)...j) -> k e. (ZZ>` (N + 1)))
21	18, 19, 20	syl2an 454	. . . . . . . . . 10 |- ((N e. (ZZ>` M) /\ k e. ((N + 1)...j)) -> k e. (ZZ>` M))
22	9	ffvelrni 3815	. . . . . . . . . 10 |- (k e. (ZZ>` M) -> (F` k) e. RR)
23	21, 22	syl 10	. . . . . . . . 9 |- ((N e. (ZZ>` M) /\ k e. ((N + 1)...j)) -> (F` k) e. RR)
24	23	r19.21aiva 1714	. . . . . . . 8 |- (N e. (ZZ>` M) -> A.k e. ((N + 1)...j)(F` k) e. RR)
25	24	adantr 389	. . . . . . 7 |- ((N e. (ZZ>` M) /\ j e. (ZZ>` (N + 1))) -> A.k e. ((N + 1)...j)(F` k) e. RR)
26	15, 16, 25	sylanc 471	. . . . . 6 |- ((N e. (ZZ>` M) /\ j e. (ZZ>` (N + 1))) -> ((<.(N + 1), + >. seq F)` j) e. RR)
27	26	adantlr 393	. . . . 5 |- (((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)0 <_ (F` k)) /\ j e. (ZZ>` (N + 1))) -> ((<.(N + 1), + >. seq F)` j) e. RR)
28	6	serzcmp0 7055	. . . . . . 7 |- ((j e. (ZZ>` (N + 1)) /\ A.k e. ((N + 1)...j)((F` k) e. RR /\ 0 <_ (F` k))) -> 0 <_ ((<.(N + 1), + >. seq F)` j))
29		pm3.2 283	. . . . . . . . . . . . . 14 |- ((F` k) e. RR -> (0 <_ (F` k) -> ((F` k) e. RR /\ 0 <_ (F` k))))
30	22, 29	syl 10	. . . . . . . . . . . . 13 |- (k e. (ZZ>` M) -> (0 <_ (F` k) -> ((F` k) e. RR /\ 0 <_ (F` k))))
31	30	a2i 9	. . . . . . . . . . . 12 |- ((k e. (ZZ>` M) -> 0 <_ (F` k)) -> (k e. (ZZ>` M) -> ((F` k) e. RR /\ 0 <_ (F` k))))
32	17, 20, 19	syl2an 454	. . . . . . . . . . . 12 |- ((k e. ((N + 1)...j) /\ N e. (ZZ>` M)) -> k e. (ZZ>` M))
33	31, 32	syl5 21	. . . . . . . . . . 11 |- ((k e. (ZZ>` M) -> 0 <_ (F` k)) -> ((k e. ((N + 1)...j) /\ N e. (ZZ>` M)) -> ((F` k) e. RR /\ 0 <_ (F` k))))
34	33	exp3a 375	. . . . . . . . . 10 |- ((k e. (ZZ>` M) -> 0 <_ (F` k)) -> (k e. ((N + 1)...j) -> (N e. (ZZ>` M) -> ((F` k) e. RR /\ 0 <_ (F` k)))))
35	34	com3r 35	. . . . . . . . 9 |- (N e. (ZZ>` M) -> ((k e. (ZZ>` M) -> 0 <_ (F` k)) -> (k e. ((N + 1)...j) -> ((F` k) e. RR /\ 0 <_ (F` k)))))
36	35	r19.20dv2 1711	. . . . . . . 8 |- (N e. (ZZ>` M) -> (A.k e. (ZZ>` M)0 <_ (F` k) -> A.k e. ((N + 1)...j)((F` k) e. RR /\ 0 <_ (F` k))))
37	36	imp 350	. . . . . . 7 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)0 <_ (F` k)) -> A.k e. ((N + 1)...j)((F` k) e. RR /\ 0 <_ (F` k)))
38	28, 37	sylan2 451	. . . . . 6 |- ((j e. (ZZ>` (N + 1)) /\ (N e. (ZZ>` M) /\ A.k e. (ZZ>` M)0 <_ (F` k))) -> 0 <_ ((<.(N + 1), + >. seq F)` j))
39	38	ancoms 436	. . . . 5 |- (((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)0 <_ (F` k)) /\ j e. (ZZ>` (N + 1))) -> 0 <_ ((<.(N + 1), + >. seq F)` j))
40	27, 39	jca 288	. . . 4 |- (((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)0 <_ (F` k)) /\ j e. (ZZ>` (N + 1))) -> (((<.(N + 1), + >. seq F)` j) e. RR /\ 0 <_ ((<.(N + 1), + >. seq F)` j)))
41	40	r19.21aiva 1714	. . 3 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)0 <_ (F` k)) -> A.j e. (ZZ>` (N + 1))(((<.(N + 1), + >. seq F)` j) e. RR /\ 0 <_ ((<.(N + 1), + >. seq F)` j)))
42	2, 5, 14, 41	syl3anc 858	. 2 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)0 <_ (F` k)) -> 0 <_ (A - ((<.M, + >. seq F)` N)))
43		subge0t 5674	. . . 4 |- ((A e. RR /\ ((<.M, + >. seq F)` N) e. RR) -> (0 <_ (A - ((<.M, + >. seq F)` N)) <-> ((<.M, + >. seq F)` N) <_ A))
44		eluzel2 6424	. . . . 5 |- (N e. (ZZ>` M) -> M e. ZZ)
45		elfzuzt 6488	. . . . . . . . . 10 |- (k e. (M...j) -> k e. (ZZ>` M))
46	45, 22	syl 10	. . . . . . . . 9 |- (k e. (M...j) -> (F` k) e. RR)
47	46	rgen 1698	. . . . . . . 8 |- A.k e. (M...j)(F` k) e. RR
48	6	serzreclt 7050	. . . . . . . 8 |- ((j e. (ZZ>` M) /\ A.k e. (M...j)(F` k) e. RR) -> ((<.M, + >. seq F)` j) e. RR)
49	47, 48	mpan2 696	. . . . . . 7 |- (j e. (ZZ>` M) -> ((<.M, + >. seq F)` j) e. RR)
50	49	rgen 1698	. . . . . 6 |- A.j e. (ZZ>` M)((<.M, + >. seq F)` j) e. RR
51	7	climrecl 7110	. . . . . 6 |- ((M e. ZZ /\ (<.M, + >. seq F) ~~> A /\ A.