Theorem leneg2d

Description: Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	leneg2d.1	$$⊢\phi \to A\in ℝ$$
	leneg2d.2	$$⊢\phi \to B\in ℝ$$
Assertion	leneg2d	$$⊢\phi \to \left(A\le -B\leftrightarrow B\le -A\right)$$

Proof

Step	Hyp	Ref	Expression
1		leneg2d.1	$$⊢\phi \to A\in ℝ$$
2		leneg2d.2	$$⊢\phi \to B\in ℝ$$
3	2	renegcld	$$⊢\phi \to -B\in ℝ$$
4	1 3	lenegd	$$⊢\phi \to \left(A\le -B\leftrightarrow -\left(-B\right)\le -A\right)$$
5	2	recnd	$$⊢\phi \to B\in ℂ$$
6	5	negnegd	$$⊢\phi \to -\left(-B\right)=B$$
7	6	breq1d	$$⊢\phi \to \left(-\left(-B\right)\le -A\leftrightarrow B\le -A\right)$$
8	4 7	bitrd	$$⊢\phi \to \left(A\le -B\leftrightarrow B\le -A\right)$$