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 e. RR -> E! x e. ZZ ( A <_ x /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) )

Proof

Step Hyp Ref Expression
1 nnssz
 |-  NN C_ ZZ
2 arch
 |-  ( A e. RR -> E. z e. NN A < z )
3 ssrexv
 |-  ( NN C_ ZZ -> ( E. z e. NN A < z -> E. z e. ZZ A < z ) )
4 1 2 3 mpsyl
 |-  ( A e. RR -> E. z e. ZZ A < z )
5 zre
 |-  ( z e. ZZ -> z e. RR )
6 ltle
 |-  ( ( A e. RR /\ z e. RR ) -> ( A < z -> A <_ z ) )
7 5 6 sylan2
 |-  ( ( A e. RR /\ z e. ZZ ) -> ( A < z -> A <_ z ) )
8 7 reximdva
 |-  ( A e. RR -> ( E. z e. ZZ A < z -> E. z e. ZZ A <_ z ) )
9 4 8 mpd
 |-  ( A e. RR -> E. z e. ZZ A <_ z )
10 rabn0
 |-  ( { z e. ZZ | A <_ z } =/= (/) <-> E. z e. ZZ A <_ z )
11 9 10 sylibr
 |-  ( A e. RR -> { z e. ZZ | A <_ z } =/= (/) )
12 breq2
 |-  ( z = n -> ( A <_ z <-> A <_ n ) )
13 12 cbvrabv
 |-  { z e. ZZ | A <_ z } = { n e. ZZ | A <_ n }
14 13 eqimssi
 |-  { z e. ZZ | A <_ z } C_ { n e. ZZ | A <_ n }
15 uzwo3
 |-  ( ( A e. RR /\ ( { z e. ZZ | A <_ z } C_ { n e. ZZ | A <_ n } /\ { z e. ZZ | A <_ z } =/= (/) ) ) -> E! x e. { z e. ZZ | A <_ z } A. y e. { z e. ZZ | A <_ z } x <_ y )
16 14 15 mpanr1
 |-  ( ( A e. RR /\ { z e. ZZ | A <_ z } =/= (/) ) -> E! x e. { z e. ZZ | A <_ z } A. y e. { z e. ZZ | A <_ z } x <_ y )
17 11 16 mpdan
 |-  ( A e. RR -> E! x e. { z e. ZZ | A <_ z } A. y e. { z e. ZZ | A <_ z } x <_ y )
18 breq2
 |-  ( z = x -> ( A <_ z <-> A <_ x ) )
19 18 elrab
 |-  ( x e. { z e. ZZ | A <_ z } <-> ( x e. ZZ /\ A <_ x ) )
20 breq2
 |-  ( z = y -> ( A <_ z <-> A <_ y ) )
21 20 ralrab
 |-  ( A. y e. { z e. ZZ | A <_ z } x <_ y <-> A. y e. ZZ ( A <_ y -> x <_ y ) )
22 19 21 anbi12i
 |-  ( ( x e. { z e. ZZ | A <_ z } /\ A. y e. { z e. ZZ | A <_ z } x <_ y ) <-> ( ( x e. ZZ /\ A <_ x ) /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) )
23 anass
 |-  ( ( ( x e. ZZ /\ A <_ x ) /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) <-> ( x e. ZZ /\ ( A <_ x /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) ) )
24 22 23 bitri
 |-  ( ( x e. { z e. ZZ | A <_ z } /\ A. y e. { z e. ZZ | A <_ z } x <_ y ) <-> ( x e. ZZ /\ ( A <_ x /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) ) )
25 24 eubii
 |-  ( E! x ( x e. { z e. ZZ | A <_ z } /\ A. y e. { z e. ZZ | A <_ z } x <_ y ) <-> E! x ( x e. ZZ /\ ( A <_ x /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) ) )
26 df-reu
 |-  ( E! x e. { z e. ZZ | A <_ z } A. y e. { z e. ZZ | A <_ z } x <_ y <-> E! x ( x e. { z e. ZZ | A <_ z } /\ A. y e. { z e. ZZ | A <_ z } x <_ y ) )
27 df-reu
 |-  ( E! x e. ZZ ( A <_ x /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) <-> E! x ( x e. ZZ /\ ( A <_ x /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) ) )
28 25 26 27 3bitr4i
 |-  ( E! x e. { z e. ZZ | A <_ z } A. y e. { z e. ZZ | A <_ z } x <_ y <-> E! x e. ZZ ( A <_ x /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) )
29 17 28 sylib
 |-  ( A e. RR -> E! x e. ZZ ( A <_ x /\ A. y e. ZZ ( A <_ y -> x <_ y ) ) )