Metamath Proof Explorer

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 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ B ↔ A ≤ A + B

Proof

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