Theorem iserzgt0 7211

Description: The infinite sum of positive reals is positive. (Contributed by Paul Chapman, 9-Feb-2008.)

Hypothesis

Ref	Expression
iserzgt0.1	|- F e. V

Assertion

Ref	Expression
iserzgt0	|- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k)) /\ E.x(<.M, + >. seq F) ~~> x) -> 0 < sum_k e. (ZZ>` N)(F` k))

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

Proof of Theorem iserzgt0

Step	Hyp	Ref	Expression
1		addgtge0t 5661	. . . 4 |- ((((F` N) e. RR /\ sum_k e. (ZZ>` (N + 1))(F` k) e. RR) /\ (0 < (F` N) /\ 0 <_ sum_k e. (ZZ>` (N + 1))(F` k))) -> 0 < ((F` N) + sum_k e. (ZZ>` (N + 1))(F` k)))
2	1	an4s 510	. . 3 |- ((((F` N) e. RR /\ 0 < (F` N)) /\ (sum_k e. (ZZ>` (N + 1))(F` k) e. RR /\ 0 <_ sum_k e. (ZZ>` (N + 1))(F` k))) -> 0 < ((F` N) + sum_k e. (ZZ>` (N + 1))(F` k)))
3		fveq2 3730	. . . . . . 7 |- (k = N -> (F` k) = (F` N))
4	3	eleq1d 1543	. . . . . 6 |- (k = N -> ((F` k) e. RR <-> (F` N) e. RR))
5	3	breq2d 2635	. . . . . 6 |- (k = N -> (0 < (F` k) <-> 0 < (F` N)))
6	4, 5	anbi12d 630	. . . . 5 |- (k = N -> (((F` k) e. RR /\ 0 < (F` k)) <-> ((F` N) e. RR /\ 0 < (F` N))))
7	6	rcla4va 1878	. . . 4 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k))) -> ((F` N) e. RR /\ 0 < (F` N)))
8	7	3adant3 801	. . 3 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k)) /\ E.x(<.M, + >. seq F) ~~> x) -> ((F` N) e. RR /\ 0 < (F` N)))
9		iserzgt0.1	. . . . . 6 |- F e. V
10	9	isumreclt 7210	. . . . 5 |- (((N + 1) e. ZZ /\ A.k e. (ZZ>` (N + 1))(F` k) e. RR /\ E.x(<.(N + 1), + >. seq F) ~~> x) -> sum_k e. (ZZ>` (N + 1))(F` k) e. RR)
11		eluzelz 6424	. . . . . . 7 |- (N e. (ZZ>` M) -> N e. ZZ)
12	11	peano2zd 6169	. . . . . 6 |- (N e. (ZZ>` M) -> (N + 1) e. ZZ)
13	12	3ad2ant1 802	. . . . 5 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k)) /\ E.x(<.M, + >. seq F) ~~> x) -> (N + 1) e. ZZ)
14		peano2uz 6448	. . . . . . . . . . 11 |- (N e. (ZZ>` M) -> (N + 1) e. (ZZ>` M))
15		uztrn 6429	. . . . . . . . . . . 12 |- ((k e. (ZZ>` (N + 1)) /\ (N + 1) e. (ZZ>` M)) -> k e. (ZZ>` M))
16	15	expcom 374	. . . . . . . . . . 11 |- ((N + 1) e. (ZZ>` M) -> (k e. (ZZ>` (N + 1)) -> k e. (ZZ>` M)))
17	14, 16	syl 10	. . . . . . . . . 10 |- (N e. (ZZ>` M) -> (k e. (ZZ>` (N + 1)) -> k e. (ZZ>` M)))
18	17	imim1d 28	. . . . . . . . 9 |- (N e. (ZZ>` M) -> ((k e. (ZZ>` M) -> ((F` k) e. RR /\ 0 < (F` k))) -> (k e. (ZZ>` (N + 1)) -> ((F` k) e. RR /\ 0 < (F` k)))))
19		pm3.26 319	. . . . . . . . 9 |- (((F` k) e. RR /\ 0 < (F` k)) -> (F` k) e. RR)
20	18, 19	syl8 24	. . . . . . . 8 |- (N e. (ZZ>` M) -> ((k e. (ZZ>` M) -> ((F` k) e. RR /\ 0 < (F` k))) -> (k e. (ZZ>` (N + 1)) -> (F` k) e. RR)))
21	20	r19.20dv2 1714	. . . . . . 7 |- (N e. (ZZ>` M) -> (A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k)) -> A.k e. (ZZ>` (N + 1))(F` k) e. RR))
22	21	imp 350	. . . . . 6 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k))) -> A.k e. (ZZ>` (N + 1))(F` k) e. RR)
23	22	3adant3 801	. . . . 5 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k)) /\ E.x(<.M, + >. seq F) ~~> x) -> A.k e. (ZZ>` (N + 1))(F` k) e. RR)
24	9	iserzext 7135	. . . . . 6 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)(F` k) e. CC /\ E.x(<.M, + >. seq F) ~~> x) -> E.x(<.(N + 1), + >. seq F) ~~> x)
25		recnt 5325	. . . . . . . 8 |- ((F` k) e. RR -> (F` k) e. CC)
26	25	adantr 391	. . . . . . 7 |- (((F` k) e. RR /\ 0 < (F` k)) -> (F` k) e. CC)
27	26	r19.20si 1709	. . . . . 6 |- (A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k)) -> A.k e. (ZZ>` M)(F` k) e. CC)
28	24, 27	syl3an2 862	. . . . 5 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k)) /\ E.x(<.M, + >. seq F) ~~> x) -> E.x(<.(N + 1), + >. seq F) ~~> x)
29	10, 13, 23, 28	syl3anc 860	. . . 4 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k)) /\ E.x(<.M, + >. seq F) ~~> x) -> sum_k e. (ZZ>` (N + 1))(F` k) e. RR)
30		sumex 6981	. . . . . 6 |- sum_k e. (ZZ>` (N + 1))(F` k) e. V
31	30, 9	iserzcmp0 7143	. . . . 5 |- (((N + 1) e. ZZ /\ (<.(N + 1), + >. seq F) ~~> sum_k e. (ZZ>` (N + 1))(F` k) /\ A.k e. (ZZ>` (N + 1))((F` k) e. RR /\ 0 <_ (F` k))) -> 0 <_ sum_k e. (ZZ>` (N + 1))(F` k))
32	9	isumclim2t 7199	. . . . . 6 |- (((N + 1) e. ZZ /\ E.x(<.(N + 1), + >. seq F) ~~> x) -> (<.(N + 1), + >. seq F) ~~> sum_k e. (ZZ>` (N + 1))(F` k))
33	32, 13, 28	sylanc 473	. . . . 5 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k)) /\ E.x(<.M, + >. seq F) ~~> x) -> (<.(N + 1), + >. seq F) ~~> sum_k e. (ZZ>` (N + 1))(F` k))
34		0re 5452	. . . . . . . . . . 11 |- 0 e. RR
35		ltlet 5532	. . . . . . . . . . 11 |- ((0 e. RR /\ (F` k) e. RR) -> (0 < (F` k) -> 0 <_ (F` k)))
36	34, 35	mpan 697	. . . . . . . . . 10 |- ((F` k) e. RR -> (0 < (F` k) -> 0 <_ (F` k)))
37	36	imdistani 445	. . . . . . . . 9 |- (((F` k) e. RR /\ 0 < (F` k)) -> ((F` k) e. RR /\ 0 <_ (F` k)))
38	18, 37	syl8 24	. . . . . . . 8 |- (N e. (ZZ>` M) -> ((k e. (ZZ>` M) -> ((F` k) e. RR /\ 0 < (F` k))) -> (k e. (ZZ>` (N + 1)) -> ((F` k) e. RR /\ 0 <_ (F` k)))))
39	38	r19.20dv2 1714	. . . . . . 7 |- (N e. (ZZ>` M) -> (A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k)) -> A.k e. (ZZ>` (N + 1))((F` k) e. RR /\ 0 <_ (F` k))))
40	39	imp 350	. . . . . 6 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k))) -> A.k e. (ZZ>` (N + 1))((F` k) e. RR /\ 0 <_ (F` k)))
41	40	3adant3 801	. . . . 5 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)((F` k) e. RR /\ 0 < (F` k)) /\ E.x(<.M, + >. seq F) ~~> x) -> A.k e. (ZZ>` (N + 1))((F` k) e. RR /\ 0 <_