Metamath Proof Explorer


Theorem flval3

Description: An alternate way to define the floor 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 , < ) )