Metamath Proof Explorer

Theorem flidm

Description: The floor function is idempotent. (Contributed by NM, 17-Aug-2008)

Ref Expression
Assertion flidm 
|- ( A e. RR -> ( |_ ` ( |_ ` A ) ) = ( |_ ` A ) )

Proof

Step Hyp Ref Expression
1 flcl 
 |-  ( A e. RR -> ( |_ ` A ) e. ZZ )
2 flid 
 |-  ( ( |_ ` A ) e. ZZ -> ( |_ ` ( |_ ` A ) ) = ( |_ ` A ) )
3 1 2 syl 
 |-  ( A e. RR -> ( |_ ` ( |_ ` A ) ) = ( |_ ` A ) )