Metamath Proof Explorer


Theorem xrlelttric

Description: Trichotomy law for extended reals. (Contributed by Thierry Arnoux, 12-Sep-2017)

Ref Expression
Assertion xrlelttric A*B*ABB<A

Proof

Step Hyp Ref Expression
1 pm2.1 ¬B<AB<A
2 xrlenlt A*B*AB¬B<A
3 2 orbi1d A*B*ABB<A¬B<AB<A
4 1 3 mpbiri A*B*ABB<A