Theorem addge01

Description: A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 21-Feb-2005)

	Ref	Expression
Assertion	addge01	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ 𝐵 ↔ 𝐴 ≤ ( 𝐴 + 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		leadd2	⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐵 ↔ ( 𝐴 + 0 ) ≤ ( 𝐴 + 𝐵 ) ) )
3	1 2	mp3an1	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐵 ↔ ( 𝐴 + 0 ) ≤ ( 𝐴 + 𝐵 ) ) )
4	3	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ 𝐵 ↔ ( 𝐴 + 0 ) ≤ ( 𝐴 + 𝐵 ) ) )
5		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
6	5	addid1d	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 0 ) = 𝐴 )
7	6	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 0 ) = 𝐴 )
8	7	breq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 0 ) ≤ ( 𝐴 + 𝐵 ) ↔ 𝐴 ≤ ( 𝐴 + 𝐵 ) ) )
9	4 8	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ 𝐵 ↔ 𝐴 ≤ ( 𝐴 + 𝐵 ) ) )