This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xadd0ge

Description: A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses xadd0ge.a ⊢ φ → A ∈ ℝ *
xadd0ge.b ⊢ φ → B ∈ 0 +∞
Assertion xadd0ge ⊢ φ → A ≤ A + 𝑒 B

Proof

Step Hyp Ref Expression
1 xadd0ge.a ⊢ φ → A ∈ ℝ *
2 xadd0ge.b ⊢ φ → B ∈ 0 +∞
3 xaddrid ⊢ A ∈ ℝ * → A + 𝑒 0 = A
4 1 3 syl ⊢ φ → A + 𝑒 0 = A
5 4 eqcomd ⊢ φ → A = A + 𝑒 0
6 0xr ⊢ 0 ∈ ℝ *
7 6 a1i ⊢ φ → 0 ∈ ℝ *
8 1 7 jca ⊢ φ → A ∈ ℝ * ∧ 0 ∈ ℝ *
9 iccssxr ⊢ 0 +∞ ⊆ ℝ *
10 9 2 sselid ⊢ φ → B ∈ ℝ *
11 1 10 jca ⊢ φ → A ∈ ℝ * ∧ B ∈ ℝ *
12 8 11 jca ⊢ φ → A ∈ ℝ * ∧ 0 ∈ ℝ * ∧ A ∈ ℝ * ∧ B ∈ ℝ *
13 1 xrleidd ⊢ φ → A ≤ A
14 pnfxr ⊢ +∞ ∈ ℝ *
15 14 a1i ⊢ φ → +∞ ∈ ℝ *
16 iccgelb ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ B ∈ 0 +∞ → 0 ≤ B
17 7 15 2 16 syl3anc ⊢ φ → 0 ≤ B
18 13 17 jca ⊢ φ → A ≤ A ∧ 0 ≤ B
19 xle2add ⊢ A ∈ ℝ * ∧ 0 ∈ ℝ * ∧ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ A ∧ 0 ≤ B → A + 𝑒 0 ≤ A + 𝑒 B
20 12 18 19 sylc ⊢ φ → A + 𝑒 0 ≤ A + 𝑒 B
21 5 20 eqbrtrd ⊢ φ → A ≤ A + 𝑒 B