isumrpcl

Description: The infinite sum of positive reals is positive. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	isumrpcl.1	\|- Z = ( ZZ>= ` M )
	isumrpcl.2	\|- W = ( ZZ>= ` N )
	isumrpcl.3	\|- ( ph -> N e. Z )
	isumrpcl.4	\|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
	isumrpcl.5	\|- ( ( ph /\ k e. Z ) -> A e. RR+ )
	isumrpcl.6	\|- ( ph -> seq M ( + , F ) e. dom ~~> )
Assertion	isumrpcl	\|- ( ph -> sum_ k e. W A e. RR+ )

Proof

Step	Hyp	Ref	Expression
1		isumrpcl.1	\|- Z = ( ZZ>= ` M )
2		isumrpcl.2	\|- W = ( ZZ>= ` N )
3		isumrpcl.3	\|- ( ph -> N e. Z )
4		isumrpcl.4	\|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
5		isumrpcl.5	\|- ( ( ph /\ k e. Z ) -> A e. RR+ )
6		isumrpcl.6	\|- ( ph -> seq M ( + , F ) e. dom ~~> )
7	3 1	eleqtrdi	\|- ( ph -> N e. ( ZZ>= ` M ) )
8		eluzelz	\|- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
9	7 8	syl	\|- ( ph -> N e. ZZ )
10		uzss	\|- ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
11	7 10	syl	\|- ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
12	11 2 1	3sstr4g	\|- ( ph -> W C_ Z )
13	12	sselda	\|- ( ( ph /\ k e. W ) -> k e. Z )
14	13 4	syldan	\|- ( ( ph /\ k e. W ) -> ( F ` k ) = A )
15	5	rpred	\|- ( ( ph /\ k e. Z ) -> A e. RR )
16	13 15	syldan	\|- ( ( ph /\ k e. W ) -> A e. RR )
17	4 5	eqeltrd	\|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR+ )
18	17	rpcnd	\|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
19	1 3 18	iserex	\|- ( ph -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )
20	6 19	mpbid	\|- ( ph -> seq N ( + , F ) e. dom ~~> )
21	2 9 14 16 20	isumrecl	\|- ( ph -> sum_ k e. W A e. RR )
22		fveq2	\|- ( k = N -> ( F ` k ) = ( F ` N ) )
23	22	eleq1d	\|- ( k = N -> ( ( F ` k ) e. RR+ <-> ( F ` N ) e. RR+ ) )
24	17	ralrimiva	\|- ( ph -> A. k e. Z ( F ` k ) e. RR+ )
25	23 24 3	rspcdva	\|- ( ph -> ( F ` N ) e. RR+ )
26		seq1	\|- ( N e. ZZ -> ( seq N ( + , F ) ` N ) = ( F ` N ) )
27	9 26	syl	\|- ( ph -> ( seq N ( + , F ) ` N ) = ( F ` N ) )
28		uzid	\|- ( N e. ZZ -> N e. ( ZZ>= ` N ) )
29	9 28	syl	\|- ( ph -> N e. ( ZZ>= ` N ) )
30	29 2	eleqtrrdi	\|- ( ph -> N e. W )
31	16	recnd	\|- ( ( ph /\ k e. W ) -> A e. CC )
32	2 9 14 31 20	isumclim2	\|- ( ph -> seq N ( + , F ) ~~> sum_ k e. W A )
33	12	sseld	\|- ( ph -> ( m e. W -> m e. Z ) )
34		fveq2	\|- ( k = m -> ( F ` k ) = ( F ` m ) )
35	34	eleq1d	\|- ( k = m -> ( ( F ` k ) e. RR+ <-> ( F ` m ) e. RR+ ) )
36	35	rspcv	\|- ( m e. Z -> ( A. k e. Z ( F ` k ) e. RR+ -> ( F ` m ) e. RR+ ) )
37	33 24 36	syl6ci	\|- ( ph -> ( m e. W -> ( F ` m ) e. RR+ ) )
38	37	imp	\|- ( ( ph /\ m e. W ) -> ( F ` m ) e. RR+ )
39	38	rpred	\|- ( ( ph /\ m e. W ) -> ( F ` m ) e. RR )
40	38	rpge0d	\|- ( ( ph /\ m e. W ) -> 0 <_ ( F ` m ) )
41	2 30 32 39 40	climserle	\|- ( ph -> ( seq N ( + , F ) ` N ) <_ sum_ k e. W A )
42	27 41	eqbrtrrd	\|- ( ph -> ( F ` N ) <_ sum_ k e. W A )
43	21 25 42	rpgecld	\|- ( ph -> sum_ k e. W A e. RR+ )

Metamath Proof Explorer

Theorem isumrpcl

Proof