Theorem ltnegcon2

Description: Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 25-Feb-2015)

	Ref	Expression
Assertion	ltnegcon2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<-B\leftrightarrow B<-A\right)$$

Proof

Step	Hyp	Ref	Expression
1		renegcl	$$⊢B\in ℝ\to -B\in ℝ$$
2		ltneg	$$⊢\left(A\in ℝ\wedge -B\in ℝ\right)\to \left(A<-B\leftrightarrow -\left(-B\right)<-A\right)$$
3	1 2	sylan2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<-B\leftrightarrow -\left(-B\right)<-A\right)$$
4		simpr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B\in ℝ$$
5	4	recnd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B\in ℂ$$
6	5	negnegd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to -\left(-B\right)=B$$
7	6	breq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(-\left(-B\right)<-A\leftrightarrow B<-A\right)$$
8	3 7	bitrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<-B\leftrightarrow B<-A\right)$$