This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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