xrge0addgt0

Description: The sum of nonnegative and positive numbers is positive. See addgtge0 . (Contributed by Thierry Arnoux, 6-Jul-2017)

		Ref	Expression
	Assertion	xrge0addgt0	$⊢ ((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \to 0 < A +_{𝑒} B$

Proof

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2		xaddid1	$⊢ 0 \in ℝ^{*} \to 0 +_{𝑒} 0 = 0$
3	1 2	ax-mp	$⊢ 0 +_{𝑒} 0 = 0$
4		simplr	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 < B) \to 0 < A$
5		simpr	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 < B) \to 0 < B$
6	1	a1i	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 < B) \to 0 \in ℝ^{*}$
7		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
8		simplll	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 < B) \to A \in [0, +∞]$
9	7 8	sselid	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 < B) \to A \in ℝ^{*}$
10		simpllr	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 < B) \to B \in [0, +∞]$
11	7 10	sselid	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 < B) \to B \in ℝ^{*}$
12		xlt2add	$⊢ ((0 \in ℝ^{} \land 0 \in ℝ^{}) \land (A \in ℝ^{} \land B \in ℝ^{})) \to ((0 < A \land 0 < B) \to 0 +_{𝑒} 0 < A +_{𝑒} B)$
13	6 6 9 11 12	syl22anc	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 < B) \to ((0 < A \land 0 < B) \to 0 +_{𝑒} 0 < A +_{𝑒} B)$
14	4 5 13	mp2and	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 < B) \to 0 +_{𝑒} 0 < A +_{𝑒} B$
15	3 14	eqbrtrrid	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 < B) \to 0 < A +_{𝑒} B$
16		simplr	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 = B) \to 0 < A$
17		oveq2	$⊢ 0 = B \to A +_{𝑒} 0 = A +_{𝑒} B$
18	17	adantl	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 = B) \to A +_{𝑒} 0 = A +_{𝑒} B$
19	18	breq2d	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 = B) \to (0 < A +_{𝑒} 0 \leftrightarrow 0 < A +_{𝑒} B)$
20		simplll	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 = B) \to A \in [0, +∞]$
21	7 20	sselid	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 = B) \to A \in ℝ^{*}$
22		xaddid1	$⊢ A \in ℝ^{*} \to A +_{𝑒} 0 = A$
23	21 22	syl	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 = B) \to A +_{𝑒} 0 = A$
24	23	breq2d	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 = B) \to (0 < A +_{𝑒} 0 \leftrightarrow 0 < A)$
25	19 24	bitr3d	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 = B) \to (0 < A +_{𝑒} B \leftrightarrow 0 < A)$
26	16 25	mpbird	$⊢ (((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \land 0 = B) \to 0 < A +_{𝑒} B$
27	1	a1i	$⊢ ((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \to 0 \in ℝ^{*}$
28		simplr	$⊢ ((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \to B \in [0, +∞]$
29	7 28	sselid	$⊢ ((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \to B \in ℝ^{*}$
30		pnfxr	$⊢ +∞ \in ℝ^{*}$
31	30	a1i	$⊢ ((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \to +∞ \in ℝ^{*}$
32		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land B \in [0, +∞]) \to 0 \leq B$
33	27 31 28 32	syl3anc	$⊢ ((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \to 0 \leq B$
34		xrleloe	$⊢ (0 \in ℝ^{} \land B \in ℝ^{}) \to (0 \leq B \leftrightarrow (0 < B \lor 0 = B))$
35	34	biimpa	$⊢ ((0 \in ℝ^{} \land B \in ℝ^{}) \land 0 \leq B) \to (0 < B \lor 0 = B)$
36	27 29 33 35	syl21anc	$⊢ ((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \to (0 < B \lor 0 = B)$
37	15 26 36	mpjaodan	$⊢ ((A \in [0, +∞] \land B \in [0, +∞]) \land 0 < A) \to 0 < A +_{𝑒} B$

Metamath Proof Explorer

Theorem xrge0addgt0

Proof