Proof of Theorem cshwidxn
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑊))) → 𝑊 ∈ Word 𝑉) |
2 | | elfzelz 12213 |
. . . 4
⊢ (𝑁 ∈ (1...(#‘𝑊)) → 𝑁 ∈ ℤ) |
3 | 2 | adantl 481 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑊))) → 𝑁 ∈ ℤ) |
4 | | elfz1b 12279 |
. . . . . 6
⊢ (𝑁 ∈ (1...(#‘𝑊)) ↔ (𝑁 ∈ ℕ ∧ (#‘𝑊) ∈ ℕ ∧ 𝑁 ≤ (#‘𝑊))) |
5 | | simp2 1055 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 ≤ (#‘𝑊)) → (#‘𝑊) ∈
ℕ) |
6 | 4, 5 | sylbi 206 |
. . . . 5
⊢ (𝑁 ∈ (1...(#‘𝑊)) → (#‘𝑊) ∈
ℕ) |
7 | 6 | adantl 481 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑊))) → (#‘𝑊) ∈ ℕ) |
8 | | fzo0end 12426 |
. . . 4
⊢
((#‘𝑊) ∈
ℕ → ((#‘𝑊)
− 1) ∈ (0..^(#‘𝑊))) |
9 | 7, 8 | syl 17 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑊))) → ((#‘𝑊) − 1) ∈ (0..^(#‘𝑊))) |
10 | | cshwidxmod 13400 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ((#‘𝑊) − 1) ∈
(0..^(#‘𝑊))) →
((𝑊 cyclShift 𝑁)‘((#‘𝑊) − 1)) = (𝑊‘((((#‘𝑊) − 1) + 𝑁) mod (#‘𝑊)))) |
11 | 1, 3, 9, 10 | syl3anc 1318 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((#‘𝑊) − 1)) = (𝑊‘((((#‘𝑊) − 1) + 𝑁) mod (#‘𝑊)))) |
12 | | nncn 10905 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℂ) |
13 | 12 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ)
→ (#‘𝑊) ∈
ℂ) |
14 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ)
→ 1 ∈ ℂ) |
15 | | nncn 10905 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
16 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ)
→ 𝑁 ∈
ℂ) |
17 | 13, 14, 16 | 3jca 1235 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ)
→ ((#‘𝑊) ∈
ℂ ∧ 1 ∈ ℂ ∧ 𝑁 ∈ ℂ)) |
18 | 17 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 ≤ (#‘𝑊)) → ((#‘𝑊) ∈ ℂ ∧ 1 ∈
ℂ ∧ 𝑁 ∈
ℂ)) |
19 | 4, 18 | sylbi 206 |
. . . . . . 7
⊢ (𝑁 ∈ (1...(#‘𝑊)) → ((#‘𝑊) ∈ ℂ ∧ 1 ∈
ℂ ∧ 𝑁 ∈
ℂ)) |
20 | | subadd23 10172 |
. . . . . . 7
⊢
(((#‘𝑊) ∈
ℂ ∧ 1 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((#‘𝑊) − 1) + 𝑁) = ((#‘𝑊) + (𝑁 − 1))) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ (1...(#‘𝑊)) → (((#‘𝑊) − 1) + 𝑁) = ((#‘𝑊) + (𝑁 − 1))) |
22 | 21 | oveq1d 6564 |
. . . . 5
⊢ (𝑁 ∈ (1...(#‘𝑊)) → ((((#‘𝑊) − 1) + 𝑁) mod (#‘𝑊)) = (((#‘𝑊) + (𝑁 − 1)) mod (#‘𝑊))) |
23 | | nnm1nn0 11211 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
24 | 23 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 ≤ (#‘𝑊)) → (𝑁 − 1) ∈
ℕ0) |
25 | | simp3 1056 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 ≤ (#‘𝑊)) → 𝑁 ≤ (#‘𝑊)) |
26 | | nnz 11276 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
27 | | nnz 11276 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℤ) |
28 | 26, 27 | anim12i 588 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ)
→ (𝑁 ∈ ℤ
∧ (#‘𝑊) ∈
ℤ)) |
29 | 28 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 ≤ (#‘𝑊)) → (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈
ℤ)) |
30 | | zlem1lt 11306 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧
(#‘𝑊) ∈ ℤ)
→ (𝑁 ≤
(#‘𝑊) ↔ (𝑁 − 1) < (#‘𝑊))) |
31 | 29, 30 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 ≤ (#‘𝑊)) → (𝑁 ≤ (#‘𝑊) ↔ (𝑁 − 1) < (#‘𝑊))) |
32 | 25, 31 | mpbid 221 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 ≤ (#‘𝑊)) → (𝑁 − 1) < (#‘𝑊)) |
33 | 24, 5, 32 | 3jca 1235 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 ≤ (#‘𝑊)) → ((𝑁 − 1) ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ (𝑁 − 1) <
(#‘𝑊))) |
34 | 4, 33 | sylbi 206 |
. . . . . 6
⊢ (𝑁 ∈ (1...(#‘𝑊)) → ((𝑁 − 1) ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ (𝑁 − 1) <
(#‘𝑊))) |
35 | | addmodid 12580 |
. . . . . 6
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ (#‘𝑊) ∈ ℕ ∧ (𝑁 − 1) < (#‘𝑊)) → (((#‘𝑊) + (𝑁 − 1)) mod (#‘𝑊)) = (𝑁 − 1)) |
36 | 34, 35 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ (1...(#‘𝑊)) → (((#‘𝑊) + (𝑁 − 1)) mod (#‘𝑊)) = (𝑁 − 1)) |
37 | 22, 36 | eqtrd 2644 |
. . . 4
⊢ (𝑁 ∈ (1...(#‘𝑊)) → ((((#‘𝑊) − 1) + 𝑁) mod (#‘𝑊)) = (𝑁 − 1)) |
38 | 37 | fveq2d 6107 |
. . 3
⊢ (𝑁 ∈ (1...(#‘𝑊)) → (𝑊‘((((#‘𝑊) − 1) + 𝑁) mod (#‘𝑊))) = (𝑊‘(𝑁 − 1))) |
39 | 38 | adantl 481 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑊))) → (𝑊‘((((#‘𝑊) − 1) + 𝑁) mod (#‘𝑊))) = (𝑊‘(𝑁 − 1))) |
40 | 11, 39 | eqtrd 2644 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((#‘𝑊) − 1)) = (𝑊‘(𝑁 − 1))) |