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

Metamath Proof Explorer

Theorem fsumlt

Description: If every term in one finite sum is less than the corresponding term in another, then the first sum is less than the second. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 3-Jun-2014)

Ref Expression
Hypotheses fsumlt.1 
|- ( ph -> A e. Fin )
fsumlt.2 
|- ( ph -> A =/= (/) )
fsumlt.3 
|- ( ( ph /\ k e. A ) -> B e. RR )
fsumlt.4 
|- ( ( ph /\ k e. A ) -> C e. RR )
fsumlt.5 
|- ( ( ph /\ k e. A ) -> B < C )
Assertion fsumlt 
|- ( ph -> sum_ k e. A B < sum_ k e. A C )

Proof

Step Hyp Ref Expression
1 fsumlt.1 
 |-  ( ph -> A e. Fin )
2 fsumlt.2 
 |-  ( ph -> A =/= (/) )
3 fsumlt.3 
 |-  ( ( ph /\ k e. A ) -> B e. RR )
4 fsumlt.4 
 |-  ( ( ph /\ k e. A ) -> C e. RR )
5 fsumlt.5 
 |-  ( ( ph /\ k e. A ) -> B < C )
6 difrp 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B < C <-> ( C - B ) e. RR+ ) )
7 3 4 6 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( B < C <-> ( C - B ) e. RR+ ) )
8 5 7 mpbid 
 |-  ( ( ph /\ k e. A ) -> ( C - B ) e. RR+ )
9 1 2 8 fsumrpcl 
 |-  ( ph -> sum_ k e. A ( C - B ) e. RR+ )
10 9 rpgt0d 
 |-  ( ph -> 0 < sum_ k e. A ( C - B ) )
11 4 recnd 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
12 3 recnd 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
13 1 11 12 fsumsub 
 |-  ( ph -> sum_ k e. A ( C - B ) = ( sum_ k e. A C - sum_ k e. A B ) )
14 10 13 breqtrd 
 |-  ( ph -> 0 < ( sum_ k e. A C - sum_ k e. A B ) )
15 1 3 fsumrecl 
 |-  ( ph -> sum_ k e. A B e. RR )
16 1 4 fsumrecl 
 |-  ( ph -> sum_ k e. A C e. RR )
17 15 16 posdifd 
 |-  ( ph -> ( sum_ k e. A B < sum_ k e. A C <-> 0 < ( sum_ k e. A C - sum_ k e. A B ) ) )
18 14 17 mpbird 
 |-  ( ph -> sum_ k e. A B < sum_ k e. A C )