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

Proof

Step	Hyp	Ref	Expression
1		fsumle.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fsumle.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$
3		fsumle.3	$$⊢\left(\phi \wedge k\in A\right)\to C\in ℝ$$
4		fsumle.4	$$⊢\left(\phi \wedge k\in A\right)\to B\le C$$
5	3 2	resubcld	$$⊢\left(\phi \wedge k\in A\right)\to C-B\in ℝ$$
6	3 2	subge0d	$$⊢\left(\phi \wedge k\in A\right)\to \left(0\le C-B\leftrightarrow B\le C\right)$$
7	4 6	mpbird	$$⊢\left(\phi \wedge k\in A\right)\to 0\le C-B$$
8	1 5 7	fsumge0	$$⊢\phi \to 0\le \sum _{k\in A}\left(C-B\right)$$
9	3	recnd	$$⊢\left(\phi \wedge k\in A\right)\to C\in ℂ$$
10	2	recnd	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
11	1 9 10	fsumsub	$$⊢\phi \to \sum _{k\in A}\left(C-B\right)=\sum _{k\in A}C-\sum _{k\in A}B$$
12	8 11	breqtrd	$$⊢\phi \to 0\le \sum _{k\in A}C-\sum _{k\in A}B$$
13	1 3	fsumrecl	$$⊢\phi \to \sum _{k\in A}C\in ℝ$$
14	1 2	fsumrecl	$$⊢\phi \to \sum _{k\in A}B\in ℝ$$
15	13 14	subge0d	$$⊢\phi \to \left(0\le \sum _{k\in A}C-\sum _{k\in A}B\leftrightarrow \sum _{k\in A}B\le \sum _{k\in A}C\right)$$
16	12 15	mpbid	$$⊢\phi \to \sum _{k\in A}B\le \sum _{k\in A}C$$