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 xaddid1 ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 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 sseldi ( 𝜑𝐵 ∈ ℝ* )
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 ( 𝜑𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) )