Theorem xrlttri3

Description: Trichotomy law for 'less than' for extended reals. (Contributed by NM, 9-Feb-2006)

	Ref	Expression
Assertion	xrlttri3	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\leftrightarrow \left(\neg A<B\wedge \neg B<A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
2		sotrieq2	$$⊢\left(<\mathrm{Or}{ℝ}^{*}\wedge \left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\right)\to \left(A=B\leftrightarrow \left(\neg A<B\wedge \neg B<A\right)\right)$$
3	1 2	mpan	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\leftrightarrow \left(\neg A<B\wedge \neg B<A\right)\right)$$