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 )

Metamath Proof Explorer

Theorem fsumless

Proof