| Step |
Hyp |
Ref |
Expression |
| 1 |
|
clwlkclwwlklem2.f |
|- F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) ) |
| 2 |
|
lencl |
|- ( P e. Word V -> ( # ` P ) e. NN0 ) |
| 3 |
|
nn0z |
|- ( ( # ` P ) e. NN0 -> ( # ` P ) e. ZZ ) |
| 4 |
3
|
adantr |
|- ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( # ` P ) e. ZZ ) |
| 5 |
|
0red |
|- ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> 0 e. RR ) |
| 6 |
|
2re |
|- 2 e. RR |
| 7 |
6
|
a1i |
|- ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> 2 e. RR ) |
| 8 |
|
nn0re |
|- ( ( # ` P ) e. NN0 -> ( # ` P ) e. RR ) |
| 9 |
8
|
adantr |
|- ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( # ` P ) e. RR ) |
| 10 |
|
2pos |
|- 0 < 2 |
| 11 |
10
|
a1i |
|- ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> 0 < 2 ) |
| 12 |
|
simpr |
|- ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> 2 <_ ( # ` P ) ) |
| 13 |
5 7 9 11 12
|
ltletrd |
|- ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> 0 < ( # ` P ) ) |
| 14 |
|
elnnz |
|- ( ( # ` P ) e. NN <-> ( ( # ` P ) e. ZZ /\ 0 < ( # ` P ) ) ) |
| 15 |
4 13 14
|
sylanbrc |
|- ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( # ` P ) e. NN ) |
| 16 |
2 15
|
sylan |
|- ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( # ` P ) e. NN ) |
| 17 |
|
nnm1nn0 |
|- ( ( # ` P ) e. NN -> ( ( # ` P ) - 1 ) e. NN0 ) |
| 18 |
16 17
|
syl |
|- ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 1 ) e. NN0 ) |
| 19 |
|
fvex |
|- ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) e. _V |
| 20 |
|
fvex |
|- ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) e. _V |
| 21 |
19 20
|
ifex |
|- if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) e. _V |
| 22 |
21 1
|
fnmpti |
|- F Fn ( 0 ..^ ( ( # ` P ) - 1 ) ) |
| 23 |
|
ffzo0hash |
|- ( ( ( ( # ` P ) - 1 ) e. NN0 /\ F Fn ( 0 ..^ ( ( # ` P ) - 1 ) ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) ) |
| 24 |
18 22 23
|
sylancl |
|- ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) ) |