This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( A e. RR -> ( A - ( |_ ` A ) ) <_ 1 )

Proof

Step Hyp Ref Expression
1 fraclt1 
 |-  ( A e. RR -> ( A - ( |_ ` A ) ) < 1 )
2 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
3 resubcl 
 |-  ( ( A e. RR /\ ( |_ ` A ) e. RR ) -> ( A - ( |_ ` A ) ) e. RR )
4 2 3 mpdan 
 |-  ( A e. RR -> ( A - ( |_ ` A ) ) e. RR )
5 1re 
 |-  1 e. RR
6 ltle 
 |-  ( ( ( A - ( |_ ` A ) ) e. RR /\ 1 e. RR ) -> ( ( A - ( |_ ` A ) ) < 1 -> ( A - ( |_ ` A ) ) <_ 1 ) )
7 4 5 6 sylancl 
 |-  ( A e. RR -> ( ( A - ( |_ ` A ) ) < 1 -> ( A - ( |_ ` A ) ) <_ 1 ) )
8 1 7 mpd 
 |-  ( A e. RR -> ( A - ( |_ ` A ) ) <_ 1 )