Metamath Proof Explorer

Theorem xrlttri2

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

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

Proof

Step Hyp Ref Expression
1 xrltso 
 |-  < Or RR*
2 sotrieq 
 |-  ( ( < 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 ) ) )
4 3 bicomd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. ( A < B \/ B < A ) <-> A = B ) )
5 4 necon1abid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A =/= B <-> ( A < B \/ B < A ) ) )