Theorem xrge0addge

Description: A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 19-Jul-2020)

	Ref	Expression
Assertion	xrge0addge	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elxrge0	⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) )
2	1	biimpi	⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) → ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) )
3		xraddge02	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ 𝐵 → 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) ) )
4	3	impr	⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) → 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) )
5	2 4	sylan2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) )