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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
xadd0ge.b ⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
Assertion xadd0ge ( 𝜑 → 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) )

Proof

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