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 ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℤ ( 𝐴𝑥 ∧ ∀ 𝑦 ∈ ℤ ( 𝐴𝑦𝑥𝑦 ) ) )

Proof

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