# Metamath Proof Explorer

## Theorem cshwsidrepswmod0

Description: If cyclically shifting a word of length being a prime number results in the word itself, the shift must be either by 0 (modulo the length of the word) or the word must be a "repeated symbol word". (Contributed by AV, 18-May-2018) (Revised by AV, 10-Nov-2018)

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

### Proof

Step Hyp Ref Expression
1 orc
` |-  ( ( L mod ( # ` W ) ) = 0 -> ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )`
2 1 2a1d
` |-  ( ( L mod ( # ` W ) ) = 0 -> ( ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) -> ( ( W cyclShift L ) = W -> ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) ) )`
3 3simpa
` |-  ( ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) -> ( W e. Word V /\ ( # ` W ) e. Prime ) )`
` |-  ( ( ( ( L mod ( # ` W ) ) =/= 0 /\ ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) ) /\ ( W cyclShift L ) = W ) -> ( W e. Word V /\ ( # ` W ) e. Prime ) )`
5 simplr3
` |-  ( ( ( ( L mod ( # ` W ) ) =/= 0 /\ ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) ) /\ ( W cyclShift L ) = W ) -> L e. ZZ )`
6 simpll
` |-  ( ( ( ( L mod ( # ` W ) ) =/= 0 /\ ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) ) /\ ( W cyclShift L ) = W ) -> ( L mod ( # ` W ) ) =/= 0 )`
7 simpr
` |-  ( ( ( ( L mod ( # ` W ) ) =/= 0 /\ ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) ) /\ ( W cyclShift L ) = W ) -> ( W cyclShift L ) = W )`
8 cshwsidrepsw
` |-  ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )`
9 8 imp
` |-  ( ( ( W e. Word V /\ ( # ` W ) e. Prime ) /\ ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) )`
10 4 5 6 7 9 syl13anc
` |-  ( ( ( ( L mod ( # ` W ) ) =/= 0 /\ ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) ) /\ ( W cyclShift L ) = W ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) )`
11 10 olcd
` |-  ( ( ( ( L mod ( # ` W ) ) =/= 0 /\ ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) ) /\ ( W cyclShift L ) = W ) -> ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )`
12 11 exp31
` |-  ( ( L mod ( # ` W ) ) =/= 0 -> ( ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) -> ( ( W cyclShift L ) = W -> ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) ) )`
13 2 12 pm2.61ine
` |-  ( ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) -> ( ( W cyclShift L ) = W -> ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) )`