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 φ A Fin
fsumlt.2 φ A
fsumlt.3 φ k A B
fsumlt.4 φ k A C
fsumlt.5 φ k A B < C
Assertion fsumlt φ k A B < k A C

Proof

Step Hyp Ref Expression
1 fsumlt.1 φ A Fin
2 fsumlt.2 φ A
3 fsumlt.3 φ k A B
4 fsumlt.4 φ k A C
5 fsumlt.5 φ k A B < C
6 difrp B C B < C C B +
7 3 4 6 syl2anc φ k A B < C C B +
8 5 7 mpbid φ k A C B +
9 1 2 8 fsumrpcl φ k A C B +
10 9 rpgt0d φ 0 < k A C B
11 4 recnd φ k A C
12 3 recnd φ k A B
13 1 11 12 fsumsub φ k A C B = k A C k A B
14 10 13 breqtrd φ 0 < k A C k A B
15 1 3 fsumrecl φ k A B
16 1 4 fsumrecl φ k A C
17 15 16 posdifd φ k A B < k A C 0 < k A C k A B
18 14 17 mpbird φ k A B < k A C