Theorem xleneg

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

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

Proof

Step	Hyp	Ref	Expression
1		xltneg	$$⊢\left(B\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(B<A\leftrightarrow -A<-B\right)$$
2	1	ancoms	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(B<A\leftrightarrow -A<-B\right)$$
3	2	notbid	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(\neg B<A\leftrightarrow \neg -A<-B\right)$$
4		xrlenlt	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\le B\leftrightarrow \neg B<A\right)$$
5		xnegcl	$$⊢B\in {ℝ}^{*}\to -B\in {ℝ}^{*}$$
6		xnegcl	$$⊢A\in {ℝ}^{*}\to -A\in {ℝ}^{*}$$
7		xrlenlt	$$⊢\left(-B\in {ℝ}^{*}\wedge -A\in {ℝ}^{*}\right)\to \left(-B\le -A\leftrightarrow \neg -A<-B\right)$$
8	5 6 7	syl2anr	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-B\le -A\leftrightarrow \neg -A<-B\right)$$
9	3 4 8	3bitr4d	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\le B\leftrightarrow -B\le -A\right)$$