Step |
Hyp |
Ref |
Expression |
1 |
|
uzind4s.1 |
|- ( M e. ZZ -> [. M / k ]. ph ) |
2 |
|
uzind4s.2 |
|- ( k e. ( ZZ>= ` M ) -> ( ph -> [. ( k + 1 ) / k ]. ph ) ) |
3 |
|
dfsbcq2 |
|- ( j = M -> ( [ j / k ] ph <-> [. M / k ]. ph ) ) |
4 |
|
sbequ |
|- ( j = m -> ( [ j / k ] ph <-> [ m / k ] ph ) ) |
5 |
|
dfsbcq2 |
|- ( j = ( m + 1 ) -> ( [ j / k ] ph <-> [. ( m + 1 ) / k ]. ph ) ) |
6 |
|
dfsbcq2 |
|- ( j = N -> ( [ j / k ] ph <-> [. N / k ]. ph ) ) |
7 |
|
nfv |
|- F/ k m e. ( ZZ>= ` M ) |
8 |
|
nfs1v |
|- F/ k [ m / k ] ph |
9 |
|
nfsbc1v |
|- F/ k [. ( m + 1 ) / k ]. ph |
10 |
8 9
|
nfim |
|- F/ k ( [ m / k ] ph -> [. ( m + 1 ) / k ]. ph ) |
11 |
7 10
|
nfim |
|- F/ k ( m e. ( ZZ>= ` M ) -> ( [ m / k ] ph -> [. ( m + 1 ) / k ]. ph ) ) |
12 |
|
eleq1w |
|- ( k = m -> ( k e. ( ZZ>= ` M ) <-> m e. ( ZZ>= ` M ) ) ) |
13 |
|
sbequ12 |
|- ( k = m -> ( ph <-> [ m / k ] ph ) ) |
14 |
|
oveq1 |
|- ( k = m -> ( k + 1 ) = ( m + 1 ) ) |
15 |
14
|
sbceq1d |
|- ( k = m -> ( [. ( k + 1 ) / k ]. ph <-> [. ( m + 1 ) / k ]. ph ) ) |
16 |
13 15
|
imbi12d |
|- ( k = m -> ( ( ph -> [. ( k + 1 ) / k ]. ph ) <-> ( [ m / k ] ph -> [. ( m + 1 ) / k ]. ph ) ) ) |
17 |
12 16
|
imbi12d |
|- ( k = m -> ( ( k e. ( ZZ>= ` M ) -> ( ph -> [. ( k + 1 ) / k ]. ph ) ) <-> ( m e. ( ZZ>= ` M ) -> ( [ m / k ] ph -> [. ( m + 1 ) / k ]. ph ) ) ) ) |
18 |
11 17 2
|
chvarfv |
|- ( m e. ( ZZ>= ` M ) -> ( [ m / k ] ph -> [. ( m + 1 ) / k ]. ph ) ) |
19 |
3 4 5 6 1 18
|
uzind4 |
|- ( N e. ( ZZ>= ` M ) -> [. N / k ]. ph ) |