Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fl Unicode version

Definition df-fl 11157
 Description: Define the floor (greatest integer) function. See flval 11158 for its value, fllelt 11161 for its basic property, and flcl 11159 for its closure. For example, while (ex-fl 21708). The term "floor" was coined by Ken Iverson. He also invented a mathematical notation for floor, consisting of an L-shaped left bracket and its reflection as a right bracket. In APL, the left-bracket alone is used, and we borrow this idea. (Thanks to Paul Chapman for this information.) (Contributed by NM, 14-Nov-2004.)
Assertion
Ref Expression
df-fl
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-fl
StepHypRef Expression
1 cfl 11156 . 2
2 vx . . 3
3 cr 8945 . . 3
4 vy . . . . . . 7
54cv 1648 . . . . . 6
62cv 1648 . . . . . 6
7 cle 9077 . . . . . 6
85, 6, 7wbr 4172 . . . . 5
9 c1 8947 . . . . . . 7
10 caddc 8949 . . . . . . 7
115, 9, 10co 6040 . . . . . 6
12 clt 9076 . . . . . 6
136, 11, 12wbr 4172 . . . . 5
148, 13wa 359 . . . 4
15 cz 10238 . . . 4
1614, 4, 15crio 6501 . . 3
172, 3, 16cmpt 4226 . 2
181, 17wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  flval  11158
 Copyright terms: Public domain W3C validator