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 ) ) )