This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )