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

Definition df-fl 10920
Description: Define the floor (greatest integer) function. See flval 10921 for its value, fllelt 10924 for its basic property, and flcl 10922 for its closure. For example,  ( |_ `  ( 3  /  2
) )  =  1 while  ( |_ `  -u ( 3  /  2
) )  =  -u
2 (ex-fl 20810).

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 10919 . 2  class  |_
2 vx . . 3  set  x
3 cr 8732 . . 3  class  RR
4 vy . . . . . . 7  set  y
54cv 1623 . . . . . 6  class  y
62cv 1623 . . . . . 6  class  x
7 cle 8864 . . . . . 6  class  <_
85, 6, 7wbr 4025 . . . . 5  wff  y  <_  x
9 c1 8734 . . . . . . 7  class  1
10 caddc 8736 . . . . . . 7  class  +
115, 9, 10co 5820 . . . . . 6  class  ( y  +  1 )
12 clt 8863 . . . . . 6  class  <
136, 11, 12wbr 4025 . . . . 5  wff  x  < 
( y  +  1 )
148, 13wa 360 . . . 4  wff  ( y  <_  x  /\  x  <  ( y  +  1 ) )
15 cz 10020 . . . 4  class  ZZ
1614, 4, 15crio 6291 . . 3  class  ( iota_ y  e.  ZZ ( y  <_  x  /\  x  <  ( y  +  1 ) ) )
172, 3, 16cmpt 4079 . 2  class  ( x  e.  RR  |->  ( iota_ y  e.  ZZ ( y  <_  x  /\  x  <  ( y  +  1 ) ) ) )
181, 17wceq 1624 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  10921
  Copyright terms: Public domain W3C validator