Metamath Proof Explorer

Theorem cshwshashlem1

Description: If cyclically shifting a word of length being a prime number not consisting of identical symbols by at least one position (and not by as many positions as the length of the word), the result will not be the word itself. (Contributed by AV, 19-May-2018) (Revised by AV, 8-Jun-2018) (Revised by AV, 10-Nov-2018)

Ref Expression
Hypothesis cshwshash.0 ⊢ φ → W ∈ Word V ∧ W ∈ ℙ
Assertion cshwshashlem1 ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 1 ..^ W → W cyclShift L ≠ W

Proof

Step Hyp Ref Expression
1 cshwshash.0 ⊢ φ → W ∈ Word V ∧ W ∈ ℙ
2 df-ne ⊢ W ⁡ i ≠ W ⁡ 0 ↔ ¬ W ⁡ i = W ⁡ 0
3 2 rexbii ⊢ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ↔ ∃ i ∈ 0 ..^ W ¬ W ⁡ i = W ⁡ 0
4 rexnal ⊢ ∃ i ∈ 0 ..^ W ¬ W ⁡ i = W ⁡ 0 ↔ ¬ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
5 3 4 bitri ⊢ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ↔ ¬ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
6 simpll ⊢ φ ∧ L ∈ 1 ..^ W ∧ W cyclShift L = W → φ
7 fzo0ss1 ⊢ 1 ..^ W ⊆ 0 ..^ W
8 fzossfz ⊢ 0 ..^ W ⊆ 0 … W
9 7 8 sstri ⊢ 1 ..^ W ⊆ 0 … W
10 9 sseli ⊢ L ∈ 1 ..^ W → L ∈ 0 … W
11 10 ad2antlr ⊢ φ ∧ L ∈ 1 ..^ W ∧ W cyclShift L = W → L ∈ 0 … W
12 simpr ⊢ φ ∧ L ∈ 1 ..^ W ∧ W cyclShift L = W → W cyclShift L = W
13 simpll ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W → W ∈ Word V
14 simpr ⊢ W ∈ Word V ∧ W ∈ ℙ → W ∈ ℙ
15 14 adantr ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W → W ∈ ℙ
16 elfzelz ⊢ L ∈ 0 … W → L ∈ ℤ
17 16 adantl ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W → L ∈ ℤ
18 cshwsidrepswmod0 ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ ℤ → W cyclShift L = W → L mod W = 0 ∨ W = W ⁡ 0 repeatS W
19 13 15 17 18 syl3anc ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W → W cyclShift L = W → L mod W = 0 ∨ W = W ⁡ 0 repeatS W
20 19 ex ⊢ W ∈ Word V ∧ W ∈ ℙ → L ∈ 0 … W → W cyclShift L = W → L mod W = 0 ∨ W = W ⁡ 0 repeatS W
21 20 3imp ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L mod W = 0 ∨ W = W ⁡ 0 repeatS W
22 olc ⊢ L = W → L = 0 ∨ L = W
23 22 a1d ⊢ L = W → L mod W = 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W
24 fzofzim ⊢ L ≠ W ∧ L ∈ 0 … W → L ∈ 0 ..^ W
25 zmodidfzoimp ⊢ L ∈ 0 ..^ W → L mod W = L
26 eqtr2 ⊢ L mod W = L ∧ L mod W = 0 → L = 0
27 26 a1d ⊢ L mod W = L ∧ L mod W = 0 → W ∈ Word V ∧ W ∈ ℙ → L = 0
28 27 ex ⊢ L mod W = L → L mod W = 0 → W ∈ Word V ∧ W ∈ ℙ → L = 0
29 25 28 syl ⊢ L ∈ 0 ..^ W → L mod W = 0 → W ∈ Word V ∧ W ∈ ℙ → L = 0
30 24 29 syl ⊢ L ≠ W ∧ L ∈ 0 … W → L mod W = 0 → W ∈ Word V ∧ W ∈ ℙ → L = 0
31 30 expcom ⊢ L ∈ 0 … W → L ≠ W → L mod W = 0 → W ∈ Word V ∧ W ∈ ℙ → L = 0
32 31 com24 ⊢ L ∈ 0 … W → W ∈ Word V ∧ W ∈ ℙ → L mod W = 0 → L ≠ W → L = 0
33 32 impcom ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W → L mod W = 0 → L ≠ W → L = 0
34 33 3adant3 ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L mod W = 0 → L ≠ W → L = 0
35 34 impcom ⊢ L mod W = 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L ≠ W → L = 0
36 35 impcom ⊢ L ≠ W ∧ L mod W = 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0
37 36 orcd ⊢ L ≠ W ∧ L mod W = 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W
38 37 ex ⊢ L ≠ W → L mod W = 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W
39 23 38 pm2.61ine ⊢ L mod W = 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W
40 39 orcd ⊢ L mod W = 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ W = W ⁡ 0 repeatS W
41 df-3or ⊢ L = 0 ∨ L = W ∨ W = W ⁡ 0 repeatS W ↔ L = 0 ∨ L = W ∨ W = W ⁡ 0 repeatS W
42 40 41 sylibr ⊢ L mod W = 0 ∧ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ W = W ⁡ 0 repeatS W
43 42 ex ⊢ L mod W = 0 → W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ W = W ⁡ 0 repeatS W
44 3mix3 ⊢ W = W ⁡ 0 repeatS W → L = 0 ∨ L = W ∨ W = W ⁡ 0 repeatS W
45 44 a1d ⊢ W = W ⁡ 0 repeatS W → W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ W = W ⁡ 0 repeatS W
46 43 45 jaoi ⊢ L mod W = 0 ∨ W = W ⁡ 0 repeatS W → W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ W = W ⁡ 0 repeatS W
47 21 46 mpcom ⊢ W ∈ Word V ∧ W ∈ ℙ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ W = W ⁡ 0 repeatS W
48 1 47 syl3an1 ⊢ φ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ W = W ⁡ 0 repeatS W
49 3mix1 ⊢ L = 0 → L = 0 ∨ L = W ∨ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
50 49 a1d ⊢ L = 0 → φ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
51 3mix2 ⊢ L = W → L = 0 ∨ L = W ∨ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
52 51 a1d ⊢ L = W → φ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
53 repswsymballbi ⊢ W ∈ Word V → W = W ⁡ 0 repeatS W ↔ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
54 53 adantr ⊢ W ∈ Word V ∧ W ∈ ℙ → W = W ⁡ 0 repeatS W ↔ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
55 1 54 syl ⊢ φ → W = W ⁡ 0 repeatS W ↔ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
56 55 3ad2ant1 ⊢ φ ∧ L ∈ 0 … W ∧ W cyclShift L = W → W = W ⁡ 0 repeatS W ↔ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
57 56 biimpa ⊢ φ ∧ L ∈ 0 … W ∧ W cyclShift L = W ∧ W = W ⁡ 0 repeatS W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
58 57 3mix3d ⊢ φ ∧ L ∈ 0 … W ∧ W cyclShift L = W ∧ W = W ⁡ 0 repeatS W → L = 0 ∨ L = W ∨ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
59 58 expcom ⊢ W = W ⁡ 0 repeatS W → φ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
60 50 52 59 3jaoi ⊢ L = 0 ∨ L = W ∨ W = W ⁡ 0 repeatS W → φ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
61 48 60 mpcom ⊢ φ ∧ L ∈ 0 … W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
62 6 11 12 61 syl3anc ⊢ φ ∧ L ∈ 1 ..^ W ∧ W cyclShift L = W → L = 0 ∨ L = W ∨ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
63 elfzo1 ⊢ L ∈ 1 ..^ W ↔ L ∈ ℕ ∧ W ∈ ℕ ∧ L < W
64 nnne0 ⊢ L ∈ ℕ → L ≠ 0
65 df-ne ⊢ L ≠ 0 ↔ ¬ L = 0
66 pm2.21 ⊢ ¬ L = 0 → L = 0 → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
67 65 66 sylbi ⊢ L ≠ 0 → L = 0 → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
68 64 67 syl ⊢ L ∈ ℕ → L = 0 → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
69 68 3ad2ant1 ⊢ L ∈ ℕ ∧ W ∈ ℕ ∧ L < W → L = 0 → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
70 63 69 sylbi ⊢ L ∈ 1 ..^ W → L = 0 → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
71 70 ad2antlr ⊢ φ ∧ L ∈ 1 ..^ W ∧ W cyclShift L = W → L = 0 → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
72 71 com12 ⊢ L = 0 → φ ∧ L ∈ 1 ..^ W ∧ W cyclShift L = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
73 nnre ⊢ L ∈ ℕ → L ∈ ℝ
74 ltne ⊢ L ∈ ℝ ∧ L < W → W ≠ L
75 73 74 sylan ⊢ L ∈ ℕ ∧ L < W → W ≠ L
76 df-ne ⊢ W ≠ L ↔ ¬ W = L
77 eqcom ⊢ L = W ↔ W = L
78 pm2.21 ⊢ ¬ W = L → W = L → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
79 77 78 biimtrid ⊢ ¬ W = L → L = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
80 76 79 sylbi ⊢ W ≠ L → L = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
81 75 80 syl ⊢ L ∈ ℕ ∧ L < W → L = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
82 81 3adant2 ⊢ L ∈ ℕ ∧ W ∈ ℕ ∧ L < W → L = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
83 63 82 sylbi ⊢ L ∈ 1 ..^ W → L = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
84 83 ad2antlr ⊢ φ ∧ L ∈ 1 ..^ W ∧ W cyclShift L = W → L = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
85 84 com12 ⊢ L = W → φ ∧ L ∈ 1 ..^ W ∧ W cyclShift L = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
86 ax-1 ⊢ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0 → φ ∧ L ∈ 1 ..^ W ∧ W cyclShift L = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
87 72 85 86 3jaoi ⊢ L = 0 ∨ L = W ∨ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0 → φ ∧ L ∈ 1 ..^ W ∧ W cyclShift L = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
88 62 87 mpcom ⊢ φ ∧ L ∈ 1 ..^ W ∧ W cyclShift L = W → ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0
89 88 pm2.24d ⊢ φ ∧ L ∈ 1 ..^ W ∧ W cyclShift L = W → ¬ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0 → W cyclShift L ≠ W
90 89 exp31 ⊢ φ → L ∈ 1 ..^ W → W cyclShift L = W → ¬ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0 → W cyclShift L ≠ W
91 90 com34 ⊢ φ → L ∈ 1 ..^ W → ¬ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0 → W cyclShift L = W → W cyclShift L ≠ W
92 91 com23 ⊢ φ → ¬ ∀ i ∈ 0 ..^ W W ⁡ i = W ⁡ 0 → L ∈ 1 ..^ W → W cyclShift L = W → W cyclShift L ≠ W
93 5 92 biimtrid ⊢ φ → ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → L ∈ 1 ..^ W → W cyclShift L = W → W cyclShift L ≠ W
94 93 3imp ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 1 ..^ W → W cyclShift L = W → W cyclShift L ≠ W
95 94 com12 ⊢ W cyclShift L = W → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 1 ..^ W → W cyclShift L ≠ W
96 ax-1 ⊢ W cyclShift L ≠ W → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 1 ..^ W → W cyclShift L ≠ W
97 95 96 pm2.61ine ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 1 ..^ W → W cyclShift L ≠ W