Metamath Proof Explorer


Theorem supxrltinfxr

Description: The supremum of the empty set is strictly smaller than the infimum of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion supxrltinfxr
|- sup ( (/) , RR* , < ) < inf ( (/) , RR* , < )

Proof

Step Hyp Ref Expression
1 mnfltpnf
 |-  -oo < +oo
2 xrsup0
 |-  sup ( (/) , RR* , < ) = -oo
3 xrinf0
 |-  inf ( (/) , RR* , < ) = +oo
4 1 2 3 3brtr4i
 |-  sup ( (/) , RR* , < ) < inf ( (/) , RR* , < )