Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-fl | Structured version Visualization version GIF version |
Description: Define the floor
(greatest integer less than or equal to) function. See
flval 13154 for its value, fllelt 13157 for its basic property, and flcl 13155
for
its closure. For example, (⌊‘(3 / 2)) =
1 while
(⌊‘-(3 / 2)) = -2 (ex-fl 28154).
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 |
---|---|
df-fl | ⊢ ⌊ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cfl 13150 | . 2 class ⌊ | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cr 10525 | . . 3 class ℝ | |
4 | vy | . . . . . . 7 setvar 𝑦 | |
5 | 4 | cv 1527 | . . . . . 6 class 𝑦 |
6 | 2 | cv 1527 | . . . . . 6 class 𝑥 |
7 | cle 10665 | . . . . . 6 class ≤ | |
8 | 5, 6, 7 | wbr 5058 | . . . . 5 wff 𝑦 ≤ 𝑥 |
9 | c1 10527 | . . . . . . 7 class 1 | |
10 | caddc 10529 | . . . . . . 7 class + | |
11 | 5, 9, 10 | co 7145 | . . . . . 6 class (𝑦 + 1) |
12 | clt 10664 | . . . . . 6 class < | |
13 | 6, 11, 12 | wbr 5058 | . . . . 5 wff 𝑥 < (𝑦 + 1) |
14 | 8, 13 | wa 396 | . . . 4 wff (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1)) |
15 | cz 11970 | . . . 4 class ℤ | |
16 | 14, 4, 15 | crio 7102 | . . 3 class (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1))) |
17 | 2, 3, 16 | cmpt 5138 | . 2 class (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1)))) |
18 | 1, 17 | wceq 1528 | 1 wff ⌊ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1)))) |
Colors of variables: wff setvar class |
This definition is referenced by: flval 13154 |
Copyright terms: Public domain | W3C validator |