Metamath Proof Explorer

Theorem flval3

Description: An alternate way to define the floor (greatest integer) function, as the supremum of all integers less than or equal to its argument. (Contributed by NM, 15-Nov-2004) (Proof shortened by Mario Carneiro, 6-Sep-2014)

Ref Expression
Assertion flval3 
|- ( A e. RR -> ( |_ ` A ) = sup ( { x e. ZZ | x <_ A } , RR , < ) )

Proof

Step Hyp Ref Expression
1 ssrab2 
 |-  { x e. ZZ | x <_ A } C_ ZZ
2 zssre 
 |-  ZZ C_ RR
3 1 2 sstri 
 |-  { x e. ZZ | x <_ A } C_ RR
4 3 a1i 
 |-  ( A e. RR -> { x e. ZZ | x <_ A } C_ RR )
5 breq1 
 |-  ( x = ( |_ ` A ) -> ( x <_ A <-> ( |_ ` A ) <_ A ) )
6 flcl 
 |-  ( A e. RR -> ( |_ ` A ) e. ZZ )
7 flle 
 |-  ( A e. RR -> ( |_ ` A ) <_ A )
8 5 6 7 elrabd 
 |-  ( A e. RR -> ( |_ ` A ) e. { x e. ZZ | x <_ A } )
9 8 ne0d 
 |-  ( A e. RR -> { x e. ZZ | x <_ A } =/= (/) )
10 reflcl 
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
11 breq1 
 |-  ( x = z -> ( x <_ A <-> z <_ A ) )
12 11 elrab 
 |-  ( z e. { x e. ZZ | x <_ A } <-> ( z e. ZZ /\ z <_ A ) )
13 flge 
 |-  ( ( A e. RR /\ z e. ZZ ) -> ( z <_ A <-> z <_ ( |_ ` A ) ) )
14 13 biimpd 
 |-  ( ( A e. RR /\ z e. ZZ ) -> ( z <_ A -> z <_ ( |_ ` A ) ) )
15 14 expimpd 
 |-  ( A e. RR -> ( ( z e. ZZ /\ z <_ A ) -> z <_ ( |_ ` A ) ) )
16 12 15 syl5bi 
 |-  ( A e. RR -> ( z e. { x e. ZZ | x <_ A } -> z <_ ( |_ ` A ) ) )
17 16 ralrimiv 
 |-  ( A e. RR -> A. z e. { x e. ZZ | x <_ A } z <_ ( |_ ` A ) )
18 brralrspcev 
 |-  ( ( ( |_ ` A ) e. RR /\ A. z e. { x e. ZZ | x <_ A } z <_ ( |_ ` A ) ) -> E. y e. RR A. z e. { x e. ZZ | x <_ A } z <_ y )
19 10 17 18 syl2anc 
 |-  ( A e. RR -> E. y e. RR A. z e. { x e. ZZ | x <_ A } z <_ y )
20 4 9 19 8 suprubd 
 |-  ( A e. RR -> ( |_ ` A ) <_ sup ( { x e. ZZ | x <_ A } , RR , < ) )
21 suprleub 
 |-  ( ( ( { x e. ZZ | x <_ A } C_ RR /\ { x e. ZZ | x <_ A } =/= (/) /\ E. y e. RR A. z e. { x e. ZZ | x <_ A } z <_ y ) /\ ( |_ ` A ) e. RR ) -> ( sup ( { x e. ZZ | x <_ A } , RR , < ) <_ ( |_ ` A ) <-> A. z e. { x e. ZZ | x <_ A } z <_ ( |_ ` A ) ) )
22 4 9 19 10 21 syl31anc 
 |-  ( A e. RR -> ( sup ( { x e. ZZ | x <_ A } , RR , < ) <_ ( |_ ` A ) <-> A. z e. { x e. ZZ | x <_ A } z <_ ( |_ ` A ) ) )
23 17 22 mpbird 
 |-  ( A e. RR -> sup ( { x e. ZZ | x <_ A } , RR , < ) <_ ( |_ ` A ) )
24 4 9 19 suprcld 
 |-  ( A e. RR -> sup ( { x e. ZZ | x <_ A } , RR , < ) e. RR )
25 10 24 letri3d 
 |-  ( A e. RR -> ( ( |_ ` A ) = sup ( { x e. ZZ | x <_ A } , RR , < ) <-> ( ( |_ ` A ) <_ sup ( { x e. ZZ | x <_ A } , RR , < ) /\ sup ( { x e. ZZ | x <_ A } , RR , < ) <_ ( |_ ` A ) ) ) )
26 20 23 25 mpbir2and 
 |-  ( A e. RR -> ( |_ ` A ) = sup ( { x e. ZZ | x <_ A } , RR , < ) )