Metamath Proof Explorer

Theorem fraclt1

Description: The fractional part of a real number is less than one. (Contributed by NM, 15-Jul-2008)

Ref Expression
Assertion fraclt1 
|- ( A e. RR -> ( A - ( |_ ` A ) ) < 1 )

Proof

Step Hyp Ref Expression
1 flltp1 
 |-  ( A e. RR -> A < ( ( |_ ` A ) + 1 ) )
2 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
3 1re 
 |-  1 e. RR
4 ltsubadd2 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. RR /\ 1 e. RR ) -> ( ( A - ( |_ ` A ) ) < 1 <-> A < ( ( |_ ` A ) + 1 ) ) )
5 3 4 mp3an3 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. RR ) -> ( ( A - ( |_ ` A ) ) < 1 <-> A < ( ( |_ ` A ) + 1 ) ) )
6 2 5 mpdan 
 |-  ( A e. RR -> ( ( A - ( |_ ` A ) ) < 1 <-> A < ( ( |_ ` A ) + 1 ) ) )
7 1 6 mpbird 
 |-  ( A e. RR -> ( A - ( |_ ` A ) ) < 1 )