Metamath Proof Explorer


Theorem lbzbi

Description: If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion lbzbi
|- ( A C_ RR -> ( E. x e. RR A. y e. A x <_ y <-> E. x e. ZZ A. y e. A x <_ y ) )

Proof

Step Hyp Ref Expression
1 nfv
 |-  F/ x A C_ RR
2 nfre1
 |-  F/ x E. x e. ZZ A. y e. A x <_ y
3 btwnz
 |-  ( x e. RR -> ( E. z e. ZZ z < x /\ E. z e. ZZ x < z ) )
4 3 simpld
 |-  ( x e. RR -> E. z e. ZZ z < x )
5 ssel2
 |-  ( ( A C_ RR /\ y e. A ) -> y e. RR )
6 zre
 |-  ( z e. ZZ -> z e. RR )
7 ltleletr
 |-  ( ( z e. RR /\ x e. RR /\ y e. RR ) -> ( ( z < x /\ x <_ y ) -> z <_ y ) )
8 6 7 syl3an1
 |-  ( ( z e. ZZ /\ x e. RR /\ y e. RR ) -> ( ( z < x /\ x <_ y ) -> z <_ y ) )
9 8 expd
 |-  ( ( z e. ZZ /\ x e. RR /\ y e. RR ) -> ( z < x -> ( x <_ y -> z <_ y ) ) )
10 9 3expia
 |-  ( ( z e. ZZ /\ x e. RR ) -> ( y e. RR -> ( z < x -> ( x <_ y -> z <_ y ) ) ) )
11 5 10 syl5
 |-  ( ( z e. ZZ /\ x e. RR ) -> ( ( A C_ RR /\ y e. A ) -> ( z < x -> ( x <_ y -> z <_ y ) ) ) )
12 11 expdimp
 |-  ( ( ( z e. ZZ /\ x e. RR ) /\ A C_ RR ) -> ( y e. A -> ( z < x -> ( x <_ y -> z <_ y ) ) ) )
13 12 com23
 |-  ( ( ( z e. ZZ /\ x e. RR ) /\ A C_ RR ) -> ( z < x -> ( y e. A -> ( x <_ y -> z <_ y ) ) ) )
14 13 imp
 |-  ( ( ( ( z e. ZZ /\ x e. RR ) /\ A C_ RR ) /\ z < x ) -> ( y e. A -> ( x <_ y -> z <_ y ) ) )
15 14 ralrimiv
 |-  ( ( ( ( z e. ZZ /\ x e. RR ) /\ A C_ RR ) /\ z < x ) -> A. y e. A ( x <_ y -> z <_ y ) )
16 ralim
 |-  ( A. y e. A ( x <_ y -> z <_ y ) -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) )
17 15 16 syl
 |-  ( ( ( ( z e. ZZ /\ x e. RR ) /\ A C_ RR ) /\ z < x ) -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) )
18 17 ex
 |-  ( ( ( z e. ZZ /\ x e. RR ) /\ A C_ RR ) -> ( z < x -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) ) )
19 18 anasss
 |-  ( ( z e. ZZ /\ ( x e. RR /\ A C_ RR ) ) -> ( z < x -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) ) )
20 19 expcom
 |-  ( ( x e. RR /\ A C_ RR ) -> ( z e. ZZ -> ( z < x -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) ) ) )
21 20 com23
 |-  ( ( x e. RR /\ A C_ RR ) -> ( z < x -> ( z e. ZZ -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) ) ) )
22 21 imp
 |-  ( ( ( x e. RR /\ A C_ RR ) /\ z < x ) -> ( z e. ZZ -> ( A. y e. A x <_ y -> A. y e. A z <_ y ) ) )
23 22 imdistand
 |-  ( ( ( x e. RR /\ A C_ RR ) /\ z < x ) -> ( ( z e. ZZ /\ A. y e. A x <_ y ) -> ( z e. ZZ /\ A. y e. A z <_ y ) ) )
24 breq1
 |-  ( x = z -> ( x <_ y <-> z <_ y ) )
25 24 ralbidv
 |-  ( x = z -> ( A. y e. A x <_ y <-> A. y e. A z <_ y ) )
26 25 rspcev
 |-  ( ( z e. ZZ /\ A. y e. A z <_ y ) -> E. x e. ZZ A. y e. A x <_ y )
27 23 26 syl6
 |-  ( ( ( x e. RR /\ A C_ RR ) /\ z < x ) -> ( ( z e. ZZ /\ A. y e. A x <_ y ) -> E. x e. ZZ A. y e. A x <_ y ) )
28 27 ex
 |-  ( ( x e. RR /\ A C_ RR ) -> ( z < x -> ( ( z e. ZZ /\ A. y e. A x <_ y ) -> E. x e. ZZ A. y e. A x <_ y ) ) )
29 28 com23
 |-  ( ( x e. RR /\ A C_ RR ) -> ( ( z e. ZZ /\ A. y e. A x <_ y ) -> ( z < x -> E. x e. ZZ A. y e. A x <_ y ) ) )
30 29 ancomsd
 |-  ( ( x e. RR /\ A C_ RR ) -> ( ( A. y e. A x <_ y /\ z e. ZZ ) -> ( z < x -> E. x e. ZZ A. y e. A x <_ y ) ) )
31 30 expdimp
 |-  ( ( ( x e. RR /\ A C_ RR ) /\ A. y e. A x <_ y ) -> ( z e. ZZ -> ( z < x -> E. x e. ZZ A. y e. A x <_ y ) ) )
32 31 rexlimdv
 |-  ( ( ( x e. RR /\ A C_ RR ) /\ A. y e. A x <_ y ) -> ( E. z e. ZZ z < x -> E. x e. ZZ A. y e. A x <_ y ) )
33 32 anasss
 |-  ( ( x e. RR /\ ( A C_ RR /\ A. y e. A x <_ y ) ) -> ( E. z e. ZZ z < x -> E. x e. ZZ A. y e. A x <_ y ) )
34 33 expcom
 |-  ( ( A C_ RR /\ A. y e. A x <_ y ) -> ( x e. RR -> ( E. z e. ZZ z < x -> E. x e. ZZ A. y e. A x <_ y ) ) )
35 4 34 mpdi
 |-  ( ( A C_ RR /\ A. y e. A x <_ y ) -> ( x e. RR -> E. x e. ZZ A. y e. A x <_ y ) )
36 35 ex
 |-  ( A C_ RR -> ( A. y e. A x <_ y -> ( x e. RR -> E. x e. ZZ A. y e. A x <_ y ) ) )
37 36 com23
 |-  ( A C_ RR -> ( x e. RR -> ( A. y e. A x <_ y -> E. x e. ZZ A. y e. A x <_ y ) ) )
38 1 2 37 rexlimd
 |-  ( A C_ RR -> ( E. x e. RR A. y e. A x <_ y -> E. x e. ZZ A. y e. A x <_ y ) )
39 zssre
 |-  ZZ C_ RR
40 ssrexv
 |-  ( ZZ C_ RR -> ( E. x e. ZZ A. y e. A x <_ y -> E. x e. RR A. y e. A x <_ y ) )
41 39 40 ax-mp
 |-  ( E. x e. ZZ A. y e. A x <_ y -> E. x e. RR A. y e. A x <_ y )
42 38 41 impbid1
 |-  ( A C_ RR -> ( E. x e. RR A. y e. A x <_ y <-> E. x e. ZZ A. y e. A x <_ y ) )