Theorem flval2

Description: An alternate way to define the floor (greatest integer) function. (Contributed by NM, 16-Nov-2004)

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

Proof

Step	Hyp	Ref	Expression
1		flle	|- ( A e. RR -> ( |_ ` A ) <_ A )
2		flge	|- ( ( A e. RR /\ y e. ZZ ) -> ( y <_ A <-> y <_ ( |_ ` A ) ) )
3	2	biimpd	|- ( ( A e. RR /\ y e. ZZ ) -> ( y <_ A -> y <_ ( |_ ` A ) ) )
4	3	ralrimiva	|- ( A e. RR -> A. y e. ZZ ( y <_ A -> y <_ ( |_ ` A ) ) )
5		flcl	|- ( A e. RR -> ( |_ ` A ) e. ZZ )
6		zmax	|- ( A e. RR -> E! x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) )
7		breq1	|- ( x = ( |_ ` A ) -> ( x <_ A <-> ( |_ ` A ) <_ A ) )
8		breq2	|- ( x = ( |_ ` A ) -> ( y <_ x <-> y <_ ( |_ ` A ) ) )
9	8	imbi2d	|- ( x = ( |_ ` A ) -> ( ( y <_ A -> y <_ x ) <-> ( y <_ A -> y <_ ( |_ ` A ) ) ) )
10	9	ralbidv	|- ( x = ( |_ ` A ) -> ( A. y e. ZZ ( y <_ A -> y <_ x ) <-> A. y e. ZZ ( y <_ A -> y <_ ( |_ ` A ) ) ) )
11	7 10	anbi12d	|- ( x = ( |_ ` A ) -> ( ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) <-> ( ( |_ ` A ) <_ A /\ A. y e. ZZ ( y <_ A -> y <_ ( |_ ` A ) ) ) ) )
12	11	riota2	|- ( ( ( |_ ` A ) e. ZZ /\ E! x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) -> ( ( ( |_ ` A ) <_ A /\ A. y e. ZZ ( y <_ A -> y <_ ( |_ ` A ) ) ) <-> ( iota_ x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) = ( |_ ` A ) ) )
13	5 6 12	syl2anc	|- ( A e. RR -> ( ( ( |_ ` A ) <_ A /\ A. y e. ZZ ( y <_ A -> y <_ ( |_ ` A ) ) ) <-> ( iota_ x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) = ( |_ ` A ) ) )
14	1 4 13	mpbi2and	|- ( A e. RR -> ( iota_ x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) = ( |_ ` A ) )
15	14	eqcomd	|- ( A e. RR -> ( |_ ` A ) = ( iota_ x e. ZZ ( x <_ A /\ A. y e. ZZ ( y <_ A -> y <_ x ) ) ) )