Metamath Proof Explorer

Theorem ltaddpos

Description: Adding a positive number to another number increases it. (Contributed by NM, 17-Nov-2004)

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

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 ltadd2 ⊢ 0 ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ↔ B + 0 < B + A
3 1 2 mp3an1 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ↔ B + 0 < B + A
4 recn ⊢ B ∈ ℝ → B ∈ ℂ
5 4 addid1d ⊢ B ∈ ℝ → B + 0 = B
6 5 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + 0 = B
7 6 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + 0 < B + A ↔ B < B + A
8 3 7 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ↔ B < B + A