Metamath Proof Explorer

Theorem cshwshashlem2

Description: If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018) (Revised by Alexander van der Vekens, 8-Jun-2018)

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

Proof

Step Hyp Ref Expression
1 cshwshash.0 ⊢ φ → W ∈ Word V ∧ W ∈ ℙ
2 oveq1 ⊢ W cyclShift L = W cyclShift K → W cyclShift L cyclShift W − L = W cyclShift K cyclShift W − L
3 2 eqcomd ⊢ W cyclShift L = W cyclShift K → W cyclShift K cyclShift W − L = W cyclShift L cyclShift W − L
4 3 ad2antrr ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W cyclShift K cyclShift W − L = W cyclShift L cyclShift W − L
5 1 simpld ⊢ φ → W ∈ Word V
6 5 adantr ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → W ∈ Word V
7 6 adantl ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → W ∈ Word V
8 7 adantr ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W ∈ Word V
9 elfzofz ⊢ K ∈ 0 ..^ W → K ∈ 0 … W
10 9 3ad2ant2 ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → K ∈ 0 … W
11 10 adantl ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → K ∈ 0 … W
12 elfzofz ⊢ L ∈ 0 ..^ W → L ∈ 0 … W
13 fznn0sub2 ⊢ L ∈ 0 … W → W − L ∈ 0 … W
14 12 13 syl ⊢ L ∈ 0 ..^ W → W − L ∈ 0 … W
15 14 3ad2ant1 ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W − L ∈ 0 … W
16 15 adantl ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W − L ∈ 0 … W
17 elfzo0 ⊢ L ∈ 0 ..^ W ↔ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W
18 zre ⊢ K ∈ ℤ → K ∈ ℝ
19 18 adantr ⊢ K ∈ ℤ ∧ L ∈ ℕ 0 ∧ W ∈ ℕ → K ∈ ℝ
20 nnre ⊢ W ∈ ℕ → W ∈ ℝ
21 nn0re ⊢ L ∈ ℕ 0 → L ∈ ℝ
22 resubcl ⊢ W ∈ ℝ ∧ L ∈ ℝ → W − L ∈ ℝ
23 20 21 22 syl2anr ⊢ L ∈ ℕ 0 ∧ W ∈ ℕ → W − L ∈ ℝ
24 23 adantl ⊢ K ∈ ℤ ∧ L ∈ ℕ 0 ∧ W ∈ ℕ → W − L ∈ ℝ
25 19 24 readdcld ⊢ K ∈ ℤ ∧ L ∈ ℕ 0 ∧ W ∈ ℕ → K + W - L ∈ ℝ
26 20 adantl ⊢ L ∈ ℕ 0 ∧ W ∈ ℕ → W ∈ ℝ
27 26 adantl ⊢ K ∈ ℤ ∧ L ∈ ℕ 0 ∧ W ∈ ℕ → W ∈ ℝ
28 25 27 jca ⊢ K ∈ ℤ ∧ L ∈ ℕ 0 ∧ W ∈ ℕ → K + W - L ∈ ℝ ∧ W ∈ ℝ
29 28 ex ⊢ K ∈ ℤ → L ∈ ℕ 0 ∧ W ∈ ℕ → K + W - L ∈ ℝ ∧ W ∈ ℝ
30 elfzoelz ⊢ K ∈ 0 ..^ W → K ∈ ℤ
31 29 30 syl11 ⊢ L ∈ ℕ 0 ∧ W ∈ ℕ → K ∈ 0 ..^ W → K + W - L ∈ ℝ ∧ W ∈ ℝ
32 31 3adant3 ⊢ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → K ∈ 0 ..^ W → K + W - L ∈ ℝ ∧ W ∈ ℝ
33 17 32 sylbi ⊢ L ∈ 0 ..^ W → K ∈ 0 ..^ W → K + W - L ∈ ℝ ∧ W ∈ ℝ
34 33 imp ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W → K + W - L ∈ ℝ ∧ W ∈ ℝ
35 34 3adant3 ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → K + W - L ∈ ℝ ∧ W ∈ ℝ
36 fzonmapblen ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → K + W - L < W
37 ltle ⊢ K + W - L ∈ ℝ ∧ W ∈ ℝ → K + W - L < W → K + W - L ≤ W
38 35 36 37 sylc ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → K + W - L ≤ W
39 38 adantl ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → K + W - L ≤ W
40 simpl ⊢ W ∈ Word V ∧ K ∈ 0 … W ∧ W − L ∈ 0 … W ∧ K + W - L ≤ W → W ∈ Word V
41 elfzelz ⊢ K ∈ 0 … W → K ∈ ℤ
42 41 3ad2ant1 ⊢ K ∈ 0 … W ∧ W − L ∈ 0 … W ∧ K + W - L ≤ W → K ∈ ℤ
43 42 adantl ⊢ W ∈ Word V ∧ K ∈ 0 … W ∧ W − L ∈ 0 … W ∧ K + W - L ≤ W → K ∈ ℤ
44 elfzelz ⊢ W − L ∈ 0 … W → W − L ∈ ℤ
45 44 3ad2ant2 ⊢ K ∈ 0 … W ∧ W − L ∈ 0 … W ∧ K + W - L ≤ W → W − L ∈ ℤ
46 45 adantl ⊢ W ∈ Word V ∧ K ∈ 0 … W ∧ W − L ∈ 0 … W ∧ K + W - L ≤ W → W − L ∈ ℤ
47 2cshw ⊢ W ∈ Word V ∧ K ∈ ℤ ∧ W − L ∈ ℤ → W cyclShift K cyclShift W − L = W cyclShift K + W - L
48 40 43 46 47 syl3anc ⊢ W ∈ Word V ∧ K ∈ 0 … W ∧ W − L ∈ 0 … W ∧ K + W - L ≤ W → W cyclShift K cyclShift W − L = W cyclShift K + W - L
49 8 11 16 39 48 syl13anc ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W cyclShift K cyclShift W − L = W cyclShift K + W - L
50 12 3ad2ant1 ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → L ∈ 0 … W
51 elfzelz ⊢ L ∈ 0 … W → L ∈ ℤ
52 2cshwid ⊢ W ∈ Word V ∧ L ∈ ℤ → W cyclShift L cyclShift W − L = W
53 51 52 sylan2 ⊢ W ∈ Word V ∧ L ∈ 0 … W → W cyclShift L cyclShift W − L = W
54 7 50 53 syl2an ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W cyclShift L cyclShift W − L = W
55 4 49 54 3eqtr3d ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W cyclShift K + W - L = W
56 simplrl ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → φ
57 simplrr ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0
58 3simpa ⊢ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → L ∈ ℕ 0 ∧ W ∈ ℕ
59 17 58 sylbi ⊢ L ∈ 0 ..^ W → L ∈ ℕ 0 ∧ W ∈ ℕ
60 nnz ⊢ W ∈ ℕ → W ∈ ℤ
61 nn0z ⊢ L ∈ ℕ 0 → L ∈ ℤ
62 zsubcl ⊢ W ∈ ℤ ∧ L ∈ ℤ → W − L ∈ ℤ
63 60 61 62 syl2anr ⊢ L ∈ ℕ 0 ∧ W ∈ ℕ → W − L ∈ ℤ
64 63 anim1ci ⊢ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ K ∈ ℤ → K ∈ ℤ ∧ W − L ∈ ℤ
65 zaddcl ⊢ K ∈ ℤ ∧ W − L ∈ ℤ → K + W - L ∈ ℤ
66 64 65 syl ⊢ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ K ∈ ℤ → K + W - L ∈ ℤ
67 59 30 66 syl2an ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W → K + W - L ∈ ℤ
68 67 3adant3 ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → K + W - L ∈ ℤ
69 elfzo0 ⊢ K ∈ 0 ..^ W ↔ K ∈ ℕ 0 ∧ W ∈ ℕ ∧ K < W
70 elnn0z ⊢ K ∈ ℕ 0 ↔ K ∈ ℤ ∧ 0 ≤ K
71 18 ad2antrr ⊢ K ∈ ℤ ∧ 0 ≤ K ∧ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → K ∈ ℝ
72 23 3adant3 ⊢ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → W − L ∈ ℝ
73 72 adantl ⊢ K ∈ ℤ ∧ 0 ≤ K ∧ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → W − L ∈ ℝ
74 simplr ⊢ K ∈ ℤ ∧ 0 ≤ K ∧ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → 0 ≤ K
75 posdif ⊢ L ∈ ℝ ∧ W ∈ ℝ → L < W ↔ 0 < W − L
76 21 20 75 syl2an ⊢ L ∈ ℕ 0 ∧ W ∈ ℕ → L < W ↔ 0 < W − L
77 76 biimp3a ⊢ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → 0 < W − L
78 77 adantl ⊢ K ∈ ℤ ∧ 0 ≤ K ∧ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → 0 < W − L
79 71 73 74 78 addgegt0d ⊢ K ∈ ℤ ∧ 0 ≤ K ∧ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → 0 < K + W - L
80 79 ex ⊢ K ∈ ℤ ∧ 0 ≤ K → L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → 0 < K + W - L
81 70 80 sylbi ⊢ K ∈ ℕ 0 → L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → 0 < K + W - L
82 81 3ad2ant1 ⊢ K ∈ ℕ 0 ∧ W ∈ ℕ ∧ K < W → L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → 0 < K + W - L
83 69 82 sylbi ⊢ K ∈ 0 ..^ W → L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → 0 < K + W - L
84 83 com12 ⊢ L ∈ ℕ 0 ∧ W ∈ ℕ ∧ L < W → K ∈ 0 ..^ W → 0 < K + W - L
85 17 84 sylbi ⊢ L ∈ 0 ..^ W → K ∈ 0 ..^ W → 0 < K + W - L
86 85 imp ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W → 0 < K + W - L
87 86 3adant3 ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → 0 < K + W - L
88 elnnz ⊢ K + W - L ∈ ℕ ↔ K + W - L ∈ ℤ ∧ 0 < K + W - L
89 68 87 88 sylanbrc ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → K + W - L ∈ ℕ
90 17 simp2bi ⊢ L ∈ 0 ..^ W → W ∈ ℕ
91 90 3ad2ant1 ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W ∈ ℕ
92 elfzo1 ⊢ K + W - L ∈ 1 ..^ W ↔ K + W - L ∈ ℕ ∧ W ∈ ℕ ∧ K + W - L < W
93 89 91 36 92 syl3anbrc ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → K + W - L ∈ 1 ..^ W
94 93 adantl ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → K + W - L ∈ 1 ..^ W
95 1 cshwshashlem1 ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ K + W - L ∈ 1 ..^ W → W cyclShift K + W - L ≠ W
96 56 57 94 95 syl3anc ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W cyclShift K + W - L ≠ W
97 55 96 pm2.21ddne ⊢ W cyclShift L = W cyclShift K ∧ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W cyclShift L ≠ W cyclShift K
98 97 exp31 ⊢ W cyclShift L = W cyclShift K → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W cyclShift L ≠ W cyclShift K
99 2a1 ⊢ W cyclShift L ≠ W cyclShift K → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W cyclShift L ≠ W cyclShift K
100 98 99 pm2.61ine ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W cyclShift L ≠ W cyclShift K