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

Metamath Proof Explorer

Theorem iserge0

Description: The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 3-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 clim2ser.1 
 |-  Z = ( ZZ>= ` M )
2 iserge0.2 
 |-  ( ph -> M e. ZZ )
3 iserge0.3 
 |-  ( ph -> seq M ( + , F ) ~~> A )
4 iserge0.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
5 iserge0.5 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
6 serclim0 
 |-  ( M e. ZZ -> seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 )
7 2 6 syl 
 |-  ( ph -> seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 )
8 simpr 
 |-  ( ( ph /\ k e. Z ) -> k e. Z )
9 8 1 eleqtrdi 
 |-  ( ( ph /\ k e. Z ) -> k e. ( ZZ>= ` M ) )
10 c0ex 
 |-  0 e. _V
11 10 fvconst2 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( ( ZZ>= ` M ) X. { 0 } ) ` k ) = 0 )
12 9 11 syl 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( ZZ>= ` M ) X. { 0 } ) ` k ) = 0 )
13 0re 
 |-  0 e. RR
14 12 13 eqeltrdi 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( ZZ>= ` M ) X. { 0 } ) ` k ) e. RR )
15 12 5 eqbrtrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( ZZ>= ` M ) X. { 0 } ) ` k ) <_ ( F ` k ) )
16 1 2 7 3 14 4 15 iserle 
 |-  ( ph -> 0 <_ A )