Proof of Theorem cshwidxm1
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → 𝑊 ∈ Word 𝑉) |
2 | | elfzoelz 12339 |
. . . 4
⊢ (𝑁 ∈ (0..^(#‘𝑊)) → 𝑁 ∈ ℤ) |
3 | 2 | adantl 481 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → 𝑁 ∈ ℤ) |
4 | | ubmelm1fzo 12430 |
. . . 4
⊢ (𝑁 ∈ (0..^(#‘𝑊)) → (((#‘𝑊) − 𝑁) − 1) ∈ (0..^(#‘𝑊))) |
5 | 4 | adantl 481 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (((#‘𝑊) − 𝑁) − 1) ∈ (0..^(#‘𝑊))) |
6 | | cshwidxmod 13400 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (((#‘𝑊) − 𝑁) − 1) ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘(((#‘𝑊) − 𝑁) − 1)) = (𝑊‘(((((#‘𝑊) − 𝑁) − 1) + 𝑁) mod (#‘𝑊)))) |
7 | 1, 3, 5, 6 | syl3anc 1318 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘(((#‘𝑊) − 𝑁) − 1)) = (𝑊‘(((((#‘𝑊) − 𝑁) − 1) + 𝑁) mod (#‘𝑊)))) |
8 | | elfzoel2 12338 |
. . . . . . . 8
⊢ (𝑁 ∈ (0..^(#‘𝑊)) → (#‘𝑊) ∈
ℤ) |
9 | 8 | zcnd 11359 |
. . . . . . 7
⊢ (𝑁 ∈ (0..^(#‘𝑊)) → (#‘𝑊) ∈
ℂ) |
10 | 2 | zcnd 11359 |
. . . . . . 7
⊢ (𝑁 ∈ (0..^(#‘𝑊)) → 𝑁 ∈ ℂ) |
11 | | 1cnd 9935 |
. . . . . . 7
⊢ (𝑁 ∈ (0..^(#‘𝑊)) → 1 ∈
ℂ) |
12 | | nnpcan 10183 |
. . . . . . 7
⊢
(((#‘𝑊) ∈
ℂ ∧ 𝑁 ∈
ℂ ∧ 1 ∈ ℂ) → ((((#‘𝑊) − 𝑁) − 1) + 𝑁) = ((#‘𝑊) − 1)) |
13 | 9, 10, 11, 12 | syl3anc 1318 |
. . . . . 6
⊢ (𝑁 ∈ (0..^(#‘𝑊)) → ((((#‘𝑊) − 𝑁) − 1) + 𝑁) = ((#‘𝑊) − 1)) |
14 | 13 | oveq1d 6564 |
. . . . 5
⊢ (𝑁 ∈ (0..^(#‘𝑊)) → (((((#‘𝑊) − 𝑁) − 1) + 𝑁) mod (#‘𝑊)) = (((#‘𝑊) − 1) mod (#‘𝑊))) |
15 | 14 | adantl 481 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (((((#‘𝑊) − 𝑁) − 1) + 𝑁) mod (#‘𝑊)) = (((#‘𝑊) − 1) mod (#‘𝑊))) |
16 | | elfzo0 12376 |
. . . . . . . 8
⊢ (𝑁 ∈ (0..^(#‘𝑊)) ↔ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝑁 < (#‘𝑊))) |
17 | | nnre 10904 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℝ) |
18 | | peano2rem 10227 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
ℝ → ((#‘𝑊)
− 1) ∈ ℝ) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
ℕ → ((#‘𝑊)
− 1) ∈ ℝ) |
20 | | nnrp 11718 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℝ+) |
21 | 19, 20 | jca 553 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℕ → (((#‘𝑊) − 1) ∈ ℝ ∧
(#‘𝑊) ∈
ℝ+)) |
22 | 21 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ 𝑁 <
(#‘𝑊)) →
(((#‘𝑊) − 1)
∈ ℝ ∧ (#‘𝑊) ∈
ℝ+)) |
23 | 16, 22 | sylbi 206 |
. . . . . . 7
⊢ (𝑁 ∈ (0..^(#‘𝑊)) → (((#‘𝑊) − 1) ∈ ℝ
∧ (#‘𝑊) ∈
ℝ+)) |
24 | | nnm1ge0 11321 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℕ → 0 ≤ ((#‘𝑊) − 1)) |
25 | 24 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ 𝑁 <
(#‘𝑊)) → 0 ≤
((#‘𝑊) −
1)) |
26 | 16, 25 | sylbi 206 |
. . . . . . 7
⊢ (𝑁 ∈ (0..^(#‘𝑊)) → 0 ≤ ((#‘𝑊) − 1)) |
27 | | zre 11258 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℤ → (#‘𝑊)
∈ ℝ) |
28 | 27 | ltm1d 10835 |
. . . . . . . 8
⊢
((#‘𝑊) ∈
ℤ → ((#‘𝑊)
− 1) < (#‘𝑊)) |
29 | 8, 28 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ (0..^(#‘𝑊)) → ((#‘𝑊) − 1) < (#‘𝑊)) |
30 | 23, 26, 29 | jca32 556 |
. . . . . 6
⊢ (𝑁 ∈ (0..^(#‘𝑊)) → ((((#‘𝑊) − 1) ∈ ℝ
∧ (#‘𝑊) ∈
ℝ+) ∧ (0 ≤ ((#‘𝑊) − 1) ∧ ((#‘𝑊) − 1) < (#‘𝑊)))) |
31 | 30 | adantl 481 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → ((((#‘𝑊) − 1) ∈ ℝ ∧
(#‘𝑊) ∈
ℝ+) ∧ (0 ≤ ((#‘𝑊) − 1) ∧ ((#‘𝑊) − 1) < (#‘𝑊)))) |
32 | | modid 12557 |
. . . . 5
⊢
(((((#‘𝑊)
− 1) ∈ ℝ ∧ (#‘𝑊) ∈ ℝ+) ∧ (0 ≤
((#‘𝑊) − 1)
∧ ((#‘𝑊) −
1) < (#‘𝑊)))
→ (((#‘𝑊)
− 1) mod (#‘𝑊))
= ((#‘𝑊) −
1)) |
33 | 31, 32 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (((#‘𝑊) − 1) mod (#‘𝑊)) = ((#‘𝑊) − 1)) |
34 | 15, 33 | eqtrd 2644 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (((((#‘𝑊) − 𝑁) − 1) + 𝑁) mod (#‘𝑊)) = ((#‘𝑊) − 1)) |
35 | 34 | fveq2d 6107 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (𝑊‘(((((#‘𝑊) − 𝑁) − 1) + 𝑁) mod (#‘𝑊))) = (𝑊‘((#‘𝑊) − 1))) |
36 | 7, 35 | eqtrd 2644 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘(((#‘𝑊) − 𝑁) − 1)) = (𝑊‘((#‘𝑊) − 1))) |