Metamath Proof Explorer


Theorem fracle1

Description: The fractional part of a real number is less than or equal to one. (Contributed by Mario Carneiro, 21-May-2016)

Ref Expression
Assertion fracle1 AAA1

Proof

Step Hyp Ref Expression
1 fraclt1 AAA<1
2 reflcl AA
3 resubcl AAAA
4 2 3 mpdan AAA
5 1re 1
6 ltle AA1AA<1AA1
7 4 5 6 sylancl AAA<1AA1
8 1 7 mpd AAA1