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 ) )
4 3 ad2antlr 
 |-  ( ( ( ( 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 ) ) ) ) )