addgt0

Description: The sum of 2 positive numbers is positive. (Contributed by NM, 1-Jun-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

		Ref	Expression
	Assertion	addgt0	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < B)) \to 0 < A + B$

Step	Hyp	Ref	Expression
1		00id	$⊢ 0 + 0 = 0$
2		0re	$⊢ 0 \in ℝ$
3		lt2add	$⊢ ((0 \in ℝ \land 0 \in ℝ) \land (A \in ℝ \land B \in ℝ)) \to ((0 < A \land 0 < B) \to 0 + 0 < A + B)$
4	2 2 3	mpanl12	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 < A \land 0 < B) \to 0 + 0 < A + B)$
5	4	imp	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < B)) \to 0 + 0 < A + B$
6	1 5	eqbrtrrid	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 < B)) \to 0 < A + B$

Metamath Proof Explorer