| Step |
Hyp |
Ref |
Expression |
| 1 |
|
crctcshwlkn0lem.s |
|- ( ph -> S e. ( 1 ..^ N ) ) |
| 2 |
|
crctcshwlkn0lem.q |
|- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) ) |
| 3 |
|
crctcshwlkn0lem.h |
|- H = ( F cyclShift S ) |
| 4 |
|
crctcshwlkn0lem.n |
|- N = ( # ` F ) |
| 5 |
|
crctcshwlkn0lem.f |
|- ( ph -> F e. Word A ) |
| 6 |
|
crctcshwlkn0lem.p |
|- ( ph -> A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) |
| 7 |
|
crctcshwlkn0lem.e |
|- ( ph -> ( P ` N ) = ( P ` 0 ) ) |
| 8 |
1 2 3 4 5 6
|
crctcshwlkn0lem4 |
|- ( ph -> A. j e. ( 0 ..^ ( N - S ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) |
| 9 |
|
eqidd |
|- ( ph -> ( N - S ) = ( N - S ) ) |
| 10 |
1 2 3 4 5 6 7
|
crctcshwlkn0lem6 |
|- ( ( ph /\ ( N - S ) = ( N - S ) ) -> if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) ) |
| 11 |
9 10
|
mpdan |
|- ( ph -> if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) ) |
| 12 |
|
ovex |
|- ( N - S ) e. _V |
| 13 |
|
wkslem1 |
|- ( j = ( N - S ) -> ( if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) ) ) |
| 14 |
12 13
|
ralsn |
|- ( A. j e. { ( N - S ) } if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> if- ( ( Q ` ( N - S ) ) = ( Q ` ( ( N - S ) + 1 ) ) , ( I ` ( H ` ( N - S ) ) ) = { ( Q ` ( N - S ) ) } , { ( Q ` ( N - S ) ) , ( Q ` ( ( N - S ) + 1 ) ) } C_ ( I ` ( H ` ( N - S ) ) ) ) ) |
| 15 |
11 14
|
sylibr |
|- ( ph -> A. j e. { ( N - S ) } if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) |
| 16 |
|
ralunb |
|- ( A. j e. ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> ( A. j e. ( 0 ..^ ( N - S ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) /\ A. j e. { ( N - S ) } if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) ) |
| 17 |
8 15 16
|
sylanbrc |
|- ( ph -> A. j e. ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) |
| 18 |
|
elfzo1 |
|- ( S e. ( 1 ..^ N ) <-> ( S e. NN /\ N e. NN /\ S < N ) ) |
| 19 |
|
nnz |
|- ( N e. NN -> N e. ZZ ) |
| 20 |
|
nnz |
|- ( S e. NN -> S e. ZZ ) |
| 21 |
|
zsubcl |
|- ( ( N e. ZZ /\ S e. ZZ ) -> ( N - S ) e. ZZ ) |
| 22 |
19 20 21
|
syl2anr |
|- ( ( S e. NN /\ N e. NN ) -> ( N - S ) e. ZZ ) |
| 23 |
22
|
3adant3 |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> ( N - S ) e. ZZ ) |
| 24 |
|
nnre |
|- ( S e. NN -> S e. RR ) |
| 25 |
|
nnre |
|- ( N e. NN -> N e. RR ) |
| 26 |
|
posdif |
|- ( ( S e. RR /\ N e. RR ) -> ( S < N <-> 0 < ( N - S ) ) ) |
| 27 |
|
0re |
|- 0 e. RR |
| 28 |
|
resubcl |
|- ( ( N e. RR /\ S e. RR ) -> ( N - S ) e. RR ) |
| 29 |
28
|
ancoms |
|- ( ( S e. RR /\ N e. RR ) -> ( N - S ) e. RR ) |
| 30 |
|
ltle |
|- ( ( 0 e. RR /\ ( N - S ) e. RR ) -> ( 0 < ( N - S ) -> 0 <_ ( N - S ) ) ) |
| 31 |
27 29 30
|
sylancr |
|- ( ( S e. RR /\ N e. RR ) -> ( 0 < ( N - S ) -> 0 <_ ( N - S ) ) ) |
| 32 |
26 31
|
sylbid |
|- ( ( S e. RR /\ N e. RR ) -> ( S < N -> 0 <_ ( N - S ) ) ) |
| 33 |
24 25 32
|
syl2an |
|- ( ( S e. NN /\ N e. NN ) -> ( S < N -> 0 <_ ( N - S ) ) ) |
| 34 |
33
|
3impia |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> 0 <_ ( N - S ) ) |
| 35 |
|
elnn0z |
|- ( ( N - S ) e. NN0 <-> ( ( N - S ) e. ZZ /\ 0 <_ ( N - S ) ) ) |
| 36 |
23 34 35
|
sylanbrc |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> ( N - S ) e. NN0 ) |
| 37 |
|
elnn0uz |
|- ( ( N - S ) e. NN0 <-> ( N - S ) e. ( ZZ>= ` 0 ) ) |
| 38 |
36 37
|
sylib |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> ( N - S ) e. ( ZZ>= ` 0 ) ) |
| 39 |
|
fzosplitsn |
|- ( ( N - S ) e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( ( N - S ) + 1 ) ) = ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) ) |
| 40 |
38 39
|
syl |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> ( 0 ..^ ( ( N - S ) + 1 ) ) = ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) ) |
| 41 |
18 40
|
sylbi |
|- ( S e. ( 1 ..^ N ) -> ( 0 ..^ ( ( N - S ) + 1 ) ) = ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) ) |
| 42 |
1 41
|
syl |
|- ( ph -> ( 0 ..^ ( ( N - S ) + 1 ) ) = ( ( 0 ..^ ( N - S ) ) u. { ( N - S ) } ) ) |
| 43 |
17 42
|
raleqtrrdv |
|- ( ph -> A. j e. ( 0 ..^ ( ( N - S ) + 1 ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) |
| 44 |
1 2 3 4 5 6
|
crctcshwlkn0lem5 |
|- ( ph -> A. j e. ( ( ( N - S ) + 1 ) ..^ N ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) |
| 45 |
|
ralunb |
|- ( A. j e. ( ( 0 ..^ ( ( N - S ) + 1 ) ) u. ( ( ( N - S ) + 1 ) ..^ N ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> ( A. j e. ( 0 ..^ ( ( N - S ) + 1 ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) /\ A. j e. ( ( ( N - S ) + 1 ) ..^ N ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) ) |
| 46 |
43 44 45
|
sylanbrc |
|- ( ph -> A. j e. ( ( 0 ..^ ( ( N - S ) + 1 ) ) u. ( ( ( N - S ) + 1 ) ..^ N ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) |
| 47 |
|
nnsub |
|- ( ( S e. NN /\ N e. NN ) -> ( S < N <-> ( N - S ) e. NN ) ) |
| 48 |
47
|
biimp3a |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> ( N - S ) e. NN ) |
| 49 |
|
nnnn0 |
|- ( ( N - S ) e. NN -> ( N - S ) e. NN0 ) |
| 50 |
|
peano2nn0 |
|- ( ( N - S ) e. NN0 -> ( ( N - S ) + 1 ) e. NN0 ) |
| 51 |
48 49 50
|
3syl |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> ( ( N - S ) + 1 ) e. NN0 ) |
| 52 |
|
nnnn0 |
|- ( N e. NN -> N e. NN0 ) |
| 53 |
52
|
3ad2ant2 |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> N e. NN0 ) |
| 54 |
25
|
anim1i |
|- ( ( N e. NN /\ S e. NN ) -> ( N e. RR /\ S e. NN ) ) |
| 55 |
54
|
ancoms |
|- ( ( S e. NN /\ N e. NN ) -> ( N e. RR /\ S e. NN ) ) |
| 56 |
|
crctcshwlkn0lem1 |
|- ( ( N e. RR /\ S e. NN ) -> ( ( N - S ) + 1 ) <_ N ) |
| 57 |
55 56
|
syl |
|- ( ( S e. NN /\ N e. NN ) -> ( ( N - S ) + 1 ) <_ N ) |
| 58 |
57
|
3adant3 |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> ( ( N - S ) + 1 ) <_ N ) |
| 59 |
|
elfz2nn0 |
|- ( ( ( N - S ) + 1 ) e. ( 0 ... N ) <-> ( ( ( N - S ) + 1 ) e. NN0 /\ N e. NN0 /\ ( ( N - S ) + 1 ) <_ N ) ) |
| 60 |
51 53 58 59
|
syl3anbrc |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> ( ( N - S ) + 1 ) e. ( 0 ... N ) ) |
| 61 |
18 60
|
sylbi |
|- ( S e. ( 1 ..^ N ) -> ( ( N - S ) + 1 ) e. ( 0 ... N ) ) |
| 62 |
|
fzosplit |
|- ( ( ( N - S ) + 1 ) e. ( 0 ... N ) -> ( 0 ..^ N ) = ( ( 0 ..^ ( ( N - S ) + 1 ) ) u. ( ( ( N - S ) + 1 ) ..^ N ) ) ) |
| 63 |
1 61 62
|
3syl |
|- ( ph -> ( 0 ..^ N ) = ( ( 0 ..^ ( ( N - S ) + 1 ) ) u. ( ( ( N - S ) + 1 ) ..^ N ) ) ) |
| 64 |
46 63
|
raleqtrrdv |
|- ( ph -> A. j e. ( 0 ..^ N ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) |