Metamath Proof Explorer

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 ⊢ A ∈ ℝ * ∧ B ∈ 0 +∞ → A ≤ A + 𝑒 B

Proof

Step Hyp Ref Expression
1 elxrge0 ⊢ B ∈ 0 +∞ ↔ B ∈ ℝ * ∧ 0 ≤ B
2 1 biimpi ⊢ B ∈ 0 +∞ → B ∈ ℝ * ∧ 0 ≤ B
3 xraddge02 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → 0 ≤ B → A ≤ A + 𝑒 B
4 3 impr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ 0 ≤ B → A ≤ A + 𝑒 B
5 2 4 sylan2 ⊢ A ∈ ℝ * ∧ B ∈ 0 +∞ → A ≤ A + 𝑒 B