Theorem ltnegcon1

Description: Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004)

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

Proof

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