Description: Define the floor (greatest integer less than or equal to) function. See flval for its value, fllelt for its basic property, and flcl for its closure. For example, ( |_( 3 / 2 ) ) = 1 while ( |_-u ( 3 / 2 ) ) = -u 2 ( ex-fl ).
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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-fl | |- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cfl | |- |_ |
|
| 1 | vx | |- x |
|
| 2 | cr | |- RR |
|
| 3 | vy | |- y |
|
| 4 | cz | |- ZZ |
|
| 5 | 3 | cv | |- y |
| 6 | cle | |- <_ |
|
| 7 | 1 | cv | |- x |
| 8 | 5 7 6 | wbr | |- y <_ x |
| 9 | clt | |- < |
|
| 10 | caddc | |- + |
|
| 11 | c1 | |- 1 |
|
| 12 | 5 11 10 | co | |- ( y + 1 ) |
| 13 | 7 12 9 | wbr | |- x < ( y + 1 ) |
| 14 | 8 13 | wa | |- ( y <_ x /\ x < ( y + 1 ) ) |
| 15 | 14 3 4 | crio | |- ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) |
| 16 | 1 2 15 | cmpt | |- ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) ) |
| 17 | 0 16 | wceq | |- |_ = ( x e. RR |-> ( iota_ y e. ZZ ( y <_ x /\ x < ( y + 1 ) ) ) ) |