Theorem xltneg

Description: Extended real version of ltneg . (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xltneg	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A<B\leftrightarrow -B<-A\right)$$

Proof

Step	Hyp	Ref	Expression
1		xltnegi	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge A<B\right)\to -B<-A$$
2	1	3expia	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A<B\to -B<-A\right)$$
3		xnegcl	$$⊢B\in {ℝ}^{*}\to -B\in {ℝ}^{*}$$
4		xnegcl	$$⊢A\in {ℝ}^{*}\to -A\in {ℝ}^{*}$$
5		xltnegi	$$⊢\left(-B\in {ℝ}^{*}\wedge -A\in {ℝ}^{*}\wedge -B<-A\right)\to -\left(-A\right)<-\left(-B\right)$$
6	5	3expia	$$⊢\left(-B\in {ℝ}^{*}\wedge -A\in {ℝ}^{*}\right)\to \left(-B<-A\to -\left(-A\right)<-\left(-B\right)\right)$$
7	3 4 6	syl2anr	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-B<-A\to -\left(-A\right)<-\left(-B\right)\right)$$
8		xnegneg	$$⊢A\in {ℝ}^{*}\to -\left(-A\right)=A$$
9		xnegneg	$$⊢B\in {ℝ}^{*}\to -\left(-B\right)=B$$
10	8 9	breqan12d	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-\left(-A\right)<-\left(-B\right)\leftrightarrow A<B\right)$$
11	7 10	sylibd	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-B<-A\to A<B\right)$$
12	2 11	impbid	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A<B\leftrightarrow -B<-A\right)$$