addge0

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

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

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

Metamath Proof Explorer