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	⊢ ( 𝜑 → 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) )