| Step |
Hyp |
Ref |
Expression |
| 1 |
|
2z |
|- 2 e. ZZ |
| 2 |
1
|
a1i |
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 2 e. ZZ ) |
| 3 |
|
lencl |
|- ( W e. Word V -> ( # ` W ) e. NN0 ) |
| 4 |
3
|
nn0zd |
|- ( W e. Word V -> ( # ` W ) e. ZZ ) |
| 5 |
4
|
adantr |
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( # ` W ) e. ZZ ) |
| 6 |
|
simpr |
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 2 <_ ( # ` W ) ) |
| 7 |
|
eluz2 |
|- ( ( # ` W ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( # ` W ) e. ZZ /\ 2 <_ ( # ` W ) ) ) |
| 8 |
2 5 6 7
|
syl3anbrc |
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` 2 ) ) |
| 9 |
|
ige2m1fz1 |
|- ( ( # ` W ) e. ( ZZ>= ` 2 ) -> ( ( # ` W ) - 1 ) e. ( 1 ... ( # ` W ) ) ) |
| 10 |
8 9
|
syl |
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( 1 ... ( # ` W ) ) ) |
| 11 |
|
pfxfvlsw |
|- ( ( W e. Word V /\ ( ( # ` W ) - 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( W ` ( ( ( # ` W ) - 1 ) - 1 ) ) ) |
| 12 |
10 11
|
syldan |
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( W ` ( ( ( # ` W ) - 1 ) - 1 ) ) ) |
| 13 |
3
|
nn0cnd |
|- ( W e. Word V -> ( # ` W ) e. CC ) |
| 14 |
|
sub1m1 |
|- ( ( # ` W ) e. CC -> ( ( ( # ` W ) - 1 ) - 1 ) = ( ( # ` W ) - 2 ) ) |
| 15 |
13 14
|
syl |
|- ( W e. Word V -> ( ( ( # ` W ) - 1 ) - 1 ) = ( ( # ` W ) - 2 ) ) |
| 16 |
15
|
adantr |
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( ( # ` W ) - 1 ) - 1 ) = ( ( # ` W ) - 2 ) ) |
| 17 |
16
|
fveq2d |
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( W ` ( ( ( # ` W ) - 1 ) - 1 ) ) = ( W ` ( ( # ` W ) - 2 ) ) ) |
| 18 |
12 17
|
eqtrd |
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( W ` ( ( # ` W ) - 2 ) ) ) |