Theorem fsumle

Description: If all of the terms of finite sums compare, so do the sums. (Contributed by NM, 11-Dec-2005) (Proof shortened by Mario Carneiro, 24-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		fsumle.1	|- ( ph -> A e. Fin )
2		fsumle.2	|- ( ( ph /\ k e. A ) -> B e. RR )
3		fsumle.3	|- ( ( ph /\ k e. A ) -> C e. RR )
4		fsumle.4	|- ( ( ph /\ k e. A ) -> B <_ C )
5	3 2	resubcld	|- ( ( ph /\ k e. A ) -> ( C - B ) e. RR )
6	3 2	subge0d	|- ( ( ph /\ k e. A ) -> ( 0 <_ ( C - B ) <-> B <_ C ) )
7	4 6	mpbird	|- ( ( ph /\ k e. A ) -> 0 <_ ( C - B ) )
8	1 5 7	fsumge0	|- ( ph -> 0 <_ sum_ k e. A ( C - B ) )
9	3	recnd	|- ( ( ph /\ k e. A ) -> C e. CC )
10	2	recnd	|- ( ( ph /\ k e. A ) -> B e. CC )
11	1 9 10	fsumsub	|- ( ph -> sum_ k e. A ( C - B ) = ( sum_ k e. A C - sum_ k e. A B ) )
12	8 11	breqtrd	|- ( ph -> 0 <_ ( sum_ k e. A C - sum_ k e. A B ) )
13	1 3	fsumrecl	|- ( ph -> sum_ k e. A C e. RR )
14	1 2	fsumrecl	|- ( ph -> sum_ k e. A B e. RR )
15	13 14	subge0d	|- ( ph -> ( 0 <_ ( sum_ k e. A C - sum_ k e. A B ) <-> sum_ k e. A B <_ sum_ k e. A C ) )
16	12 15	mpbid	|- ( ph -> sum_ k e. A B <_ sum_ k e. A C )