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∈WordV∧W∈ℙ
Assertion cshwshashlem1 ⊢φ∧∃i∈0..^WW⁡i≠W⁡0∧L∈1..^W→WcyclShiftL≠W

Proof

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