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 | ⊢ ⌊ = ( 𝑥 ∈ ℝ ↦ ( ℩ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝑥 ∧ 𝑥 < ( 𝑦 + 1 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cfl | ⊢ ⌊ | |
| 1 | vx | ⊢ 𝑥 | |
| 2 | cr | ⊢ ℝ | |
| 3 | vy | ⊢ 𝑦 | |
| 4 | cz | ⊢ ℤ | |
| 5 | 3 | cv | ⊢ 𝑦 |
| 6 | cle | ⊢ ≤ | |
| 7 | 1 | cv | ⊢ 𝑥 |
| 8 | 5 7 6 | wbr | ⊢ 𝑦 ≤ 𝑥 |
| 9 | clt | ⊢ < | |
| 10 | caddc | ⊢ + | |
| 11 | c1 | ⊢ 1 | |
| 12 | 5 11 10 | co | ⊢ ( 𝑦 + 1 ) |
| 13 | 7 12 9 | wbr | ⊢ 𝑥 < ( 𝑦 + 1 ) |
| 14 | 8 13 | wa | ⊢ ( 𝑦 ≤ 𝑥 ∧ 𝑥 < ( 𝑦 + 1 ) ) |
| 15 | 14 3 4 | crio | ⊢ ( ℩ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝑥 ∧ 𝑥 < ( 𝑦 + 1 ) ) ) |
| 16 | 1 2 15 | cmpt | ⊢ ( 𝑥 ∈ ℝ ↦ ( ℩ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝑥 ∧ 𝑥 < ( 𝑦 + 1 ) ) ) ) |
| 17 | 0 16 | wceq | ⊢ ⌊ = ( 𝑥 ∈ ℝ ↦ ( ℩ 𝑦 ∈ ℤ ( 𝑦 ≤ 𝑥 ∧ 𝑥 < ( 𝑦 + 1 ) ) ) ) |