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 )