Theorem xrltne

Description: 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006)

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

Proof

Step	Hyp	Ref	Expression
1		orc	$$⊢A<B\to \left(A<B\vee B<A\right)$$
2		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
3		sotrieq	$$⊢\left(<\mathrm{Or}{ℝ}^{*}\wedge \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\right)\to \left(A=B\leftrightarrow \neg \left(A<B\vee B<A\right)\right)$$
4	2 3	mpan	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\leftrightarrow \neg \left(A<B\vee B<A\right)\right)$$
5	4	necon2abid	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(\left(A<B\vee B<A\right)\leftrightarrow A\ne B\right)$$
6	1 5	imbitrid	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A<B\to A\ne B\right)$$
7	6	3impia	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge A<B\right)\to A\ne B$$
8	7	necomd	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge A<B\right)\to B\ne A$$