addgegt0

Description: The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

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

Proof

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

Metamath Proof Explorer

Theorem addgegt0

Proof