Theorem flval

Description: Value of the floor (greatest integer) function. The floor of A is the (unique) integer less than or equal to A whose successor is strictly greater than A . (Contributed by NM, 14-Nov-2004) (Revised by Mario Carneiro, 2-Nov-2013)

	Ref	Expression
Assertion	flval	|- ( A e. RR -> ( |_ ` A ) = ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	|- ( y = A -> ( x <_ y <-> x <_ A ) )
2		breq1	|- ( y = A -> ( y < ( x + 1 ) <-> A < ( x + 1 ) ) )
3	1 2	anbi12d	|- ( y = A -> ( ( x <_ y /\ y < ( x + 1 ) ) <-> ( x <_ A /\ A < ( x + 1 ) ) ) )
4	3	riotabidv	|- ( y = A -> ( iota_ x e. ZZ ( x <_ y /\ y < ( x + 1 ) ) ) = ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) )
5		df-fl	|- |_ = ( y e. RR |-> ( iota_ x e. ZZ ( x <_ y /\ y < ( x + 1 ) ) ) )
6		riotaex	|- ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) e. _V
7	4 5 6	fvmpt	|- ( A e. RR -> ( |_ ` A ) = ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) )