xraddge02

Description: A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 28-Dec-2016)

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

Step	Hyp	Ref	Expression
1		xrleid	$⊢ A \in ℝ^{*} \to A \leq A$
2	1	adantr	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A \leq A$
3		simpl	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A \in ℝ^{*}$
4		0xr	$⊢ 0 \in ℝ^{*}$
5	3 4	jctir	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \in ℝ^{} \land 0 \in ℝ^{})$
6		xle2add	$⊢ ((A \in ℝ^{} \land 0 \in ℝ^{}) \land (A \in ℝ^{} \land B \in ℝ^{})) \to ((A \leq A \land 0 \leq B) \to A +_{𝑒} 0 \leq A +_{𝑒} B)$
7	5 6	mpancom	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A \leq A \land 0 \leq B) \to A +_{𝑒} 0 \leq A +_{𝑒} B)$
8	2 7	mpand	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (0 \leq B \to A +_{𝑒} 0 \leq A +_{𝑒} B)$
9		xaddrid	$⊢ A \in ℝ^{*} \to A +_{𝑒} 0 = A$
10	9	breq1d	$⊢ A \in ℝ^{*} \to (A +_{𝑒} 0 \leq A +_{𝑒} B \leftrightarrow A \leq A +_{𝑒} B)$
11	10	adantr	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A +_{𝑒} 0 \leq A +_{𝑒} B \leftrightarrow A \leq A +_{𝑒} B)$
12	8 11	sylibd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (0 \leq B \to A \leq A +_{𝑒} B)$

Metamath Proof Explorer