Metamath Proof Explorer

Theorem ceicl

Description: The ceiling function returns an integer (closure law). (Contributed by Jeff Hankins, 10-Jun-2007)

Ref Expression
Assertion ceicl 
|- ( A e. RR -> -u ( |_ ` -u A ) e. ZZ )

Proof

Step Hyp Ref Expression
1 renegcl 
 |-  ( A e. RR -> -u A e. RR )
2 1 flcld 
 |-  ( A e. RR -> ( |_ ` -u A ) e. ZZ )
3 2 znegcld 
 |-  ( A e. RR -> -u ( |_ ` -u A ) e. ZZ )