Theorem lenegcon2

Description: Contraposition of negative in 'less than or equal to'. (Contributed by NM, 8-Oct-2005)

	Ref	Expression
Assertion	lenegcon2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le -B\leftrightarrow B\le -A\right)$$

Proof

Step	Hyp	Ref	Expression
1		renegcl	$$⊢B\in ℝ\to -B\in ℝ$$
2		leneg	$$⊢\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		recn	$$⊢B\in ℝ\to B\in ℂ$$
5	4	negnegd	$$⊢B\in ℝ\to -\left(-B\right)=B$$
6	5	adantl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to -\left(-B\right)=B$$
7	6	breq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(-\left(-B\right)\le -A\leftrightarrow B\le -A\right)$$
8	3 7	bitrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le -B\leftrightarrow B\le -A\right)$$