Metamath Proof Explorer

Theorem sn-ltaddpos

Description: ltaddpos without ax-mulcom . (Contributed by SN, 13-Feb-2024)

Ref Expression
Assertion sn-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 readdrid ⊢ B ∈ ℝ → B + 0 = B
5 4 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + 0 = B
6 5 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + 0 < B + A ↔ B < B + A
7 3 6 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ↔ B < B + A