Metamath Proof Explorer

Theorem ltaddpos2

Description: Adding a positive number to another number increases it. (Contributed by NM, 8-Apr-2005)

Ref Expression
Assertion ltaddpos2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ↔ B < A + B

Proof

Step Hyp Ref Expression
1 ltaddpos ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ↔ B < B + A
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 ∈ ℝ → B < A + B ↔ B < B + A
7 1 6 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ↔ B < A + B