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