Theorem xlenegcon1

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

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

Proof

Step	Hyp	Ref	Expression
1		xnegcl	$$⊢A\in {ℝ}^{*}\to -A\in {ℝ}^{*}$$
2		xleneg	$$⊢\left(-A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-A\le B\leftrightarrow -B\le -\left(-A\right)\right)$$
3	1 2	sylan	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-A\le B\leftrightarrow -B\le -\left(-A\right)\right)$$
4		xnegneg	$$⊢A\in {ℝ}^{*}\to -\left(-A\right)=A$$
5	4	breq2d	$$⊢A\in {ℝ}^{*}\to \left(-B\le -\left(-A\right)\leftrightarrow -B\le A\right)$$
6	5	adantr	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-B\le -\left(-A\right)\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)$$