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 ⊢ ( 𝜑 → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) ∈ ℙ ) )
Assertion cshwshashlem2 ( ( 𝜑 ∧ ∃ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 ‘ 𝑖 ) ≠ ( 𝑊 ‘ 0 ) ) → ( ( 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐾 < 𝐿 ) → ( 𝑊 cyclShift 𝐿 ) ≠ ( 𝑊 cyclShift 𝐾 ) ) )

Proof

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