Metamath Proof Explorer

Theorem xrlttri3

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

Ref Expression
Assertion xrlttri3 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )

Proof

Step Hyp Ref Expression
1 xrltso 
 |-  < Or RR*
2 sotrieq2 
 |-  ( ( < Or RR* /\ ( A e. RR* /\ B e. RR* ) ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
3 1 2 mpan 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )