Metamath Proof Explorer

Theorem flo1

Description: The floor function satisfies |_ ( x ) = x + O(1) . (Contributed by Mario Carneiro, 21-May-2016)

Ref Expression
Assertion flo1 
|- ( x e. RR |-> ( x - ( |_ ` x ) ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 ssidd 
 |-  ( T. -> RR C_ RR )
2 reflcl 
 |-  ( x e. RR -> ( |_ ` x ) e. RR )
3 resubcl 
 |-  ( ( x e. RR /\ ( |_ ` x ) e. RR ) -> ( x - ( |_ ` x ) ) e. RR )
4 2 3 mpdan 
 |-  ( x e. RR -> ( x - ( |_ ` x ) ) e. RR )
5 4 recnd 
 |-  ( x e. RR -> ( x - ( |_ ` x ) ) e. CC )
6 5 adantl 
 |-  ( ( T. /\ x e. RR ) -> ( x - ( |_ ` x ) ) e. CC )
7 1red 
 |-  ( T. -> 1 e. RR )
8 id 
 |-  ( x e. RR -> x e. RR )
9 flle 
 |-  ( x e. RR -> ( |_ ` x ) <_ x )
10 2 8 9 abssubge0d 
 |-  ( x e. RR -> ( abs ` ( x - ( |_ ` x ) ) ) = ( x - ( |_ ` x ) ) )
11 fracle1 
 |-  ( x e. RR -> ( x - ( |_ ` x ) ) <_ 1 )
12 10 11 eqbrtrd 
 |-  ( x e. RR -> ( abs ` ( x - ( |_ ` x ) ) ) <_ 1 )
13 12 ad2antrl 
 |-  ( ( T. /\ ( x e. RR /\ 1 <_ x ) ) -> ( abs ` ( x - ( |_ ` x ) ) ) <_ 1 )
14 1 6 7 7 13 elo1d 
 |-  ( T. -> ( x e. RR |-> ( x - ( |_ ` x ) ) ) e. O(1) )
15 14 mptru 
 |-  ( x e. RR |-> ( x - ( |_ ` x ) ) ) e. O(1)