Metamath Proof Explorer

Theorem sn-ltaddneg

Description: ltaddneg without ax-mulcom . (Contributed by SN, 25-Jan-2025)

Ref Expression
Assertion sn-ltaddneg ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < 0 ↔ B + A < B

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 ltadd2 ⊢ A ∈ ℝ ∧ 0 ∈ ℝ ∧ B ∈ ℝ → A < 0 ↔ B + A < B + 0
3 1 2 mp3an2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < 0 ↔ B + A < B + 0
4 readdrid ⊢ B ∈ ℝ → B + 0 = B
5 4 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + 0 = B
6 5 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A < B + 0 ↔ B + A < B
7 3 6 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < 0 ↔ B + A < B