MPE Home 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,  ( |_ `  ( 3  /  2
) )  =  1 while  ( |_ `  -u ( 3  /  2
) )  =  -u
2 (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  |-  |_  =  ( 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 11232 . 2  class  |_
2 vx . . 3  set  x
3 cr 9020 . . 3  class  RR
4 vy . . . . . . 7  set  y
54cv 1652 . . . . . 6  class  y
62cv 1652 . . . . . 6  class  x
7 cle 9152 . . . . . 6  class  <_
85, 6, 7wbr 4237 . . . . 5  wff  y  <_  x
9 c1 9022 . . . . . . 7  class  1
10 caddc 9024 . . . . . . 7  class  +
115, 9, 10co 6110 . . . . . 6  class  ( y  +  1 )
12 clt 9151 . . . . . 6  class  <
136, 11, 12wbr 4237 . . . . 5  wff  x  < 
( y  +  1 )
148, 13wa 360 . . . 4  wff  ( y  <_  x  /\  x  <  ( y  +  1 ) )
15 cz 10313 . . . 4  class  ZZ
1614, 4, 15crio 6571 . . 3  class  ( iota_ y  e.  ZZ ( y  <_  x  /\  x  <  ( y  +  1 ) ) )
172, 3, 16cmpt 4291 . 2  class  ( x  e.  RR  |->  ( iota_ y  e.  ZZ ( y  <_  x  /\  x  <  ( y  +  1 ) ) ) )
181, 17wceq 1653 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  11234
  Copyright terms: Public domain W3C validator