Theorem lt2halvesd

Description: A sum is less than the whole if each term is less than half. (Contributed by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		rehalfcld.1	$$⊢\phi \to A\in ℝ$$
2		lt2halvesd.2	$$⊢\phi \to B\in ℝ$$
3		lt2halvesd.3	$$⊢\phi \to C\in ℝ$$
4		lt2halvesd.4	$$⊢\phi \to A<\frac{C}{2}$$
5		lt2halvesd.5	$$⊢\phi \to B<\frac{C}{2}$$
6		lt2halves	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge C\in ℝ\right)\to \left(\left(A<\frac{C}{2}\wedge B<\frac{C}{2}\right)\to A+B<C\right)$$
7	1 2 3 6	syl3anc	$$⊢\phi \to \left(\left(A<\frac{C}{2}\wedge B<\frac{C}{2}\right)\to A+B<C\right)$$
8	4 5 7	mp2and	$$⊢\phi \to A+B<C$$