Definition df-fl

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	$$⊢⌊.⌋=\left(x\in ℝ⟼\left(\iota y\in \mathbb{Z}|\left(y\le x\wedge x<y+1\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfl	$$class⌊.⌋$$
1		vx	$$setvarx$$
2		cr	$$classℝ$$
3		vy	$$setvary$$
4		cz	$$class\mathbb{Z}$$
5	3	cv	$$setvary$$
6		cle	$$class\le$$
7	1	cv	$$setvarx$$
8	5 7 6	wbr	$$wffy\le x$$
9		clt	$$class<$$
10		caddc	$$class+$$
11		c1	$$class1$$
12	5 11 10	co	$$class\left(y+1\right)$$
13	7 12 9	wbr	$$wffx<y+1$$
14	8 13	wa	$$wff\left(y\le x\wedge x<y+1\right)$$
15	14 3 4	crio	$$class\left(\iota y\in \mathbb{Z}|\left(y\le x\wedge x<y+1\right)\right)$$
16	1 2 15	cmpt	$$class\left(x\in ℝ⟼\left(\iota y\in \mathbb{Z}|\left(y\le x\wedge x<y+1\right)\right)\right)$$
17	0 16	wceq	$$wff⌊.⌋=\left(x\in ℝ⟼\left(\iota y\in \mathbb{Z}|\left(y\le x\wedge x<y+1\right)\right)\right)$$