Step |
Hyp |
Ref |
Expression |
1 |
|
uzubico2.1 |
|- ( ph -> M e. ZZ ) |
2 |
|
uzubico2.2 |
|- Z = ( ZZ>= ` M ) |
3 |
1 2
|
uzubioo2 |
|- ( ph -> A. x e. RR E. k e. ( x (,) +oo ) k e. Z ) |
4 |
|
ioossico |
|- ( x (,) +oo ) C_ ( x [,) +oo ) |
5 |
|
ssrexv |
|- ( ( x (,) +oo ) C_ ( x [,) +oo ) -> ( E. k e. ( x (,) +oo ) k e. Z -> E. k e. ( x [,) +oo ) k e. Z ) ) |
6 |
4 5
|
ax-mp |
|- ( E. k e. ( x (,) +oo ) k e. Z -> E. k e. ( x [,) +oo ) k e. Z ) |
7 |
6
|
ralimi |
|- ( A. x e. RR E. k e. ( x (,) +oo ) k e. Z -> A. x e. RR E. k e. ( x [,) +oo ) k e. Z ) |
8 |
3 7
|
syl |
|- ( ph -> A. x e. RR E. k e. ( x [,) +oo ) k e. Z ) |