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 ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ → 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 ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ → W cyclShift L = W → L mod W = 0 ∨ W = W ⁡ 0 repeatS W
3 3simpa ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ → W ∈ Word V ∧ W ∈ ℙ
4 3 ad2antlr ⊢ L mod W ≠ 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ ∧ W cyclShift L = W → W ∈ Word V ∧ W ∈ ℙ
5 simplr3 ⊢ L mod W ≠ 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ ∧ W cyclShift L = W → L ∈ ℤ
6 simpll ⊢ L mod W ≠ 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ ∧ W cyclShift L = W → L mod W ≠ 0
7 simpr ⊢ L mod W ≠ 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ ∧ W cyclShift L = W → W cyclShift L = W
8 cshwsidrepsw ⊢ W ∈ Word V ∧ W ∈ ℙ → L ∈ ℤ ∧ L mod W ≠ 0 ∧ W cyclShift L = W → W = W ⁡ 0 repeatS W
9 8 imp ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ ∧ 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 ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ ∧ W cyclShift L = W → W = W ⁡ 0 repeatS W
11 10 olcd ⊢ L mod W ≠ 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ ∧ W cyclShift L = W → L mod W = 0 ∨ W = W ⁡ 0 repeatS W
12 11 exp31 ⊢ L mod W ≠ 0 → W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ → W cyclShift L = W → L mod W = 0 ∨ W = W ⁡ 0 repeatS W
13 2 12 pm2.61ine ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ → W cyclShift L = W → L mod W = 0 ∨ W = W ⁡ 0 repeatS W