Metamath Proof Explorer


Theorem xrltlen

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015)

Ref Expression
Assertion xrltlen A * B * A < B A B B A

Proof

Step Hyp Ref Expression
1 xrlttri A * B * A < B ¬ A = B B < A
2 ioran ¬ A = B B < A ¬ A = B ¬ B < A
3 2 biancomi ¬ A = B B < A ¬ B < A ¬ A = B
4 1 3 bitrdi A * B * A < B ¬ B < A ¬ A = B
5 xrlenlt A * B * A B ¬ B < A
6 nesym B A ¬ A = B
7 6 a1i A * B * B A ¬ A = B
8 5 7 anbi12d A * B * A B B A ¬ B < A ¬ A = B
9 4 8 bitr4d A * B * A < B A B B A