Metamath Proof Explorer

Theorem fsumless

Description: A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by NM, 26-Dec-2005) (Proof shortened 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 )
fsumless.4 
|- ( ph -> C C_ A )
Assertion fsumless 
|- ( ph -> sum_ k e. C B <_ 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 fsumless.4 
 |-  ( ph -> C C_ A )
5 difss 
 |-  ( A \ C ) C_ A
6 ssfi 
 |-  ( ( A e. Fin /\ ( A \ C ) C_ A ) -> ( A \ C ) e. Fin )
7 1 5 6 sylancl 
 |-  ( ph -> ( A \ C ) e. Fin )
8 eldifi 
 |-  ( k e. ( A \ C ) -> k e. A )
9 8 2 sylan2 
 |-  ( ( ph /\ k e. ( A \ C ) ) -> B e. RR )
10 8 3 sylan2 
 |-  ( ( ph /\ k e. ( A \ C ) ) -> 0 <_ B )
11 7 9 10 fsumge0 
 |-  ( ph -> 0 <_ sum_ k e. ( A \ C ) B )
12 1 4 ssfid 
 |-  ( ph -> C e. Fin )
13 4 sselda 
 |-  ( ( ph /\ k e. C ) -> k e. A )
14 13 2 syldan 
 |-  ( ( ph /\ k e. C ) -> B e. RR )
15 12 14 fsumrecl 
 |-  ( ph -> sum_ k e. C B e. RR )
16 7 9 fsumrecl 
 |-  ( ph -> sum_ k e. ( A \ C ) B e. RR )
17 15 16 addge01d 
 |-  ( ph -> ( 0 <_ sum_ k e. ( A \ C ) B <-> sum_ k e. C B <_ ( sum_ k e. C B + sum_ k e. ( A \ C ) B ) ) )
18 11 17 mpbid 
 |-  ( ph -> sum_ k e. C B <_ ( sum_ k e. C B + sum_ k e. ( A \ C ) B ) )
19 disjdif 
 |-  ( C i^i ( A \ C ) ) = (/)
20 19 a1i 
 |-  ( ph -> ( C i^i ( A \ C ) ) = (/) )
21 undif 
 |-  ( C C_ A <-> ( C u. ( A \ C ) ) = A )
22 4 21 sylib 
 |-  ( ph -> ( C u. ( A \ C ) ) = A )
23 22 eqcomd 
 |-  ( ph -> A = ( C u. ( A \ C ) ) )
24 2 recnd 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
25 20 23 1 24 fsumsplit 
 |-  ( ph -> sum_ k e. A B = ( sum_ k e. C B + sum_ k e. ( A \ C ) B ) )
26 18 25 breqtrrd 
 |-  ( ph -> sum_ k e. C B <_ sum_ k e. A B )