This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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