Metamath Proof Explorer

Theorem cshwidxmodr

Description: The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 17-Mar-2021)

Ref Expression
Assertion cshwidxmodr ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ I ∈ 0 ..^ W → W cyclShift N ⁡ I − N mod W = W ⁡ I

Proof

Step Hyp Ref Expression
1 elfzo0 ⊢ I ∈ 0 ..^ W ↔ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I < W
2 nn0z ⊢ I ∈ ℕ 0 → I ∈ ℤ
3 2 3ad2ant1 ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I < W → I ∈ ℤ
4 zsubcl ⊢ I ∈ ℤ ∧ N ∈ ℤ → I − N ∈ ℤ
5 3 4 sylan ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I < W ∧ N ∈ ℤ → I − N ∈ ℤ
6 simpl2 ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I < W ∧ N ∈ ℤ → W ∈ ℕ
7 5 6 jca ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I < W ∧ N ∈ ℤ → I − N ∈ ℤ ∧ W ∈ ℕ
8 7 ex ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I < W → N ∈ ℤ → I − N ∈ ℤ ∧ W ∈ ℕ
9 1 8 sylbi ⊢ I ∈ 0 ..^ W → N ∈ ℤ → I − N ∈ ℤ ∧ W ∈ ℕ
10 9 impcom ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ W → I − N ∈ ℤ ∧ W ∈ ℕ
11 10 3adant1 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ I ∈ 0 ..^ W → I − N ∈ ℤ ∧ W ∈ ℕ
12 zmodfzo ⊢ I − N ∈ ℤ ∧ W ∈ ℕ → I − N mod W ∈ 0 ..^ W
13 11 12 syl ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ I ∈ 0 ..^ W → I − N mod W ∈ 0 ..^ W
14 cshwidxmod ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ I − N mod W ∈ 0 ..^ W → W cyclShift N ⁡ I − N mod W = W ⁡ I − N mod W + N mod W
15 13 14 syld3an3 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ I ∈ 0 ..^ W → W cyclShift N ⁡ I − N mod W = W ⁡ I − N mod W + N mod W
16 elfzoelz ⊢ I ∈ 0 ..^ W → I ∈ ℤ
17 16 adantl ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W → I ∈ ℤ
18 17 4 sylan ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W ∧ N ∈ ℤ → I − N ∈ ℤ
19 18 zred ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W ∧ N ∈ ℤ → I − N ∈ ℝ
20 zre ⊢ N ∈ ℤ → N ∈ ℝ
21 20 adantl ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W ∧ N ∈ ℤ → N ∈ ℝ
22 nnrp ⊢ W ∈ ℕ → W ∈ ℝ +
23 22 ad3antlr ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W ∧ N ∈ ℤ → W ∈ ℝ +
24 modaddmod ⊢ I − N ∈ ℝ ∧ N ∈ ℝ ∧ W ∈ ℝ + → I − N mod W + N mod W = I - N + N mod W
25 19 21 23 24 syl3anc ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W ∧ N ∈ ℤ → I − N mod W + N mod W = I - N + N mod W
26 nn0cn ⊢ I ∈ ℕ 0 → I ∈ ℂ
27 26 ad2antrr ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W → I ∈ ℂ
28 zcn ⊢ N ∈ ℤ → N ∈ ℂ
29 npcan ⊢ I ∈ ℂ ∧ N ∈ ℂ → I - N + N = I
30 27 28 29 syl2an ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W ∧ N ∈ ℤ → I - N + N = I
31 30 oveq1d ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W ∧ N ∈ ℤ → I - N + N mod W = I mod W
32 zmodidfzoimp ⊢ I ∈ 0 ..^ W → I mod W = I
33 32 ad2antlr ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W ∧ N ∈ ℤ → I mod W = I
34 25 31 33 3eqtrd ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W ∧ N ∈ ℤ → I − N mod W + N mod W = I
35 34 fveq2d ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W ∧ N ∈ ℤ → W ⁡ I − N mod W + N mod W = W ⁡ I
36 35 ex ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I ∈ 0 ..^ W → N ∈ ℤ → W ⁡ I − N mod W + N mod W = W ⁡ I
37 36 ex ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ → I ∈ 0 ..^ W → N ∈ ℤ → W ⁡ I − N mod W + N mod W = W ⁡ I
38 37 3adant3 ⊢ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I < W → I ∈ 0 ..^ W → N ∈ ℤ → W ⁡ I − N mod W + N mod W = W ⁡ I
39 1 38 sylbi ⊢ I ∈ 0 ..^ W → I ∈ 0 ..^ W → N ∈ ℤ → W ⁡ I − N mod W + N mod W = W ⁡ I
40 39 pm2.43i ⊢ I ∈ 0 ..^ W → N ∈ ℤ → W ⁡ I − N mod W + N mod W = W ⁡ I
41 40 impcom ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ W → W ⁡ I − N mod W + N mod W = W ⁡ I
42 41 3adant1 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ I ∈ 0 ..^ W → W ⁡ I − N mod W + N mod W = W ⁡ I
43 15 42 eqtrd ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ I ∈ 0 ..^ W → W cyclShift N ⁡ I − N mod W = W ⁡ I