Metamath Proof Explorer

Theorem ltaddnegr

Description: Adding a negative number to another number decreases it. (Contributed by AV, 19-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 ltaddneg ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < 0 ↔ B + A < B
2 recn ⊢ B ∈ ℝ → B ∈ ℂ
3 recn ⊢ A ∈ ℝ → A ∈ ℂ
4 addcom ⊢ B ∈ ℂ ∧ A ∈ ℂ → B + A = A + B
5 2 3 4 syl2anr ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A = A + B
6 5 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A < B ↔ A + B < B
7 1 6 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < 0 ↔ A + B < B