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

Metamath Proof Explorer

Theorem fsumge0

Description: If all of the terms of a finite sum are nonnegative, so is the sum. (Contributed by NM, 26-Dec-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumge0.1 
|- ( ph -> A e. Fin )
fsumge0.2 
|- ( ( ph /\ k e. A ) -> B e. RR )
fsumge0.3 
|- ( ( ph /\ k e. A ) -> 0 <_ B )
Assertion fsumge0 
|- ( ph -> 0 <_ sum_ k e. A B )

Proof

Step Hyp Ref Expression
1 fsumge0.1 
 |-  ( ph -> A e. Fin )
2 fsumge0.2 
 |-  ( ( ph /\ k e. A ) -> B e. RR )
3 fsumge0.3 
 |-  ( ( ph /\ k e. A ) -> 0 <_ B )
4 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
5 ax-resscn 
 |-  RR C_ CC
6 4 5 sstri 
 |-  ( 0 [,) +oo ) C_ CC
7 6 a1i 
 |-  ( ph -> ( 0 [,) +oo ) C_ CC )
8 ge0addcl 
 |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
9 8 adantl 
 |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x + y ) e. ( 0 [,) +oo ) )
10 elrege0 
 |-  ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
11 2 3 10 sylanbrc 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
12 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
13 12 a1i 
 |-  ( ph -> 0 e. ( 0 [,) +oo ) )
14 7 9 1 11 13 fsumcllem 
 |-  ( ph -> sum_ k e. A B e. ( 0 [,) +oo ) )
15 elrege0 
 |-  ( sum_ k e. A B e. ( 0 [,) +oo ) <-> ( sum_ k e. A B e. RR /\ 0 <_ sum_ k e. A B ) )
16 15 simprbi 
 |-  ( sum_ k e. A B e. ( 0 [,) +oo ) -> 0 <_ sum_ k e. A B )
17 14 16 syl 
 |-  ( ph -> 0 <_ sum_ k e. A B )