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