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

Definition df-fl 11929
Description: Define the floor (greatest integer less than or equal to) function. See flval 11931 for its value, fllelt 11934 for its basic property, and flcl 11932 for its closure. For example, while (ex-fl 25168).

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 11927 . 2
2 vx . . 3
3 cr 9512 . . 3
4 vy . . . . . . 7
54cv 1394 . . . . . 6
62cv 1394 . . . . . 6
7 cle 9650 . . . . . 6
85, 6, 7wbr 4452 . . . . 5
9 c1 9514 . . . . . . 7
10 caddc 9516 . . . . . . 7
115, 9, 10co 6296 . . . . . 6
12 clt 9649 . . . . . 6
136, 11, 12wbr 4452 . . . . 5
148, 13wa 369 . . . 4
15 cz 10889 . . . 4
1614, 4, 15crio 6256 . . 3
172, 3, 16cmpt 4510 . 2
181, 17wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  flval  11931
  Copyright terms: Public domain W3C validator