lt2halves

Description: A sum is less than the whole if each term is less than half. (Contributed by NM, 13-Dec-2006)

		Ref	Expression
	Assertion	lt2halves	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A < \frac{C}{2} \land B < \frac{C}{2}) \to A + B < C)$

Step	Hyp	Ref	Expression
1		3simpa	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A \in ℝ \land B \in ℝ)$
2		rehalfcl	$⊢ C \in ℝ \to \frac{C}{2} \in ℝ$
3	2 2	jca	$⊢ C \in ℝ \to (\frac{C}{2} \in ℝ \land \frac{C}{2} \in ℝ)$
4	3	3ad2ant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (\frac{C}{2} \in ℝ \land \frac{C}{2} \in ℝ)$
5		lt2add	$⊢ ((A \in ℝ \land B \in ℝ) \land (\frac{C}{2} \in ℝ \land \frac{C}{2} \in ℝ)) \to ((A < \frac{C}{2} \land B < \frac{C}{2}) \to A + B < (\frac{C}{2}) + (\frac{C}{2}))$
6	1 4 5	syl2anc	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A < \frac{C}{2} \land B < \frac{C}{2}) \to A + B < (\frac{C}{2}) + (\frac{C}{2}))$
7		recn	$⊢ C \in ℝ \to C \in ℂ$
8		2halves	$⊢ C \in ℂ \to (\frac{C}{2}) + (\frac{C}{2}) = C$
9	7 8	syl	$⊢ C \in ℝ \to (\frac{C}{2}) + (\frac{C}{2}) = C$
10	9	breq2d	$⊢ C \in ℝ \to (A + B < (\frac{C}{2}) + (\frac{C}{2}) \leftrightarrow A + B < C)$
11	10	3ad2ant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A + B < (\frac{C}{2}) + (\frac{C}{2}) \leftrightarrow A + B < C)$
12	6 11	sylibd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A < \frac{C}{2} \land B < \frac{C}{2}) \to A + B < C)$

Metamath Proof Explorer