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

Proof

Step Hyp Ref Expression
1 cshwshash.0 ⊢φ→W∈WordV∧W∈ℙ
2 oveq1 ⊢WcyclShiftL=WcyclShiftK→WcyclShiftLcyclShiftW−L=WcyclShiftKcyclShiftW−L
3 2 eqcomd ⊢WcyclShiftL=WcyclShiftK→WcyclShiftKcyclShiftW−L=WcyclShiftLcyclShiftW−L
4 3 ad2antrr ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡i≠W⁡0∧L∈0..^W∧K∈0..^W∧K<L→WcyclShiftKcyclShiftW−L=WcyclShiftLcyclShiftW−L
5 1 simpld ⊢φ→W∈WordV
6 5 adantr ⊢φ∧∃i∈0..^WW⁡i≠W⁡0→W∈WordV
7 6 adantl ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡i≠W⁡0→W∈WordV
8 7 adantr ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡i≠W⁡0∧L∈0..^W∧K∈0..^W∧K<L→W∈WordV
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 ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡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 ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡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 ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡i≠W⁡0∧L∈0..^W∧K∈0..^W∧K<L→K+W-L≤W
40 simpl ⊢W∈WordV∧K∈0…W∧W−L∈0…W∧K+W-L≤W→W∈WordV
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∈WordV∧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∈WordV∧K∈0…W∧W−L∈0…W∧K+W-L≤W→W−L∈ℤ
47 2cshw ⊢W∈WordV∧K∈ℤ∧W−L∈ℤ→WcyclShiftKcyclShiftW−L=WcyclShiftK+W-L
48 40 43 46 47 syl3anc ⊢W∈WordV∧K∈0…W∧W−L∈0…W∧K+W-L≤W→WcyclShiftKcyclShiftW−L=WcyclShiftK+W-L
49 8 11 16 39 48 syl13anc ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡i≠W⁡0∧L∈0..^W∧K∈0..^W∧K<L→WcyclShiftKcyclShiftW−L=WcyclShiftK+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∈WordV∧L∈ℤ→WcyclShiftLcyclShiftW−L=W
53 51 52 sylan2 ⊢W∈WordV∧L∈0…W→WcyclShiftLcyclShiftW−L=W
54 7 50 53 syl2an ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡i≠W⁡0∧L∈0..^W∧K∈0..^W∧K<L→WcyclShiftLcyclShiftW−L=W
55 4 49 54 3eqtr3d ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡i≠W⁡0∧L∈0..^W∧K∈0..^W∧K<L→WcyclShiftK+W-L=W
56 simplrl ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡i≠W⁡0∧L∈0..^W∧K∈0..^W∧K<L→φ
57 simplrr ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡i≠W⁡0∧L∈0..^W∧K∈0..^W∧K<L→∃i∈0..^WW⁡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 ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡i≠W⁡0∧L∈0..^W∧K∈0..^W∧K<L→K+W-L∈1..^W
95 1 cshwshashlem1 ⊢φ∧∃i∈0..^WW⁡i≠W⁡0∧K+W-L∈1..^W→WcyclShiftK+W-L≠W
96 56 57 94 95 syl3anc ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡i≠W⁡0∧L∈0..^W∧K∈0..^W∧K<L→WcyclShiftK+W-L≠W
97 55 96 pm2.21ddne ⊢WcyclShiftL=WcyclShiftK∧φ∧∃i∈0..^WW⁡i≠W⁡0∧L∈0..^W∧K∈0..^W∧K<L→WcyclShiftL≠WcyclShiftK
98 97 exp31 ⊢WcyclShiftL=WcyclShiftK→φ∧∃i∈0..^WW⁡i≠W⁡0→L∈0..^W∧K∈0..^W∧K<L→WcyclShiftL≠WcyclShiftK
99 2a1 ⊢WcyclShiftL≠WcyclShiftK→φ∧∃i∈0..^WW⁡i≠W⁡0→L∈0..^W∧K∈0..^W∧K<L→WcyclShiftL≠WcyclShiftK
100 98 99 pm2.61ine ⊢φ∧∃i∈0..^WW⁡i≠W⁡0→L∈0..^W∧K∈0..^W∧K<L→WcyclShiftL≠WcyclShiftK