Metamath Proof Explorer


Theorem xrleloe

Description: 'Less than or equal' expressed in terms of 'less than' or 'equals', for extended reals. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion xrleloe A * B * A B A < B A = B

Proof

Step Hyp Ref Expression
1 xrlenlt A * B * A B ¬ B < A
2 eqcom B = A A = B
3 2 orbi1i B = A A < B A = B A < B
4 orcom A = B A < B A < B A = B
5 3 4 bitri B = A A < B A < B A = B
6 xrlttri B * A * B < A ¬ B = A A < B
7 6 ancoms A * B * B < A ¬ B = A A < B
8 7 con2bid A * B * B = A A < B ¬ B < A
9 5 8 syl5rbbr A * B * ¬ B < A A < B A = B
10 1 9 bitrd A * B * A B A < B A = B