Metamath Proof Explorer

Theorem addge02

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

Ref Expression
Assertion addge02 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ B ↔ A ≤ B + A

Proof

Step Hyp Ref Expression
1 addge01 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ B ↔ A ≤ A + B
2 recn ⊢ A ∈ ℝ → A ∈ ℂ
3 recn ⊢ B ∈ ℝ → B ∈ ℂ
4 addcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B = B + A
5 2 3 4 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B = B + A
6 5 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ A + B ↔ A ≤ B + A
7 1 6 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ B ↔ A ≤ B + A