Theorem ltlen

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999)

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

Proof

Step	Hyp	Ref	Expression
1		ltle	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\to A\le B\right)$$
2		ltne	$$⊢\left(A\in ℝ\wedge A<B\right)\to B\ne A$$
3	2	ex	$$⊢A\in ℝ\to \left(A<B\to B\ne A\right)$$
4	3	adantr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\to B\ne A\right)$$
5	1 4	jcad	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\to \left(A\le B\wedge B\ne A\right)\right)$$
6		leloe	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le B\leftrightarrow \left(A<B\vee A=B\right)\right)$$
7		df-ne	$$⊢B\ne A\leftrightarrow \neg B=A$$
8		pm2.24	$$⊢B=A\to \left(\neg B=A\to A<B\right)$$
9	8	eqcoms	$$⊢A=B\to \left(\neg B=A\to A<B\right)$$
10	7 9	biimtrid	$$⊢A=B\to \left(B\ne A\to A<B\right)$$
11	10	jao1i	$$⊢\left(A<B\vee A=B\right)\to \left(B\ne A\to A<B\right)$$
12	6 11	biimtrdi	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A\le B\to \left(B\ne A\to A<B\right)\right)$$
13	12	impd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(\left(A\le B\wedge B\ne A\right)\to A<B\right)$$
14	5 13	impbid	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow \left(A\le B\wedge B\ne A\right)\right)$$