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

Metamath Proof Explorer

Theorem fsumge1

Description: A sum of nonnegative numbers is greater than or equal to any one of its terms. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 4-Jun-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 )
fsumge1.4 
|- ( k = M -> B = C )
fsumge1.5 
|- ( ph -> M e. A )
Assertion fsumge1 
|- ( ph -> C <_ 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 fsumge1.4 
 |-  ( k = M -> B = C )
5 fsumge1.5 
 |-  ( ph -> M e. A )
6 4 eleq1d 
 |-  ( k = M -> ( B e. CC <-> C e. CC ) )
7 2 recnd 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
8 7 ralrimiva 
 |-  ( ph -> A. k e. A B e. CC )
9 6 8 5 rspcdva 
 |-  ( ph -> C e. CC )
10 4 sumsn 
 |-  ( ( M e. A /\ C e. CC ) -> sum_ k e. { M } B = C )
11 5 9 10 syl2anc 
 |-  ( ph -> sum_ k e. { M } B = C )
12 5 snssd 
 |-  ( ph -> { M } C_ A )
13 1 2 3 12 fsumless 
 |-  ( ph -> sum_ k e. { M } B <_ sum_ k e. A B )
14 11 13 eqbrtrrd 
 |-  ( ph -> C <_ sum_ k e. A B )