Metamath Proof Explorer


Theorem xeqlelt

Description: Equality in terms of 'less than or equal to', 'less than'. (Contributed by Thierry Arnoux, 5-Jul-2017)

Ref Expression
Assertion xeqlelt A * B * A = B A B ¬ A < B

Proof

Step Hyp Ref Expression
1 xrletri3 A * B * A = B A B B A
2 xrlenlt B * A * B A ¬ A < B
3 2 ancoms A * B * B A ¬ A < B
4 3 anbi2d A * B * A B B A A B ¬ A < B
5 1 4 bitrd A * B * A = B A B ¬ A < B