Metamath Proof Explorer


Theorem xrletri

Description: Trichotomy law for extended reals. (Contributed by NM, 7-Feb-2007)

Ref Expression
Assertion xrletri A * B * A B B A

Proof

Step Hyp Ref Expression
1 xrltnle B * A * B < A ¬ A B
2 1 ancoms A * B * B < A ¬ A B
3 xrltle B * A * B < A B A
4 3 ancoms A * B * B < A B A
5 2 4 sylbird A * B * ¬ A B B A
6 5 orrd A * B * A B B A