Metamath Proof Explorer


Theorem xrlenltd

Description: "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses xrlenltd.a φ A *
xrlenltd.b φ B *
Assertion xrlenltd φ A B ¬ B < A

Proof

Step Hyp Ref Expression
1 xrlenltd.a φ A *
2 xrlenltd.b φ B *
3 xrlenlt A * B * A B ¬ B < A
4 1 2 3 syl2anc φ A B ¬ B < A