Theorem xrlttri2

Description: Trichotomy law for 'less than' for extended reals. (Contributed by NM, 10-Dec-2007)

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

Proof

Step	Hyp	Ref	Expression
1		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
2		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)$$
3	1 2	mpan	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\leftrightarrow \neg \left(A<B\vee B<A\right)\right)$$
4	3	bicomd	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(\neg \left(A<B\vee B<A\right)\leftrightarrow A=B\right)$$
5	4	necon1abid	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\ne B\leftrightarrow \left(A<B\vee B<A\right)\right)$$