Metamath Proof Explorer


Theorem xrlenlt

Description: "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion xrlenlt A * B * A B ¬ B < A

Proof

Step Hyp Ref Expression
1 df-br A B A B
2 opelxpi A * B * A B * × *
3 df-le = * × * < -1
4 3 eleq2i A B A B * × * < -1
5 eldif A B * × * < -1 A B * × * ¬ A B < -1
6 4 5 bitri A B A B * × * ¬ A B < -1
7 6 baib A B * × * A B ¬ A B < -1
8 2 7 syl A * B * A B ¬ A B < -1
9 1 8 syl5bb A * B * A B ¬ A B < -1
10 opelcnvg A * B * A B < -1 B A <
11 df-br B < A B A <
12 10 11 syl6rbbr A * B * B < A A B < -1
13 12 notbid A * B * ¬ B < A ¬ A B < -1
14 9 13 bitr4d A * B * A B ¬ B < A