ltaddneg

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

		Ref	Expression
	Assertion	ltaddneg	$⊢ (A \in ℝ \land B \in ℝ) \to (A < 0 \leftrightarrow B + A < B)$

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		ltadd2	$⊢ (A \in ℝ \land 0 \in ℝ \land B \in ℝ) \to (A < 0 \leftrightarrow B + A < B + 0)$
3	1 2	mp3an2	$⊢ (A \in ℝ \land B \in ℝ) \to (A < 0 \leftrightarrow B + A < B + 0)$
4		recn	$⊢ B \in ℝ \to B \in ℂ$
5	4	addridd	$⊢ B \in ℝ \to B + 0 = B$
6	5	adantl	$⊢ (A \in ℝ \land B \in ℝ) \to B + 0 = B$
7	6	breq2d	$⊢ (A \in ℝ \land B \in ℝ) \to (B + A < B + 0 \leftrightarrow B + A < B)$
8	3 7	bitrd	$⊢ (A \in ℝ \land B \in ℝ) \to (A < 0 \leftrightarrow B + A < B)$

Metamath Proof Explorer