Theorem ltaddnegr

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

	Ref	Expression
Assertion	ltaddnegr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 0 ↔ ( 𝐴 + 𝐵 ) < 𝐵 ) )

Proof

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