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 )