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	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumlt.2	$$⊢\phi \to A\ne \varnothing$$
	fsumlt.3	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$
	fsumlt.4	$$⊢\left(\phi \wedge k\in A\right)\to C\in ℝ$$
	fsumlt.5	$$⊢\left(\phi \wedge k\in A\right)\to B<C$$
Assertion	fsumlt	$$⊢\phi \to \sum _{k\in A}B<\sum _{k\in A}C$$

Proof

Step	Hyp	Ref	Expression
1		fsumlt.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fsumlt.2	$$⊢\phi \to A\ne \varnothing$$
3		fsumlt.3	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$
4		fsumlt.4	$$⊢\left(\phi \wedge k\in A\right)\to C\in ℝ$$
5		fsumlt.5	$$⊢\left(\phi \wedge k\in A\right)\to B<C$$
6		difrp	$$⊢\left(B\in ℝ\wedge C\in ℝ\right)\to \left(B<C\leftrightarrow C-B\in {ℝ}^{+}\right)$$
7	3 4 6	syl2anc	$$⊢\left(\phi \wedge k\in A\right)\to \left(B<C\leftrightarrow C-B\in {ℝ}^{+}\right)$$
8	5 7	mpbid	$$⊢\left(\phi \wedge k\in A\right)\to C-B\in {ℝ}^{+}$$
9	1 2 8	fsumrpcl	$$⊢\phi \to \sum _{k\in A}\left(C-B\right)\in {ℝ}^{+}$$
10	9	rpgt0d	$$⊢\phi \to 0<\sum _{k\in A}\left(C-B\right)$$
11	4	recnd	$$⊢\left(\phi \wedge k\in A\right)\to C\in ℂ$$
12	3	recnd	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
13	1 11 12	fsumsub	$$⊢\phi \to \sum _{k\in A}\left(C-B\right)=\sum _{k\in A}C-\sum _{k\in A}B$$
14	10 13	breqtrd	$$⊢\phi \to 0<\sum _{k\in A}C-\sum _{k\in A}B$$
15	1 3	fsumrecl	$$⊢\phi \to \sum _{k\in A}B\in ℝ$$
16	1 4	fsumrecl	$$⊢\phi \to \sum _{k\in A}C\in ℝ$$
17	15 16	posdifd	$$⊢\phi \to \left(\sum _{k\in A}B<\sum _{k\in A}C\leftrightarrow 0<\sum _{k\in A}C-\sum _{k\in A}B\right)$$
18	14 17	mpbird	$$⊢\phi \to \sum _{k\in A}B<\sum _{k\in A}C$$