# Metamath Proof Explorer

## Theorem cshwsidrepsw

Description: If cyclically shifting a word of length being a prime number by a number of positions which is not divisible by the prime number results in the word itself, the word is a "repeated symbol word". (Contributed by AV, 18-May-2018) (Revised by AV, 10-Nov-2018)

Ref Expression
Assertion cshwsidrepsw
`|- ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )`

### Proof

Step Hyp Ref Expression
1 simpr
` |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( # ` W ) e. Prime )`
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> ( # ` W ) e. Prime )`
3 simp1
` |-  ( ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) -> L e. ZZ )`
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> L e. ZZ )`
5 simpr2
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> ( L mod ( # ` W ) ) =/= 0 )`
6 2 4 5 3jca
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> ( ( # ` W ) e. Prime /\ L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 ) )`
` |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( # ` W ) e. Prime /\ L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 ) )`
8 simpr
` |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> i e. ( 0 ..^ ( # ` W ) ) )`
9 modprmn0modprm0
` |-  ( ( ( # ` W ) e. Prime /\ L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 ) -> ( i e. ( 0 ..^ ( # ` W ) ) -> E. j e. ( 0 ..^ ( # ` W ) ) ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) )`
10 7 8 9 sylc
` |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> E. j e. ( 0 ..^ ( # ` W ) ) ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 )`
11 oveq1
` |-  ( k = j -> ( k x. L ) = ( j x. L ) )`
12 11 oveq2d
` |-  ( k = j -> ( i + ( k x. L ) ) = ( i + ( j x. L ) ) )`
13 12 fvoveq1d
` |-  ( k = j -> ( W ` ( ( i + ( k x. L ) ) mod ( # ` W ) ) ) = ( W ` ( ( i + ( j x. L ) ) mod ( # ` W ) ) ) )`
14 13 eqeq2d
` |-  ( k = j -> ( ( W ` i ) = ( W ` ( ( i + ( k x. L ) ) mod ( # ` W ) ) ) <-> ( W ` i ) = ( W ` ( ( i + ( j x. L ) ) mod ( # ` W ) ) ) ) )`
15 simpl
` |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> W e. Word V )`
16 15 3 anim12i
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> ( W e. Word V /\ L e. ZZ ) )`
` |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W e. Word V /\ L e. ZZ ) )`
` |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W e. Word V /\ L e. ZZ ) )`
19 simpr3
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> ( W cyclShift L ) = W )`
20 19 anim1i
` |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift L ) = W /\ i e. ( 0 ..^ ( # ` W ) ) ) )`
` |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> ( ( W cyclShift L ) = W /\ i e. ( 0 ..^ ( # ` W ) ) ) )`
22 cshweqrep
` |-  ( ( W e. Word V /\ L e. ZZ ) -> ( ( ( W cyclShift L ) = W /\ i e. ( 0 ..^ ( # ` W ) ) ) -> A. k e. NN0 ( W ` i ) = ( W ` ( ( i + ( k x. L ) ) mod ( # ` W ) ) ) ) )`
23 18 21 22 sylc
` |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> A. k e. NN0 ( W ` i ) = ( W ` ( ( i + ( k x. L ) ) mod ( # ` W ) ) ) )`
24 elfzonn0
` |-  ( j e. ( 0 ..^ ( # ` W ) ) -> j e. NN0 )`
` |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> j e. NN0 )`
26 14 23 25 rspcdva
` |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` i ) = ( W ` ( ( i + ( j x. L ) ) mod ( # ` W ) ) ) )`
27 fveq2
` |-  ( ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 -> ( W ` ( ( i + ( j x. L ) ) mod ( # ` W ) ) ) = ( W ` 0 ) )`
` |-  ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) -> ( W ` ( ( i + ( j x. L ) ) mod ( # ` W ) ) ) = ( W ` 0 ) )`
` |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` ( ( i + ( j x. L ) ) mod ( # ` W ) ) ) = ( W ` 0 ) )`
30 26 29 eqtrd
` |-  ( ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) /\ ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) ) -> ( W ` i ) = ( W ` 0 ) )`
31 30 ex
` |-  ( ( j e. ( 0 ..^ ( # ` W ) ) /\ ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 ) -> ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` i ) = ( W ` 0 ) ) )`
32 31 rexlimiva
` |-  ( E. j e. ( 0 ..^ ( # ` W ) ) ( ( i + ( j x. L ) ) mod ( # ` W ) ) = 0 -> ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` i ) = ( W ` 0 ) ) )`
33 10 32 mpcom
` |-  ( ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` i ) = ( W ` 0 ) )`
34 33 ralrimiva
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) )`
35 repswsymballbi
` |-  ( W e. Word V -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> ( W = ( ( W ` 0 ) repeatS ( # ` W ) ) <-> A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( W ` 0 ) ) )`
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) )`
` |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )`