Metamath Proof Explorer


Theorem 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+ )