Metamath Proof Explorer

Theorem cshwshashlem3

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 cshwshashlem3 ⊢ φ ∧ ∃ 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 elfzoelz ⊢ K ∈ 0 ..^ W → K ∈ ℤ
3 2 zred ⊢ K ∈ 0 ..^ W → K ∈ ℝ
4 elfzoelz ⊢ L ∈ 0 ..^ W → L ∈ ℤ
5 4 zred ⊢ L ∈ 0 ..^ W → L ∈ ℝ
6 lttri2 ⊢ K ∈ ℝ ∧ L ∈ ℝ → K ≠ L ↔ K < L ∨ L < K
7 3 5 6 syl2anr ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W → K ≠ L ↔ K < L ∨ L < K
8 1 cshwshashlem2 ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → W cyclShift L ≠ W cyclShift K
9 8 com12 ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K < L → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → W cyclShift L ≠ W cyclShift K
10 9 3expia ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W → K < L → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → W cyclShift L ≠ W cyclShift K
11 1 cshwshashlem2 ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → K ∈ 0 ..^ W ∧ L ∈ 0 ..^ W ∧ L < K → W cyclShift K ≠ W cyclShift L
12 11 imp ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ K ∈ 0 ..^ W ∧ L ∈ 0 ..^ W ∧ L < K → W cyclShift K ≠ W cyclShift L
13 12 necomd ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 ∧ K ∈ 0 ..^ W ∧ L ∈ 0 ..^ W ∧ L < K → W cyclShift L ≠ W cyclShift K
14 13 expcom ⊢ K ∈ 0 ..^ W ∧ L ∈ 0 ..^ W ∧ L < K → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → W cyclShift L ≠ W cyclShift K
15 14 3expia ⊢ K ∈ 0 ..^ W ∧ L ∈ 0 ..^ W → L < K → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → W cyclShift L ≠ W cyclShift K
16 15 ancoms ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W → L < K → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → W cyclShift L ≠ W cyclShift K
17 10 16 jaod ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W → K < L ∨ L < K → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → W cyclShift L ≠ W cyclShift K
18 7 17 sylbid ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W → K ≠ L → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → W cyclShift L ≠ W cyclShift K
19 18 3impia ⊢ L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K ≠ L → φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → W cyclShift L ≠ W cyclShift K
20 19 com12 ⊢ φ ∧ ∃ i ∈ 0 ..^ W W ⁡ i ≠ W ⁡ 0 → L ∈ 0 ..^ W ∧ K ∈ 0 ..^ W ∧ K ≠ L → W cyclShift L ≠ W cyclShift K