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 ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )

Proof

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