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 )