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 ⊆ ℝ → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ↔ ∃ x ∈ ℤ ∀ y ∈ A x ≤ y

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ x A ⊆ ℝ
2 nfre1 ⊢ Ⅎ x ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
3 btwnz ⊢ x ∈ ℝ → ∃ z ∈ ℤ z < x ∧ ∃ z ∈ ℤ x < z
4 3 simpld ⊢ x ∈ ℝ → ∃ z ∈ ℤ z < x
5 ssel2 ⊢ A ⊆ ℝ ∧ y ∈ A → y ∈ ℝ
6 zre ⊢ z ∈ ℤ → z ∈ ℝ
7 ltleletr ⊢ z ∈ ℝ ∧ x ∈ ℝ ∧ y ∈ ℝ → z < x ∧ x ≤ y → z ≤ y
8 6 7 syl3an1 ⊢ z ∈ ℤ ∧ x ∈ ℝ ∧ y ∈ ℝ → z < x ∧ x ≤ y → z ≤ y
9 8 expd ⊢ z ∈ ℤ ∧ x ∈ ℝ ∧ y ∈ ℝ → z < x → x ≤ y → z ≤ y
10 9 3expia ⊢ z ∈ ℤ ∧ x ∈ ℝ → y ∈ ℝ → z < x → x ≤ y → z ≤ y
11 5 10 syl5 ⊢ z ∈ ℤ ∧ x ∈ ℝ → A ⊆ ℝ ∧ y ∈ A → z < x → x ≤ y → z ≤ y
12 11 expdimp ⊢ z ∈ ℤ ∧ x ∈ ℝ ∧ A ⊆ ℝ → y ∈ A → z < x → x ≤ y → z ≤ y
13 12 com23 ⊢ z ∈ ℤ ∧ x ∈ ℝ ∧ A ⊆ ℝ → z < x → y ∈ A → x ≤ y → z ≤ y
14 13 imp ⊢ z ∈ ℤ ∧ x ∈ ℝ ∧ A ⊆ ℝ ∧ z < x → y ∈ A → x ≤ y → z ≤ y
15 14 ralrimiv ⊢ z ∈ ℤ ∧ x ∈ ℝ ∧ A ⊆ ℝ ∧ z < x → ∀ y ∈ A x ≤ y → z ≤ y
16 ralim ⊢ ∀ y ∈ A x ≤ y → z ≤ y → ∀ y ∈ A x ≤ y → ∀ y ∈ A z ≤ y
17 15 16 syl ⊢ z ∈ ℤ ∧ x ∈ ℝ ∧ A ⊆ ℝ ∧ z < x → ∀ y ∈ A x ≤ y → ∀ y ∈ A z ≤ y
18 17 ex ⊢ z ∈ ℤ ∧ x ∈ ℝ ∧ A ⊆ ℝ → z < x → ∀ y ∈ A x ≤ y → ∀ y ∈ A z ≤ y
19 18 anasss ⊢ z ∈ ℤ ∧ x ∈ ℝ ∧ A ⊆ ℝ → z < x → ∀ y ∈ A x ≤ y → ∀ y ∈ A z ≤ y
20 19 expcom ⊢ x ∈ ℝ ∧ A ⊆ ℝ → z ∈ ℤ → z < x → ∀ y ∈ A x ≤ y → ∀ y ∈ A z ≤ y
21 20 com23 ⊢ x ∈ ℝ ∧ A ⊆ ℝ → z < x → z ∈ ℤ → ∀ y ∈ A x ≤ y → ∀ y ∈ A z ≤ y
22 21 imp ⊢ x ∈ ℝ ∧ A ⊆ ℝ ∧ z < x → z ∈ ℤ → ∀ y ∈ A x ≤ y → ∀ y ∈ A z ≤ y
23 22 imdistand ⊢ x ∈ ℝ ∧ A ⊆ ℝ ∧ z < x → z ∈ ℤ ∧ ∀ y ∈ A x ≤ y → z ∈ ℤ ∧ ∀ y ∈ A z ≤ y
24 breq1 ⊢ x = z → x ≤ y ↔ z ≤ y
25 24 ralbidv ⊢ x = z → ∀ y ∈ A x ≤ y ↔ ∀ y ∈ A z ≤ y
26 25 rspcev ⊢ z ∈ ℤ ∧ ∀ y ∈ A z ≤ y → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
27 23 26 syl6 ⊢ x ∈ ℝ ∧ A ⊆ ℝ ∧ z < x → z ∈ ℤ ∧ ∀ y ∈ A x ≤ y → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
28 27 ex ⊢ x ∈ ℝ ∧ A ⊆ ℝ → z < x → z ∈ ℤ ∧ ∀ y ∈ A x ≤ y → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
29 28 com23 ⊢ x ∈ ℝ ∧ A ⊆ ℝ → z ∈ ℤ ∧ ∀ y ∈ A x ≤ y → z < x → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
30 29 ancomsd ⊢ x ∈ ℝ ∧ A ⊆ ℝ → ∀ y ∈ A x ≤ y ∧ z ∈ ℤ → z < x → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
31 30 expdimp ⊢ x ∈ ℝ ∧ A ⊆ ℝ ∧ ∀ y ∈ A x ≤ y → z ∈ ℤ → z < x → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
32 31 rexlimdv ⊢ x ∈ ℝ ∧ A ⊆ ℝ ∧ ∀ y ∈ A x ≤ y → ∃ z ∈ ℤ z < x → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
33 32 anasss ⊢ x ∈ ℝ ∧ A ⊆ ℝ ∧ ∀ y ∈ A x ≤ y → ∃ z ∈ ℤ z < x → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
34 33 expcom ⊢ A ⊆ ℝ ∧ ∀ y ∈ A x ≤ y → x ∈ ℝ → ∃ z ∈ ℤ z < x → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
35 4 34 mpdi ⊢ A ⊆ ℝ ∧ ∀ y ∈ A x ≤ y → x ∈ ℝ → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
36 35 ex ⊢ A ⊆ ℝ → ∀ y ∈ A x ≤ y → x ∈ ℝ → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
37 36 com23 ⊢ A ⊆ ℝ → x ∈ ℝ → ∀ y ∈ A x ≤ y → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
38 1 2 37 rexlimd ⊢ A ⊆ ℝ → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y
39 zssre ⊢ ℤ ⊆ ℝ
40 ssrexv ⊢ ℤ ⊆ ℝ → ∃ x ∈ ℤ ∀ y ∈ A x ≤ y → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y
41 39 40 ax-mp ⊢ ∃ x ∈ ℤ ∀ y ∈ A x ≤ y → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y
42 38 41 impbid1 ⊢ A ⊆ ℝ → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ↔ ∃ x ∈ ℤ ∀ y ∈ A x ≤ y