Metamath Proof Explorer

Theorem reflcl

Description: The floor (greatest integer) function is real. (Contributed by NM, 15-Jul-2008)

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

Proof

Step Hyp Ref Expression
1 flcl 
 |-  ( A e. RR -> ( |_ ` A ) e. ZZ )
2 1 zred 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )