Metamath Proof Explorer

Theorem zmin

Description: There is a unique smallest integer greater than or equal to a given real number. (Contributed by NM, 12-Nov-2004) (Revised by Mario Carneiro, 13-Jun-2014)

Ref Expression
Assertion zmin ⊢ A ∈ ℝ → ∃! x ∈ ℤ A ≤ x ∧ ∀ y ∈ ℤ A ≤ y → x ≤ y

Proof

Step Hyp Ref Expression
1 nnssz ⊢ ℕ ⊆ ℤ
2 arch ⊢ A ∈ ℝ → ∃ z ∈ ℕ A < z
3 ssrexv ⊢ ℕ ⊆ ℤ → ∃ z ∈ ℕ A < z → ∃ z ∈ ℤ A < z
4 1 2 3 mpsyl ⊢ A ∈ ℝ → ∃ z ∈ ℤ A < z
5 zre ⊢ z ∈ ℤ → z ∈ ℝ
6 ltle ⊢ A ∈ ℝ ∧ z ∈ ℝ → A < z → A ≤ z
7 5 6 sylan2 ⊢ A ∈ ℝ ∧ z ∈ ℤ → A < z → A ≤ z
8 7 reximdva ⊢ A ∈ ℝ → ∃ z ∈ ℤ A < z → ∃ z ∈ ℤ A ≤ z
9 4 8 mpd ⊢ A ∈ ℝ → ∃ z ∈ ℤ A ≤ z
10 rabn0 ⊢ z ∈ ℤ | A ≤ z ≠ ∅ ↔ ∃ z ∈ ℤ A ≤ z
11 9 10 sylibr ⊢ A ∈ ℝ → z ∈ ℤ | A ≤ z ≠ ∅
12 breq2 ⊢ z = n → A ≤ z ↔ A ≤ n
13 12 cbvrabv ⊢ z ∈ ℤ | A ≤ z = n ∈ ℤ | A ≤ n
14 13 eqimssi ⊢ z ∈ ℤ | A ≤ z ⊆ n ∈ ℤ | A ≤ n
15 uzwo3 ⊢ A ∈ ℝ ∧ z ∈ ℤ | A ≤ z ⊆ n ∈ ℤ | A ≤ n ∧ z ∈ ℤ | A ≤ z ≠ ∅ → ∃! x ∈ z ∈ ℤ | A ≤ z ∀ y ∈ z ∈ ℤ | A ≤ z x ≤ y
16 14 15 mpanr1 ⊢ A ∈ ℝ ∧ z ∈ ℤ | A ≤ z ≠ ∅ → ∃! x ∈ z ∈ ℤ | A ≤ z ∀ y ∈ z ∈ ℤ | A ≤ z x ≤ y
17 11 16 mpdan ⊢ A ∈ ℝ → ∃! x ∈ z ∈ ℤ | A ≤ z ∀ y ∈ z ∈ ℤ | A ≤ z x ≤ y
18 breq2 ⊢ z = x → A ≤ z ↔ A ≤ x
19 18 elrab ⊢ x ∈ z ∈ ℤ | A ≤ z ↔ x ∈ ℤ ∧ A ≤ x
20 breq2 ⊢ z = y → A ≤ z ↔ A ≤ y
21 20 ralrab ⊢ ∀ y ∈ z ∈ ℤ | A ≤ z x ≤ y ↔ ∀ y ∈ ℤ A ≤ y → x ≤ y
22 19 21 anbi12i ⊢ x ∈ z ∈ ℤ | A ≤ z ∧ ∀ y ∈ z ∈ ℤ | A ≤ z x ≤ y ↔ x ∈ ℤ ∧ A ≤ x ∧ ∀ y ∈ ℤ A ≤ y → x ≤ y
23 anass ⊢ x ∈ ℤ ∧ A ≤ x ∧ ∀ y ∈ ℤ A ≤ y → x ≤ y ↔ x ∈ ℤ ∧ A ≤ x ∧ ∀ y ∈ ℤ A ≤ y → x ≤ y
24 22 23 bitri ⊢ x ∈ z ∈ ℤ | A ≤ z ∧ ∀ y ∈ z ∈ ℤ | A ≤ z x ≤ y ↔ x ∈ ℤ ∧ A ≤ x ∧ ∀ y ∈ ℤ A ≤ y → x ≤ y
25 24 eubii ⊢ ∃! x x ∈ z ∈ ℤ | A ≤ z ∧ ∀ y ∈ z ∈ ℤ | A ≤ z x ≤ y ↔ ∃! x x ∈ ℤ ∧ A ≤ x ∧ ∀ y ∈ ℤ A ≤ y → x ≤ y
26 df-reu ⊢ ∃! x ∈ z ∈ ℤ | A ≤ z ∀ y ∈ z ∈ ℤ | A ≤ z x ≤ y ↔ ∃! x x ∈ z ∈ ℤ | A ≤ z ∧ ∀ y ∈ z ∈ ℤ | A ≤ z x ≤ y
27 df-reu ⊢ ∃! x ∈ ℤ A ≤ x ∧ ∀ y ∈ ℤ A ≤ y → x ≤ y ↔ ∃! x x ∈ ℤ ∧ A ≤ x ∧ ∀ y ∈ ℤ A ≤ y → x ≤ y
28 25 26 27 3bitr4i ⊢ ∃! x ∈ z ∈ ℤ | A ≤ z ∀ y ∈ z ∈ ℤ | A ≤ z x ≤ y ↔ ∃! x ∈ ℤ A ≤ x ∧ ∀ y ∈ ℤ A ≤ y → x ≤ y
29 17 28 sylib ⊢ A ∈ ℝ → ∃! x ∈ ℤ A ≤ x ∧ ∀ y ∈ ℤ A ≤ y → x ≤ y