Metamath Proof Explorer


Theorem isumge0

Description: An infinite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 28-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 isumrecl.1
 |-  Z = ( ZZ>= ` M )
2 isumrecl.2
 |-  ( ph -> M e. ZZ )
3 isumrecl.3
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4 isumrecl.4
 |-  ( ( ph /\ k e. Z ) -> A e. RR )
5 isumrecl.5
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
6 isumge0.6
 |-  ( ( ph /\ k e. Z ) -> 0 <_ A )
7 4 recnd
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
8 1 2 3 7 5 isumclim2
 |-  ( ph -> seq M ( + , F ) ~~> sum_ k e. Z A )
9 fveq2
 |-  ( j = k -> ( F ` j ) = ( F ` k ) )
10 9 cbvsumv
 |-  sum_ j e. Z ( F ` j ) = sum_ k e. Z ( F ` k )
11 3 sumeq2dv
 |-  ( ph -> sum_ k e. Z ( F ` k ) = sum_ k e. Z A )
12 10 11 eqtrid
 |-  ( ph -> sum_ j e. Z ( F ` j ) = sum_ k e. Z A )
13 8 12 breqtrrd
 |-  ( ph -> seq M ( + , F ) ~~> sum_ j e. Z ( F ` j ) )
14 3 4 eqeltrd
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
15 6 3 breqtrrd
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
16 1 2 13 14 15 iserge0
 |-  ( ph -> 0 <_ sum_ j e. Z ( F ` j ) )
17 16 12 breqtrd
 |-  ( ph -> 0 <_ sum_ k e. Z A )