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 x y y < x

Proof

Step Hyp Ref Expression
1 breq1 y = x 1 y < x x 1 < x
2 peano2rem x x 1
3 ltm1 x x 1 < x
4 1 2 3 rspcedvdw x y y < x
5 4 rgen x y y < x