Theorem ltnle

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005)

	Ref	Expression
Assertion	ltnle	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow \neg B\le A\right)$$

Proof

Step	Hyp	Ref	Expression
1		lenlt	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(B\le A\leftrightarrow \neg A<B\right)$$
2	1	ancoms	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B\le A\leftrightarrow \neg A<B\right)$$
3	2	con2bid	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow \neg B\le A\right)$$