Proof of Theorem cshwmodn
Step | Hyp | Ref
| Expression |
1 | | 0csh0 13390 |
. . . 4
⊢ (∅
cyclShift 𝑁) =
∅ |
2 | | oveq1 6556 |
. . . 4
⊢ (𝑊 = ∅ → (𝑊 cyclShift 𝑁) = (∅ cyclShift 𝑁)) |
3 | | oveq1 6556 |
. . . . 5
⊢ (𝑊 = ∅ → (𝑊 cyclShift (𝑁 mod (#‘𝑊))) = (∅ cyclShift (𝑁 mod (#‘𝑊)))) |
4 | | 0csh0 13390 |
. . . . 5
⊢ (∅
cyclShift (𝑁 mod
(#‘𝑊))) =
∅ |
5 | 3, 4 | syl6eq 2660 |
. . . 4
⊢ (𝑊 = ∅ → (𝑊 cyclShift (𝑁 mod (#‘𝑊))) = ∅) |
6 | 1, 2, 5 | 3eqtr4a 2670 |
. . 3
⊢ (𝑊 = ∅ → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (#‘𝑊)))) |
7 | 6 | a1d 25 |
. 2
⊢ (𝑊 = ∅ → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (#‘𝑊))))) |
8 | | lennncl 13180 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈
ℕ) |
9 | | zre 11258 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
10 | | nnrp 11718 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℝ+) |
11 | | modabs2 12566 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧
(#‘𝑊) ∈
ℝ+) → ((𝑁 mod (#‘𝑊)) mod (#‘𝑊)) = (𝑁 mod (#‘𝑊))) |
12 | 9, 10, 11 | syl2anr 494 |
. . . . . . . . . . 11
⊢
(((#‘𝑊) ∈
ℕ ∧ 𝑁 ∈
ℤ) → ((𝑁 mod
(#‘𝑊)) mod
(#‘𝑊)) = (𝑁 mod (#‘𝑊))) |
13 | 12 | opeq1d 4346 |
. . . . . . . . . 10
⊢
(((#‘𝑊) ∈
ℕ ∧ 𝑁 ∈
ℤ) → 〈((𝑁
mod (#‘𝑊)) mod
(#‘𝑊)),
(#‘𝑊)〉 =
〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) |
14 | 13 | oveq2d 6565 |
. . . . . . . . 9
⊢
(((#‘𝑊) ∈
ℕ ∧ 𝑁 ∈
ℤ) → (𝑊 substr
〈((𝑁 mod
(#‘𝑊)) mod
(#‘𝑊)),
(#‘𝑊)〉) = (𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) |
15 | 12 | opeq2d 4347 |
. . . . . . . . . 10
⊢
(((#‘𝑊) ∈
ℕ ∧ 𝑁 ∈
ℤ) → 〈0, ((𝑁 mod (#‘𝑊)) mod (#‘𝑊))〉 = 〈0, (𝑁 mod (#‘𝑊))〉) |
16 | 15 | oveq2d 6565 |
. . . . . . . . 9
⊢
(((#‘𝑊) ∈
ℕ ∧ 𝑁 ∈
ℤ) → (𝑊 substr
〈0, ((𝑁 mod
(#‘𝑊)) mod
(#‘𝑊))〉) =
(𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)) |
17 | 14, 16 | oveq12d 6567 |
. . . . . . . 8
⊢
(((#‘𝑊) ∈
ℕ ∧ 𝑁 ∈
ℤ) → ((𝑊 substr
〈((𝑁 mod
(#‘𝑊)) mod
(#‘𝑊)),
(#‘𝑊)〉) ++
(𝑊 substr 〈0, ((𝑁 mod (#‘𝑊)) mod (#‘𝑊))〉)) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
18 | 17 | ex 449 |
. . . . . . 7
⊢
((#‘𝑊) ∈
ℕ → (𝑁 ∈
ℤ → ((𝑊 substr
〈((𝑁 mod
(#‘𝑊)) mod
(#‘𝑊)),
(#‘𝑊)〉) ++
(𝑊 substr 〈0, ((𝑁 mod (#‘𝑊)) mod (#‘𝑊))〉)) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
19 | 8, 18 | syl 17 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑁 ∈ ℤ → ((𝑊 substr 〈((𝑁 mod (#‘𝑊)) mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, ((𝑁 mod (#‘𝑊)) mod (#‘𝑊))〉)) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
20 | 19 | impancom 455 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 ≠ ∅ → ((𝑊 substr 〈((𝑁 mod (#‘𝑊)) mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, ((𝑁 mod (#‘𝑊)) mod (#‘𝑊))〉)) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
21 | 20 | impcom 445 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → ((𝑊 substr 〈((𝑁 mod (#‘𝑊)) mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, ((𝑁 mod (#‘𝑊)) mod (#‘𝑊))〉)) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
22 | | simprl 790 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → 𝑊 ∈ Word 𝑉) |
23 | | simprr 792 |
. . . . . . 7
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℤ) |
24 | 8 | ex 449 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ → (#‘𝑊) ∈
ℕ)) |
25 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 ≠ ∅ → (#‘𝑊) ∈
ℕ)) |
26 | 25 | impcom 445 |
. . . . . . 7
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (#‘𝑊) ∈
ℕ) |
27 | 23, 26 | zmodcld 12553 |
. . . . . 6
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑁 mod (#‘𝑊)) ∈
ℕ0) |
28 | 27 | nn0zd 11356 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑁 mod (#‘𝑊)) ∈ ℤ) |
29 | | cshword 13388 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (#‘𝑊)) ∈ ℤ) → (𝑊 cyclShift (𝑁 mod (#‘𝑊))) = ((𝑊 substr 〈((𝑁 mod (#‘𝑊)) mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, ((𝑁 mod (#‘𝑊)) mod (#‘𝑊))〉))) |
30 | 22, 28, 29 | syl2anc 691 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑊 cyclShift (𝑁 mod (#‘𝑊))) = ((𝑊 substr 〈((𝑁 mod (#‘𝑊)) mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, ((𝑁 mod (#‘𝑊)) mod (#‘𝑊))〉))) |
31 | | cshword 13388 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
32 | 31 | adantl 481 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑊 cyclShift 𝑁) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
33 | 21, 30, 32 | 3eqtr4rd 2655 |
. . 3
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (#‘𝑊)))) |
34 | 33 | ex 449 |
. 2
⊢ (𝑊 ≠ ∅ → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (#‘𝑊))))) |
35 | 7, 34 | pm2.61ine 2865 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (#‘𝑊)))) |