Theorem xraddge02

Description: A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 28-Dec-2016)

	Ref	Expression
Assertion	xraddge02	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ 𝐵 → 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrleid	⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ 𝐴 )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → 𝐴 ≤ 𝐴 )
3		simpl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → 𝐴 ∈ ℝ* )
4		0xr	⊢ 0 ∈ ℝ*
5	3 4	jctir	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ∈ ℝ* ∧ 0 ∈ ℝ* ) )
6		xle2add	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 ∈ ℝ* ) ∧ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ) → ( ( 𝐴 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( 𝐴 +𝑒 0 ) ≤ ( 𝐴 +𝑒 𝐵 ) ) )
7	5 6	mpancom	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( 𝐴 +𝑒 0 ) ≤ ( 𝐴 +𝑒 𝐵 ) ) )
8	2 7	mpand	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ 𝐵 → ( 𝐴 +𝑒 0 ) ≤ ( 𝐴 +𝑒 𝐵 ) ) )
9		xaddrid	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 0 ) = 𝐴 )
10	9	breq1d	⊢ ( 𝐴 ∈ ℝ* → ( ( 𝐴 +𝑒 0 ) ≤ ( 𝐴 +𝑒 𝐵 ) ↔ 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) ) )
11	10	adantr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 +𝑒 0 ) ≤ ( 𝐴 +𝑒 𝐵 ) ↔ 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) ) )
12	8 11	sylibd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ 𝐵 → 𝐴 ≤ ( 𝐴 +𝑒 𝐵 ) ) )