# 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 )`
` |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x + y ) e. ( 0 [,) +oo ) )`
` |-  ( ( 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 )`