Metamath Proof Explorer

Theorem cshwsublen

Description: Cyclically shifting a word is invariant regarding subtraction of the word's length. (Contributed by AV, 3-Nov-2018)

Ref Expression
Assertion cshwsublen ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W cyclShift N − W

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ W = 0 → N − W = N − 0
2 zcn ⊢ N ∈ ℤ → N ∈ ℂ
3 2 subid1d ⊢ N ∈ ℤ → N − 0 = N
4 3 adantl ⊢ W ∈ Word V ∧ N ∈ ℤ → N − 0 = N
5 1 4 sylan9eq ⊢ W = 0 ∧ W ∈ Word V ∧ N ∈ ℤ → N − W = N
6 5 eqcomd ⊢ W = 0 ∧ W ∈ Word V ∧ N ∈ ℤ → N = N − W
7 6 oveq2d ⊢ W = 0 ∧ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W cyclShift N − W
8 7 ex ⊢ W = 0 → W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W cyclShift N − W
9 zre ⊢ N ∈ ℤ → N ∈ ℝ
10 9 adantl ⊢ W ∈ Word V ∧ N ∈ ℤ → N ∈ ℝ
11 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
12 elnnne0 ⊢ W ∈ ℕ ↔ W ∈ ℕ 0 ∧ W ≠ 0
13 nnrp ⊢ W ∈ ℕ → W ∈ ℝ +
14 12 13 sylbir ⊢ W ∈ ℕ 0 ∧ W ≠ 0 → W ∈ ℝ +
15 14 ex ⊢ W ∈ ℕ 0 → W ≠ 0 → W ∈ ℝ +
16 11 15 syl ⊢ W ∈ Word V → W ≠ 0 → W ∈ ℝ +
17 16 adantr ⊢ W ∈ Word V ∧ N ∈ ℤ → W ≠ 0 → W ∈ ℝ +
18 17 impcom ⊢ W ≠ 0 ∧ W ∈ Word V ∧ N ∈ ℤ → W ∈ ℝ +
19 modeqmodmin ⊢ N ∈ ℝ ∧ W ∈ ℝ + → N mod W = N − W mod W
20 10 18 19 syl2an2 ⊢ W ≠ 0 ∧ W ∈ Word V ∧ N ∈ ℤ → N mod W = N − W mod W
21 20 oveq2d ⊢ W ≠ 0 ∧ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N mod W = W cyclShift N − W mod W
22 cshwmodn ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W cyclShift N mod W
23 22 adantl ⊢ W ≠ 0 ∧ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W cyclShift N mod W
24 simpl ⊢ W ∈ Word V ∧ N ∈ ℤ → W ∈ Word V
25 11 nn0zd ⊢ W ∈ Word V → W ∈ ℤ
26 zsubcl ⊢ N ∈ ℤ ∧ W ∈ ℤ → N − W ∈ ℤ
27 25 26 sylan2 ⊢ N ∈ ℤ ∧ W ∈ Word V → N − W ∈ ℤ
28 27 ancoms ⊢ W ∈ Word V ∧ N ∈ ℤ → N − W ∈ ℤ
29 24 28 jca ⊢ W ∈ Word V ∧ N ∈ ℤ → W ∈ Word V ∧ N − W ∈ ℤ
30 29 adantl ⊢ W ≠ 0 ∧ W ∈ Word V ∧ N ∈ ℤ → W ∈ Word V ∧ N − W ∈ ℤ
31 cshwmodn ⊢ W ∈ Word V ∧ N − W ∈ ℤ → W cyclShift N − W = W cyclShift N − W mod W
32 30 31 syl ⊢ W ≠ 0 ∧ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N − W = W cyclShift N − W mod W
33 21 23 32 3eqtr4d ⊢ W ≠ 0 ∧ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W cyclShift N − W
34 33 ex ⊢ W ≠ 0 → W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W cyclShift N − W
35 8 34 pm2.61ine ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W cyclShift N − W