Mathbox for David A. Wheeler 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > dfceiling  Unicode version 
Description: The ceiling function.
Defined in ISO 800002:2009(E) operation 29.18 and
the "NIST Digital Library of Mathematical Functions" , front
introduction,
"Common Notations and Definitions" section at
http://dlmf.nist.gov/front/introduction#Sx4.
By convention metamath users tend to expand this construct directly, instead of using the definition. However, we want to make sure this is separately and formally defined. Proof ceicl 10971 shows that the ceiling function returns an integer when provided a real. Formalized by David A. Wheeler. (Contributed by David A. Wheeler, 19May2015.) 
Ref  Expression 

dfceiling  ⌈ 
Step  Hyp  Ref  Expression 

1  ccei 28507  . 2 ⌈  
2  vx  . . 3  
3  cr 8752  . . 3  
4  2  cv 1631  . . . . . 6 
5  4  cneg 9054  . . . . 5 
6  cfl 10940  . . . . 5  
7  5, 6  cfv 5271  . . . 4 
8  7  cneg 9054  . . 3 
9  2, 3, 8  cmpt 4093  . 2 
10  1, 9  wceq 1632  1 ⌈ 
Colors of variables: wff set class 
This definition is referenced by: ceilingval 28509 
Copyright terms: Public domain  W3C validator 