This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addgtge0

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	addgtge0	$⊢ ((A \in ℝ \land B \in ℝ) \land (0 < A \land 0 \leq B)) \to 0 < A + B$

Proof

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