Theorem ltaddneg

Description: Adding a negative number to another number decreases it. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		ltadd2	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 0 ↔ ( 𝐵 + 𝐴 ) < ( 𝐵 + 0 ) ) )
3	1 2	mp3an2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 0 ↔ ( 𝐵 + 𝐴 ) < ( 𝐵 + 0 ) ) )
4		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
5	4	addridd	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 0 ) = 𝐵 )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 + 0 ) = 𝐵 )
7	6	breq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐵 + 𝐴 ) < ( 𝐵 + 0 ) ↔ ( 𝐵 + 𝐴 ) < 𝐵 ) )
8	3 7	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 0 ↔ ( 𝐵 + 𝐴 ) < 𝐵 ) )