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

Definition df-fl 11233
 Description: Define the floor (greatest integer) function. See flval 11234 for its value, fllelt 11237 for its basic property, and flcl 11235 for its closure. For example, while (ex-fl 21786). 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 11232 . 2
2 vx . . 3
3 cr 9020 . . 3
4 vy . . . . . . 7
54cv 1652 . . . . . 6
62cv 1652 . . . . . 6
7 cle 9152 . . . . . 6
85, 6, 7wbr 4237 . . . . 5
9 c1 9022 . . . . . . 7
10 caddc 9024 . . . . . . 7
115, 9, 10co 6110 . . . . . 6
12 clt 9151 . . . . . 6
136, 11, 12wbr 4237 . . . . 5
148, 13wa 360 . . . 4
15 cz 10313 . . . 4
1614, 4, 15crio 6571 . . 3
172, 3, 16cmpt 4291 . 2
181, 17wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  flval  11234
 Copyright terms: Public domain W3C validator