Theorem le2halvesd

Description: A sum is less than the whole if each term is less than half. (Contributed by Thierry Arnoux, 29-Nov-2017)

	Ref	Expression
Hypotheses	le2halvesd.1	$$⊢\phi \to A\in ℝ$$
	le2halvesd.2	$$⊢\phi \to B\in ℝ$$
	le2halvesd.3	$$⊢\phi \to C\in ℝ$$
	le2halvesd.4	$$⊢\phi \to A\le \frac{C}{2}$$
	le2halvesd.5	$$⊢\phi \to B\le \frac{C}{2}$$
Assertion	le2halvesd	$$⊢\phi \to A+B\le C$$

Proof

Step	Hyp	Ref	Expression
1		le2halvesd.1	$$⊢\phi \to A\in ℝ$$
2		le2halvesd.2	$$⊢\phi \to B\in ℝ$$
3		le2halvesd.3	$$⊢\phi \to C\in ℝ$$
4		le2halvesd.4	$$⊢\phi \to A\le \frac{C}{2}$$
5		le2halvesd.5	$$⊢\phi \to B\le \frac{C}{2}$$
6	3	rehalfcld	$$⊢\phi \to \frac{C}{2}\in ℝ$$
7	1 2 6 6 4 5	le2addd	$$⊢\phi \to A+B\le \left(\frac{C}{2}\right)+\left(\frac{C}{2}\right)$$
8	3	recnd	$$⊢\phi \to C\in ℂ$$
9	8	2halvesd	$$⊢\phi \to \left(\frac{C}{2}\right)+\left(\frac{C}{2}\right)=C$$
10	7 9	breqtrd	$$⊢\phi \to A+B\le C$$