Description: The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N (modulo the length of the word) of the original word. (Contributed by AV, 30-Oct-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | cshwidx0mod | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 | |
|
2 | simp3 | |
|
3 | lennncl | |
|
4 | lbfzo0 | |
|
5 | 3 4 | sylibr | |
6 | 5 | 3adant3 | |
7 | cshwidxmod | |
|
8 | 1 2 6 7 | syl3anc | |
9 | zcn | |
|
10 | 9 | addlidd | |
11 | 10 | 3ad2ant3 | |
12 | 11 | fvoveq1d | |
13 | 8 12 | eqtrd | |