Metamath Proof Explorer

Theorem serge0

Description: A finite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 8-Feb-2014) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses serge0.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
serge0.2 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )
serge0.3 
|- ( ( ph /\ k e. ( M ... N ) ) -> 0 <_ ( F ` k ) )
Assertion serge0 
|- ( ph -> 0 <_ ( seq M ( + , F ) ` N ) )

Proof

Step Hyp Ref Expression
1 serge0.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 serge0.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )
3 serge0.3 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> 0 <_ ( F ` k ) )
4 breq2 
 |-  ( x = ( F ` k ) -> ( 0 <_ x <-> 0 <_ ( F ` k ) ) )
5 4 2 3 elrabd 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. { x e. RR | 0 <_ x } )
6 breq2 
 |-  ( x = k -> ( 0 <_ x <-> 0 <_ k ) )
7 6 elrab 
 |-  ( k e. { x e. RR | 0 <_ x } <-> ( k e. RR /\ 0 <_ k ) )
8 breq2 
 |-  ( x = y -> ( 0 <_ x <-> 0 <_ y ) )
9 8 elrab 
 |-  ( y e. { x e. RR | 0 <_ x } <-> ( y e. RR /\ 0 <_ y ) )
10 breq2 
 |-  ( x = ( k + y ) -> ( 0 <_ x <-> 0 <_ ( k + y ) ) )
11 readdcl 
 |-  ( ( k e. RR /\ y e. RR ) -> ( k + y ) e. RR )
12 11 ad2ant2r 
 |-  ( ( ( k e. RR /\ 0 <_ k ) /\ ( y e. RR /\ 0 <_ y ) ) -> ( k + y ) e. RR )
13 addge0 
 |-  ( ( ( k e. RR /\ y e. RR ) /\ ( 0 <_ k /\ 0 <_ y ) ) -> 0 <_ ( k + y ) )
14 13 an4s 
 |-  ( ( ( k e. RR /\ 0 <_ k ) /\ ( y e. RR /\ 0 <_ y ) ) -> 0 <_ ( k + y ) )
15 10 12 14 elrabd 
 |-  ( ( ( k e. RR /\ 0 <_ k ) /\ ( y e. RR /\ 0 <_ y ) ) -> ( k + y ) e. { x e. RR | 0 <_ x } )
16 7 9 15 syl2anb 
 |-  ( ( k e. { x e. RR | 0 <_ x } /\ y e. { x e. RR | 0 <_ x } ) -> ( k + y ) e. { x e. RR | 0 <_ x } )
17 16 adantl 
 |-  ( ( ph /\ ( k e. { x e. RR | 0 <_ x } /\ y e. { x e. RR | 0 <_ x } ) ) -> ( k + y ) e. { x e. RR | 0 <_ x } )
18 1 5 17 seqcl 
 |-  ( ph -> ( seq M ( + , F ) ` N ) e. { x e. RR | 0 <_ x } )
19 breq2 
 |-  ( x = ( seq M ( + , F ) ` N ) -> ( 0 <_ x <-> 0 <_ ( seq M ( + , F ) ` N ) ) )
20 19 elrab 
 |-  ( ( seq M ( + , F ) ` N ) e. { x e. RR | 0 <_ x } <-> ( ( seq M ( + , F ) ` N ) e. RR /\ 0 <_ ( seq M ( + , F ) ` N ) ) )
21 20 simprbi 
 |-  ( ( seq M ( + , F ) ` N ) e. { x e. RR | 0 <_ x } -> 0 <_ ( seq M ( + , F ) ` N ) )
22 18 21 syl 
 |-  ( ph -> 0 <_ ( seq M ( + , F ) ` N ) )