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≤zx≤y
16 14 15 mpanr1 ⊢A∈ℝ∧z∈ℤ|A≤z≠∅→∃!x∈z∈ℤ|A≤z∀y∈z∈ℤ|A≤zx≤y
17 11 16 mpdan ⊢A∈ℝ→∃!x∈z∈ℤ|A≤z∀y∈z∈ℤ|A≤zx≤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≤zx≤y↔∀y∈ℤA≤y→x≤y
22 19 21 anbi12i ⊢x∈z∈ℤ|A≤z∧∀y∈z∈ℤ|A≤zx≤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≤zx≤y↔x∈ℤ∧A≤x∧∀y∈ℤA≤y→x≤y
25 24 eubii ⊢∃!xx∈z∈ℤ|A≤z∧∀y∈z∈ℤ|A≤zx≤y↔∃!xx∈ℤ∧A≤x∧∀y∈ℤA≤y→x≤y
26 df-reu ⊢∃!x∈z∈ℤ|A≤z∀y∈z∈ℤ|A≤zx≤y↔∃!xx∈z∈ℤ|A≤z∧∀y∈z∈ℤ|A≤zx≤y
27 df-reu ⊢∃!x∈ℤA≤x∧∀y∈ℤA≤y→x≤y↔∃!xx∈ℤ∧A≤x∧∀y∈ℤA≤y→x≤y
28 25 26 27 3bitr4i ⊢∃!x∈z∈ℤ|A≤z∀y∈z∈ℤ|A≤zx≤y↔∃!x∈ℤA≤x∧∀y∈ℤA≤y→x≤y
29 17 28 sylib ⊢A∈ℝ→∃!x∈ℤA≤x∧∀y∈ℤA≤y→x≤y