Theorem xrleltne

Description: 'Less than or equal to' implies 'less than' is not 'equals', for extended reals. (Contributed by NM, 9-Feb-2006)

	Ref	Expression
Assertion	xrleltne	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge A\le B\right)\to \left(A<B\leftrightarrow B\ne A\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrlttri3	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\leftrightarrow \left(\neg A<B\wedge \neg B<A\right)\right)$$
2		simpl	$$⊢\left(\neg A<B\wedge \neg B<A\right)\to \neg A<B$$
3	1 2	biimtrdi	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\to \neg A<B\right)$$
4	3	adantr	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge A\le B\right)\to \left(A=B\to \neg A<B\right)$$
5		xrleloe	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\le B\leftrightarrow \left(A<B\vee A=B\right)\right)$$
6	5	biimpa	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge A\le B\right)\to \left(A<B\vee A=B\right)$$
7	6	ord	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge A\le B\right)\to \left(\neg A<B\to A=B\right)$$
8	4 7	impbid	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge A\le B\right)\to \left(A=B\leftrightarrow \neg A<B\right)$$
9	8	necon2abid	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge A\le B\right)\to \left(A<B\leftrightarrow A\ne B\right)$$
10		necom	$$⊢B\ne A\leftrightarrow A\ne B$$
11	9 10	bitr4di	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge A\le B\right)\to \left(A<B\leftrightarrow B\ne A\right)$$
12	11	3impa	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge A\le B\right)\to \left(A<B\leftrightarrow B\ne A\right)$$