Step |
Hyp |
Ref |
Expression |
1 |
|
nnnn0 |
|- ( N e. NN -> N e. NN0 ) |
2 |
|
repsw |
|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) e. Word V ) |
3 |
1 2
|
sylan2 |
|- ( ( S e. V /\ N e. NN ) -> ( S repeatS N ) e. Word V ) |
4 |
|
lsw |
|- ( ( S repeatS N ) e. Word V -> ( lastS ` ( S repeatS N ) ) = ( ( S repeatS N ) ` ( ( # ` ( S repeatS N ) ) - 1 ) ) ) |
5 |
3 4
|
syl |
|- ( ( S e. V /\ N e. NN ) -> ( lastS ` ( S repeatS N ) ) = ( ( S repeatS N ) ` ( ( # ` ( S repeatS N ) ) - 1 ) ) ) |
6 |
|
simpl |
|- ( ( S e. V /\ N e. NN ) -> S e. V ) |
7 |
1
|
adantl |
|- ( ( S e. V /\ N e. NN ) -> N e. NN0 ) |
8 |
|
repswlen |
|- ( ( S e. V /\ N e. NN0 ) -> ( # ` ( S repeatS N ) ) = N ) |
9 |
1 8
|
sylan2 |
|- ( ( S e. V /\ N e. NN ) -> ( # ` ( S repeatS N ) ) = N ) |
10 |
9
|
oveq1d |
|- ( ( S e. V /\ N e. NN ) -> ( ( # ` ( S repeatS N ) ) - 1 ) = ( N - 1 ) ) |
11 |
|
fzo0end |
|- ( N e. NN -> ( N - 1 ) e. ( 0 ..^ N ) ) |
12 |
11
|
adantl |
|- ( ( S e. V /\ N e. NN ) -> ( N - 1 ) e. ( 0 ..^ N ) ) |
13 |
10 12
|
eqeltrd |
|- ( ( S e. V /\ N e. NN ) -> ( ( # ` ( S repeatS N ) ) - 1 ) e. ( 0 ..^ N ) ) |
14 |
|
repswsymb |
|- ( ( S e. V /\ N e. NN0 /\ ( ( # ` ( S repeatS N ) ) - 1 ) e. ( 0 ..^ N ) ) -> ( ( S repeatS N ) ` ( ( # ` ( S repeatS N ) ) - 1 ) ) = S ) |
15 |
6 7 13 14
|
syl3anc |
|- ( ( S e. V /\ N e. NN ) -> ( ( S repeatS N ) ` ( ( # ` ( S repeatS N ) ) - 1 ) ) = S ) |
16 |
5 15
|
eqtrd |
|- ( ( S e. V /\ N e. NN ) -> ( lastS ` ( S repeatS N ) ) = S ) |