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