xaddge0

Description: The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	xaddge0	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 \leq A \land 0 \leq B)) \to 0 \leq A +_{𝑒} B$

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2	1	a1i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 \leq A \land 0 \leq B)) \to 0 \in ℝ^{*}$
3		simplr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 \leq A \land 0 \leq B)) \to B \in ℝ^{*}$
4		xaddcl	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A +_{𝑒} B \in ℝ^{*}$
5	4	adantr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 \leq A \land 0 \leq B)) \to A +_{𝑒} B \in ℝ^{*}$
6		simprr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 \leq A \land 0 \leq B)) \to 0 \leq B$
7		xaddid2	$⊢ B \in ℝ^{*} \to 0 +_{𝑒} B = B$
8	3 7	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 \leq A \land 0 \leq B)) \to 0 +_{𝑒} B = B$
9		simpll	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 \leq A \land 0 \leq B)) \to A \in ℝ^{*}$
10		simprl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 \leq A \land 0 \leq B)) \to 0 \leq A$
11		xleadd1a	$⊢ ((0 \in ℝ^{} \land A \in ℝ^{} \land B \in ℝ^{*}) \land 0 \leq A) \to 0 +_{𝑒} B \leq A +_{𝑒} B$
12	2 9 3 10 11	syl31anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 \leq A \land 0 \leq B)) \to 0 +_{𝑒} B \leq A +_{𝑒} B$
13	8 12	eqbrtrrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 \leq A \land 0 \leq B)) \to B \leq A +_{𝑒} B$
14	2 3 5 6 13	xrletrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (0 \leq A \land 0 \leq B)) \to 0 \leq A +_{𝑒} B$

Metamath Proof Explorer