Theorem xrltlen

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015)

	Ref	Expression
Assertion	xrltlen	$$⊢\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		xrlttri	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A<B\leftrightarrow \neg \left(A=B\vee B<A\right)\right)$$
2		ioran	$$⊢\neg \left(A=B\vee B<A\right)\leftrightarrow \left(\neg A=B\wedge \neg B<A\right)$$
3	2	biancomi	$$⊢\neg \left(A=B\vee B<A\right)\leftrightarrow \left(\neg B<A\wedge \neg A=B\right)$$
4	1 3	bitrdi	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A<B\leftrightarrow \left(\neg B<A\wedge \neg A=B\right)\right)$$
5		xrlenlt	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\le B\leftrightarrow \neg B<A\right)$$
6		nesym	$$⊢B\ne A\leftrightarrow \neg A=B$$
7	6	a1i	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(B\ne A\leftrightarrow \neg A=B\right)$$
8	5 7	anbi12d	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(\left(A\le B\wedge B\ne A\right)\leftrightarrow \left(\neg B<A\wedge \neg A=B\right)\right)$$
9	4 8	bitr4d	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A<B\leftrightarrow \left(A\le B\wedge B\ne A\right)\right)$$