Theorem lenegcon1

Description: Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004)

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

Proof

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