Metamath Proof Explorer

Theorem ceilcl

Description: Closure of the ceiling function. (Contributed by David A. Wheeler, 19-May-2015)

Ref Expression
Assertion ceilcl 
|- ( A e. RR -> ( |^ ` A ) e. ZZ )

Proof

Step Hyp Ref Expression
1 ceilval 
 |-  ( A e. RR -> ( |^ ` A ) = -u ( |_ ` -u A ) )
2 ceicl 
 |-  ( A e. RR -> -u ( |_ ` -u A ) e. ZZ )
3 1 2 eqeltrd 
 |-  ( A e. RR -> ( |^ ` A ) e. ZZ )