Definition df-fl 4622

Description: Define the floor (greatest integer) function. See flleltt 4625 for its basic property and flclt 4624 for its closure.

Assertion

Ref	Expression
df-fl	⊢ floor = {⟨x, y⟩∣(x ∈ ℝ ∧ y = ∪{z ∈ ℤ∣(z ≤ x ∧ x < (z + 1))})}

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Definition df-fl

Step	Hyp	Ref	Expression
1		cfl 4621	. 2 class floor
2		vx	. . . . . 6 set x
3	2	cv 1089	. . . . 5 class x
4		cr 4027	. . . . 5 class ℝ
5	3, 4	wcel 1092	. . . 4 wff x ∈ ℝ
6		vy	. . . . . 6 set y
7	6	cv 1089	. . . . 5 class y
8		vz	. . . . . . . . . 10 set z
9	8	cv 1089	. . . . . . . . 9 class z
10		cle 4092	. . . . . . . . 9 class ≤
11	9, 3, 10	wbr 2054	. . . . . . . 8 wff z ≤ x
12		c1 4029	. . . . . . . . . 10 class 1
13		caddc 4031	. . . . . . . . . 10 class +
14	9, 12, 13	co 3001	. . . . . . . . 9 class (z + 1)
15		clt 4033	. . . . . . . . 9 class <
16	3, 14, 15	wbr 2054	. . . . . . . 8 wff x < (z + 1)
17	11, 16	wa 196	. . . . . . 7 wff (z ≤ x ∧ x < (z + 1))
18		cz 4095	. . . . . . 7 class ℤ
19	17, 8, 18	crab 1204	. . . . . 6 class {z ∈ ℤ∣(z ≤ x ∧ x < (z + 1))}
20	19	cuni 1919	. . . . 5 class ∪{z ∈ ℤ∣(z ≤ x ∧ x < (z + 1))}
21	7, 20	wceq 1091	. . . 4 wff y = ∪{z ∈ ℤ∣(z ≤ x ∧ x < (z + 1))}
22	5, 21	wa 196	. . 3 wff (x ∈ ℝ ∧ y = ∪{z ∈ ℤ∣(z ≤ x ∧ x < (z + 1))})
23	22, 2, 6	copab 2055	. 2 class {⟨x, y⟩∣(x ∈ ℝ ∧ y = ∪{z ∈ ℤ∣(z ≤ x ∧ x < (z + 1))})}
24	1, 23	wceq 1091	1 wff floor = {⟨x, y⟩∣(x ∈ ℝ ∧ y = ∪{z ∈ ℤ∣(z ≤ x ∧ x < (z + 1))})}

This definition is referenced by:  flvalt 4623

metamath.org