Metamath Proof Explorer

Theorem clwwisshclwwslem

Description: Lemma for clwwisshclwws . (Contributed by AV, 24-Mar-2018) (Revised by AV, 28-Apr-2021)

Ref Expression
Assertion clwwisshclwwslem ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E → ∀ j ∈ 0 ..^ W cyclShift N − 1 W cyclShift N ⁡ j W cyclShift N ⁡ j + 1 ∈ E

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢ N ∈ 1 ..^ W → N ∈ ℤ
2 cshwlen ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W
3 1 2 sylan2 ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W → W cyclShift N = W
4 3 oveq1d ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W → W cyclShift N − 1 = W − 1
5 4 oveq2d ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W → 0 ..^ W cyclShift N − 1 = 0 ..^ W − 1
6 5 eleq2d ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W → j ∈ 0 ..^ W cyclShift N − 1 ↔ j ∈ 0 ..^ W − 1
7 6 adantr ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E → j ∈ 0 ..^ W cyclShift N − 1 ↔ j ∈ 0 ..^ W − 1
8 simpll ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ j ∈ 0 ..^ W − 1 → W ∈ Word V
9 1 ad2antlr ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ j ∈ 0 ..^ W − 1 → N ∈ ℤ
10 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
11 nn0z ⊢ W ∈ ℕ 0 → W ∈ ℤ
12 peano2zm ⊢ W ∈ ℤ → W − 1 ∈ ℤ
13 11 12 syl ⊢ W ∈ ℕ 0 → W − 1 ∈ ℤ
14 nn0re ⊢ W ∈ ℕ 0 → W ∈ ℝ
15 14 lem1d ⊢ W ∈ ℕ 0 → W − 1 ≤ W
16 eluz2 ⊢ W ∈ ℤ ≥ W − 1 ↔ W − 1 ∈ ℤ ∧ W ∈ ℤ ∧ W − 1 ≤ W
17 13 11 15 16 syl3anbrc ⊢ W ∈ ℕ 0 → W ∈ ℤ ≥ W − 1
18 10 17 syl ⊢ W ∈ Word V → W ∈ ℤ ≥ W − 1
19 18 adantr ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W → W ∈ ℤ ≥ W − 1
20 fzoss2 ⊢ W ∈ ℤ ≥ W − 1 → 0 ..^ W − 1 ⊆ 0 ..^ W
21 19 20 syl ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W → 0 ..^ W − 1 ⊆ 0 ..^ W
22 21 sselda ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ j ∈ 0 ..^ W − 1 → j ∈ 0 ..^ W
23 cshwidxmod ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ j ∈ 0 ..^ W → W cyclShift N ⁡ j = W ⁡ j + N mod W
24 8 9 22 23 syl3anc ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ j ∈ 0 ..^ W − 1 → W cyclShift N ⁡ j = W ⁡ j + N mod W
25 elfzo1 ⊢ N ∈ 1 ..^ W ↔ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W
26 25 simp2bi ⊢ N ∈ 1 ..^ W → W ∈ ℕ
27 26 adantl ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W → W ∈ ℕ
28 elfzom1p1elfzo ⊢ W ∈ ℕ ∧ j ∈ 0 ..^ W − 1 → j + 1 ∈ 0 ..^ W
29 27 28 sylan ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ j ∈ 0 ..^ W − 1 → j + 1 ∈ 0 ..^ W
30 cshwidxmod ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ j + 1 ∈ 0 ..^ W → W cyclShift N ⁡ j + 1 = W ⁡ j + 1 + N mod W
31 8 9 29 30 syl3anc ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ j ∈ 0 ..^ W − 1 → W cyclShift N ⁡ j + 1 = W ⁡ j + 1 + N mod W
32 24 31 preq12d ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ j ∈ 0 ..^ W − 1 → W cyclShift N ⁡ j W cyclShift N ⁡ j + 1 = W ⁡ j + N mod W W ⁡ j + 1 + N mod W
33 32 adantlr ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ j ∈ 0 ..^ W − 1 → W cyclShift N ⁡ j W cyclShift N ⁡ j + 1 = W ⁡ j + N mod W W ⁡ j + 1 + N mod W
34 2z ⊢ 2 ∈ ℤ
35 34 a1i ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → 2 ∈ ℤ
36 nnz ⊢ W ∈ ℕ → W ∈ ℤ
37 36 3ad2ant2 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → W ∈ ℤ
38 nnnn0 ⊢ W ∈ ℕ → W ∈ ℕ 0
39 38 3ad2ant2 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → W ∈ ℕ 0
40 nnne0 ⊢ W ∈ ℕ → W ≠ 0
41 40 3ad2ant2 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → W ≠ 0
42 1red ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → 1 ∈ ℝ
43 nnre ⊢ N ∈ ℕ → N ∈ ℝ
44 43 3ad2ant1 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → N ∈ ℝ
45 nnre ⊢ W ∈ ℕ → W ∈ ℝ
46 45 3ad2ant2 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → W ∈ ℝ
47 nnge1 ⊢ N ∈ ℕ → 1 ≤ N
48 47 3ad2ant1 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → 1 ≤ N
49 simp3 ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → N < W
50 42 44 46 48 49 lelttrd ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → 1 < W
51 42 50 gtned ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → W ≠ 1
52 nn0n0n1ge2 ⊢ W ∈ ℕ 0 ∧ W ≠ 0 ∧ W ≠ 1 → 2 ≤ W
53 39 41 51 52 syl3anc ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → 2 ≤ W
54 eluz2 ⊢ W ∈ ℤ ≥ 2 ↔ 2 ∈ ℤ ∧ W ∈ ℤ ∧ 2 ≤ W
55 35 37 53 54 syl3anbrc ⊢ N ∈ ℕ ∧ W ∈ ℕ ∧ N < W → W ∈ ℤ ≥ 2
56 25 55 sylbi ⊢ N ∈ 1 ..^ W → W ∈ ℤ ≥ 2
57 56 ad3antlr ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ j ∈ 0 ..^ W − 1 → W ∈ ℤ ≥ 2
58 elfzoelz ⊢ j ∈ 0 ..^ W − 1 → j ∈ ℤ
59 58 adantl ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ j ∈ 0 ..^ W − 1 → j ∈ ℤ
60 1 ad3antlr ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ j ∈ 0 ..^ W − 1 → N ∈ ℤ
61 simplrl ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ j ∈ 0 ..^ W − 1 → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E
62 lsw ⊢ W ∈ Word V → lastS ⁡ W = W ⁡ W − 1
63 62 adantr ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W → lastS ⁡ W = W ⁡ W − 1
64 63 preq1d ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W → lastS ⁡ W W ⁡ 0 = W ⁡ W − 1 W ⁡ 0
65 64 eleq1d ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W → lastS ⁡ W W ⁡ 0 ∈ E ↔ W ⁡ W − 1 W ⁡ 0 ∈ E
66 65 biimpcd ⊢ lastS ⁡ W W ⁡ 0 ∈ E → W ∈ Word V ∧ N ∈ 1 ..^ W → W ⁡ W − 1 W ⁡ 0 ∈ E
67 66 adantl ⊢ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E → W ∈ Word V ∧ N ∈ 1 ..^ W → W ⁡ W − 1 W ⁡ 0 ∈ E
68 67 impcom ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E → W ⁡ W − 1 W ⁡ 0 ∈ E
69 68 adantr ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ j ∈ 0 ..^ W − 1 → W ⁡ W − 1 W ⁡ 0 ∈ E
70 clwwisshclwwslemlem ⊢ W ∈ ℤ ≥ 2 ∧ j ∈ ℤ ∧ N ∈ ℤ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ W ⁡ W − 1 W ⁡ 0 ∈ E → W ⁡ j + N mod W W ⁡ j + 1 + N mod W ∈ E
71 57 59 60 61 69 70 syl311anc ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ j ∈ 0 ..^ W − 1 → W ⁡ j + N mod W W ⁡ j + 1 + N mod W ∈ E
72 33 71 eqeltrd ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ j ∈ 0 ..^ W − 1 → W cyclShift N ⁡ j W cyclShift N ⁡ j + 1 ∈ E
73 72 ex ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E → j ∈ 0 ..^ W − 1 → W cyclShift N ⁡ j W cyclShift N ⁡ j + 1 ∈ E
74 7 73 sylbid ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E → j ∈ 0 ..^ W cyclShift N − 1 → W cyclShift N ⁡ j W cyclShift N ⁡ j + 1 ∈ E
75 74 ralrimiv ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E → ∀ j ∈ 0 ..^ W cyclShift N − 1 W cyclShift N ⁡ j W cyclShift N ⁡ j + 1 ∈ E
76 75 ex ⊢ W ∈ Word V ∧ N ∈ 1 ..^ W → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E → ∀ j ∈ 0 ..^ W cyclShift N − 1 W cyclShift N ⁡ j W cyclShift N ⁡ j + 1 ∈ E