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

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 imbitrdi 
 |-  ( 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 biimtrdi 
 |-  ( 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 )