Metamath Proof Explorer


Definition df-ceil

Description: The ceiling (least integer greater than or equal to) function. Defined in ISO 80000-2:2009(E) operation 2-9.18 and the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4 . See ceilval for its value, ceilge and ceilm1lt for its basic properties, and ceilcl for its closure. For example, ( |^( 3 / 2 ) ) = 2 while ( |^-u ( 3 / 2 ) ) = -u 1 ( ex-ceil ).

The symbol |^ is inspired by the gamma shaped left bracket of the usual notation. (Contributed by David A. Wheeler, 19-May-2015)

Ref Expression
Assertion df-ceil . = x x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cceil class .
1 vx setvar x
2 cr class
3 cfl class .
4 1 cv setvar x
5 4 cneg class x
6 5 3 cfv class x
7 6 cneg class x
8 1 2 7 cmpt class x x
9 0 8 wceq wff . = x x