Definition df-fl 13886

Description: Define the floor (greatest integer less than or equal to) function. See flval 13888 for its value, fllelt 13891 for its basic property, and flcl 13889 for its closure. For example, (⌊‘(3 / 2)) = 1 while (⌊‘-(3 / 2)) = -2 (ex-fl 30967).

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	⊢ ⌊ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1))))

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-fl

Step	Hyp	Ref	Expression
1		cfl 13884	. 2 class ⌊
2		vx	. . 3 setvar 𝑥
3		cr 11156	. . 3 class ℝ
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1569	. . . . . 6 class 𝑦
6	2	cv 1569	. . . . . 6 class 𝑥
7		cle 11301	. . . . . 6 class ≤
8	5, 6, 7	wbr 5103	. . . . 5 wff 𝑦 ≤ 𝑥
9		c1 11158	. . . . . . 7 class 1
10		caddc 11160	. . . . . . 7 class +
11	5, 9, 10	co 7409	. . . . . 6 class (𝑦 + 1)
12		clt 11300	. . . . . 6 class <
13	6, 11, 12	wbr 5103	. . . . 5 wff 𝑥 < (𝑦 + 1)
14	8, 13	wa 401	. . . 4 wff (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1))
15		cz 12648	. . . 4 class ℤ
16	14, 4, 15	crio 7365	. . 3 class (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1)))
17	2, 3, 16	cmpt 5186	. 2 class (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1))))
18	1, 17	wceq 1570	1 wff ⌊ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℤ (𝑦 ≤ 𝑥 ∧ 𝑥 < (𝑦 + 1))))

This definition is used by:  flval  13888