Theorem xrletri3

Description: Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009)

	Ref	Expression
Assertion	xrletri3	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\leftrightarrow \left(A\le B\wedge B\le A\right)\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	1	biancomd	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\leftrightarrow \left(\neg B<A\wedge \neg A<B\right)\right)$$
3		xrlenlt	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\le B\leftrightarrow \neg B<A\right)$$
4		xrlenlt	$$⊢\left(B\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(B\le A\leftrightarrow \neg A<B\right)$$
5	4	ancoms	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(B\le A\leftrightarrow \neg A<B\right)$$
6	3 5	anbi12d	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(\left(A\le B\wedge B\le A\right)\leftrightarrow \left(\neg B<A\wedge \neg A<B\right)\right)$$
7	2 6	bitr4d	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\leftrightarrow \left(A\le B\wedge B\le A\right)\right)$$