sn-ltaddneg

		Ref	Expression
	Assertion	sn-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		readdrid	$⊢ B \in ℝ \to B + 0 = B$
5	4	adantl	$⊢ (A \in ℝ \land B \in ℝ) \to B + 0 = B$
6	5	breq2d	$⊢ (A \in ℝ \land B \in ℝ) \to (B + A < B + 0 \leftrightarrow B + A < B)$
7	3 6	bitrd	$⊢ (A \in ℝ \land B \in ℝ) \to (A < 0 \leftrightarrow B + A < B)$

Metamath Proof Explorer