Metamath Proof Explorer


Theorem reltre

Description: For all real numbers there is a smaller real number. (Contributed by AV, 5-Sep-2020)

Ref Expression
Assertion reltre xyy<x

Proof

Step Hyp Ref Expression
1 peano2rem xx1
2 breq1 y=x1y<xx1<x
3 2 adantl xy=x1y<xx1<x
4 ltm1 xx1<x
5 1 3 4 rspcedvd xyy<x
6 5 rgen xyy<x