Metamath Proof Explorer


Theorem nnunb

Description: The set of positive integers is unbounded above. Theorem I.28 of Apostol p. 26. (Contributed by NM, 21-Jan-1997)

Ref Expression
Assertion nnunb
|- -. E. x e. RR A. y e. NN ( y < x \/ y = x )

Proof

Step Hyp Ref Expression
1 pm3.24
 |-  -. ( A. y e. NN -. x < y /\ -. A. y e. NN -. x < y )
2 peano2rem
 |-  ( x e. RR -> ( x - 1 ) e. RR )
3 ltm1
 |-  ( x e. RR -> ( x - 1 ) < x )
4 ovex
 |-  ( x - 1 ) e. _V
5 eleq1
 |-  ( y = ( x - 1 ) -> ( y e. RR <-> ( x - 1 ) e. RR ) )
6 breq1
 |-  ( y = ( x - 1 ) -> ( y < x <-> ( x - 1 ) < x ) )
7 breq1
 |-  ( y = ( x - 1 ) -> ( y < z <-> ( x - 1 ) < z ) )
8 7 rexbidv
 |-  ( y = ( x - 1 ) -> ( E. z e. NN y < z <-> E. z e. NN ( x - 1 ) < z ) )
9 6 8 imbi12d
 |-  ( y = ( x - 1 ) -> ( ( y < x -> E. z e. NN y < z ) <-> ( ( x - 1 ) < x -> E. z e. NN ( x - 1 ) < z ) ) )
10 5 9 imbi12d
 |-  ( y = ( x - 1 ) -> ( ( y e. RR -> ( y < x -> E. z e. NN y < z ) ) <-> ( ( x - 1 ) e. RR -> ( ( x - 1 ) < x -> E. z e. NN ( x - 1 ) < z ) ) ) )
11 4 10 spcv
 |-  ( A. y ( y e. RR -> ( y < x -> E. z e. NN y < z ) ) -> ( ( x - 1 ) e. RR -> ( ( x - 1 ) < x -> E. z e. NN ( x - 1 ) < z ) ) )
12 3 11 syl7
 |-  ( A. y ( y e. RR -> ( y < x -> E. z e. NN y < z ) ) -> ( ( x - 1 ) e. RR -> ( x e. RR -> E. z e. NN ( x - 1 ) < z ) ) )
13 2 12 syl5
 |-  ( A. y ( y e. RR -> ( y < x -> E. z e. NN y < z ) ) -> ( x e. RR -> ( x e. RR -> E. z e. NN ( x - 1 ) < z ) ) )
14 13 pm2.43d
 |-  ( A. y ( y e. RR -> ( y < x -> E. z e. NN y < z ) ) -> ( x e. RR -> E. z e. NN ( x - 1 ) < z ) )
15 df-rex
 |-  ( E. z e. NN ( x - 1 ) < z <-> E. z ( z e. NN /\ ( x - 1 ) < z ) )
16 14 15 syl6ib
 |-  ( A. y ( y e. RR -> ( y < x -> E. z e. NN y < z ) ) -> ( x e. RR -> E. z ( z e. NN /\ ( x - 1 ) < z ) ) )
17 16 com12
 |-  ( x e. RR -> ( A. y ( y e. RR -> ( y < x -> E. z e. NN y < z ) ) -> E. z ( z e. NN /\ ( x - 1 ) < z ) ) )
18 nnre
 |-  ( z e. NN -> z e. RR )
19 1re
 |-  1 e. RR
20 ltsubadd
 |-  ( ( x e. RR /\ 1 e. RR /\ z e. RR ) -> ( ( x - 1 ) < z <-> x < ( z + 1 ) ) )
21 19 20 mp3an2
 |-  ( ( x e. RR /\ z e. RR ) -> ( ( x - 1 ) < z <-> x < ( z + 1 ) ) )
22 18 21 sylan2
 |-  ( ( x e. RR /\ z e. NN ) -> ( ( x - 1 ) < z <-> x < ( z + 1 ) ) )
23 22 pm5.32da
 |-  ( x e. RR -> ( ( z e. NN /\ ( x - 1 ) < z ) <-> ( z e. NN /\ x < ( z + 1 ) ) ) )
24 23 exbidv
 |-  ( x e. RR -> ( E. z ( z e. NN /\ ( x - 1 ) < z ) <-> E. z ( z e. NN /\ x < ( z + 1 ) ) ) )
25 peano2nn
 |-  ( z e. NN -> ( z + 1 ) e. NN )
26 ovex
 |-  ( z + 1 ) e. _V
27 eleq1
 |-  ( y = ( z + 1 ) -> ( y e. NN <-> ( z + 1 ) e. NN ) )
28 breq2
 |-  ( y = ( z + 1 ) -> ( x < y <-> x < ( z + 1 ) ) )
29 27 28 anbi12d
 |-  ( y = ( z + 1 ) -> ( ( y e. NN /\ x < y ) <-> ( ( z + 1 ) e. NN /\ x < ( z + 1 ) ) ) )
30 26 29 spcev
 |-  ( ( ( z + 1 ) e. NN /\ x < ( z + 1 ) ) -> E. y ( y e. NN /\ x < y ) )
31 25 30 sylan
 |-  ( ( z e. NN /\ x < ( z + 1 ) ) -> E. y ( y e. NN /\ x < y ) )
32 31 exlimiv
 |-  ( E. z ( z e. NN /\ x < ( z + 1 ) ) -> E. y ( y e. NN /\ x < y ) )
33 24 32 syl6bi
 |-  ( x e. RR -> ( E. z ( z e. NN /\ ( x - 1 ) < z ) -> E. y ( y e. NN /\ x < y ) ) )
34 17 33 syld
 |-  ( x e. RR -> ( A. y ( y e. RR -> ( y < x -> E. z e. NN y < z ) ) -> E. y ( y e. NN /\ x < y ) ) )
35 df-ral
 |-  ( A. y e. RR ( y < x -> E. z e. NN y < z ) <-> A. y ( y e. RR -> ( y < x -> E. z e. NN y < z ) ) )
36 df-ral
 |-  ( A. y e. NN -. x < y <-> A. y ( y e. NN -> -. x < y ) )
37 alinexa
 |-  ( A. y ( y e. NN -> -. x < y ) <-> -. E. y ( y e. NN /\ x < y ) )
38 36 37 bitr2i
 |-  ( -. E. y ( y e. NN /\ x < y ) <-> A. y e. NN -. x < y )
39 38 con1bii
 |-  ( -. A. y e. NN -. x < y <-> E. y ( y e. NN /\ x < y ) )
40 34 35 39 3imtr4g
 |-  ( x e. RR -> ( A. y e. RR ( y < x -> E. z e. NN y < z ) -> -. A. y e. NN -. x < y ) )
41 40 anim2d
 |-  ( x e. RR -> ( ( A. y e. NN -. x < y /\ A. y e. RR ( y < x -> E. z e. NN y < z ) ) -> ( A. y e. NN -. x < y /\ -. A. y e. NN -. x < y ) ) )
42 1 41 mtoi
 |-  ( x e. RR -> -. ( A. y e. NN -. x < y /\ A. y e. RR ( y < x -> E. z e. NN y < z ) ) )
43 42 nrex
 |-  -. E. x e. RR ( A. y e. NN -. x < y /\ A. y e. RR ( y < x -> E. z e. NN y < z ) )
44 nnssre
 |-  NN C_ RR
45 1nn
 |-  1 e. NN
46 45 ne0ii
 |-  NN =/= (/)
47 sup2
 |-  ( ( NN C_ RR /\ NN =/= (/) /\ E. x e. RR A. y e. NN ( y < x \/ y = x ) ) -> E. x e. RR ( A. y e. NN -. x < y /\ A. y e. RR ( y < x -> E. z e. NN y < z ) ) )
48 44 46 47 mp3an12
 |-  ( E. x e. RR A. y e. NN ( y < x \/ y = x ) -> E. x e. RR ( A. y e. NN -. x < y /\ A. y e. RR ( y < x -> E. z e. NN y < z ) ) )
49 43 48 mto
 |-  -. E. x e. RR A. y e. NN ( y < x \/ y = x )