Theorem xlenegcon2

Description: Extended real version of lenegcon2 . (Contributed by Glauco Siliprandi, 23-Apr-2023)

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

Proof

Step	Hyp	Ref	Expression
1		xnegcl	$$⊢B\in {ℝ}^{*}\to -B\in {ℝ}^{*}$$
2		xleneg	$$⊢\left(A\in {ℝ}^{*}\wedge -B\in {ℝ}^{*}\right)\to \left(A\le -B\leftrightarrow -\left(-B\right)\le -A\right)$$
3	1 2	sylan2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\le -B\leftrightarrow -\left(-B\right)\le -A\right)$$
4		xnegneg	$$⊢B\in {ℝ}^{*}\to -\left(-B\right)=B$$
5	4	breq1d	$$⊢B\in {ℝ}^{*}\to \left(-\left(-B\right)\le -A\leftrightarrow B\le -A\right)$$
6	5	adantl	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-\left(-B\right)\le -A\leftrightarrow B\le -A\right)$$
7	3 6	bitrd	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\le -B\leftrightarrow B\le -A\right)$$