MPE Home 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,  ( |_ `  ( 3  /  2
) )  =  1 while  ( |_ `  -u ( 3  /  2
) )  =  -u
2 (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  |-  |_  =  ( x  e.  RR  |->  ( iota_ y  e.  ZZ ( y  <_  x  /\  x  <  ( y  +  1 ) ) ) )
Distinct variable group:    x, y

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