Proof of Theorem cshwlen
Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . . 5
⊢ (𝑊 = ∅ → (𝑊 cyclShift 𝑁) = (∅ cyclShift 𝑁)) |
2 | | 0csh0 13539 |
. . . . . 6
⊢ (∅
cyclShift 𝑁) =
∅ |
3 | 2 | a1i 11 |
. . . . 5
⊢ (𝑊 = ∅ → (∅
cyclShift 𝑁) =
∅) |
4 | | eqcom 2629 |
. . . . . 6
⊢ (𝑊 = ∅ ↔ ∅ =
𝑊) |
5 | 4 | biimpi 206 |
. . . . 5
⊢ (𝑊 = ∅ → ∅ =
𝑊) |
6 | 1, 3, 5 | 3eqtrd 2660 |
. . . 4
⊢ (𝑊 = ∅ → (𝑊 cyclShift 𝑁) = 𝑊) |
7 | 6 | fveq2d 6195 |
. . 3
⊢ (𝑊 = ∅ →
(#‘(𝑊 cyclShift 𝑁)) = (#‘𝑊)) |
8 | 7 | a1d 25 |
. 2
⊢ (𝑊 = ∅ → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (#‘(𝑊 cyclShift 𝑁)) = (#‘𝑊))) |
9 | | cshword 13537 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) |
10 | 9 | fveq2d 6195 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (#‘(𝑊 cyclShift 𝑁)) = (#‘((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
11 | 10 | adantr 481 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → (#‘(𝑊 cyclShift 𝑁)) = (#‘((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
12 | | swrdcl 13419 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ∈ Word 𝑉) |
13 | | swrdcl 13419 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉) ∈ Word 𝑉) |
14 | | ccatlen 13360 |
. . . . . . 7
⊢ (((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ∈ Word 𝑉 ∧ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉) ∈ Word 𝑉) → (#‘((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((#‘(𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) + (#‘(𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
15 | 12, 13, 14 | syl2anc 693 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (#‘((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((#‘(𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) + (#‘(𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
16 | 15 | adantr 481 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (#‘((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((#‘(𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) + (#‘(𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
17 | 16 | adantr 481 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → (#‘((𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉) ++ (𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = ((#‘(𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) + (#‘(𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)))) |
18 | | lennncl 13325 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈
ℕ) |
19 | | pm3.21 464 |
. . . . . . . . . . 11
⊢
(((#‘𝑊) ∈
ℕ ∧ 𝑁 ∈
ℤ) → (𝑊 ∈
Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)))) |
20 | 19 | ex 450 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
ℕ → (𝑁 ∈
ℤ → (𝑊 ∈
Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))))) |
21 | 18, 20 | syl 17 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑁 ∈ ℤ → (𝑊 ∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))))) |
22 | 21 | ex 450 |
. . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ → (𝑁 ∈ ℤ → (𝑊 ∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)))))) |
23 | 22 | com24 95 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ∈ Word 𝑉 → (𝑁 ∈ ℤ → (𝑊 ≠ ∅ → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)))))) |
24 | 23 | pm2.43i 52 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (𝑁 ∈ ℤ → (𝑊 ≠ ∅ → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))))) |
25 | 24 | imp31 448 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))) |
26 | | simpl 473 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → 𝑊 ∈ Word 𝑉) |
27 | | pm3.22 465 |
. . . . . . . . . 10
⊢
(((#‘𝑊) ∈
ℕ ∧ 𝑁 ∈
ℤ) → (𝑁 ∈
ℤ ∧ (#‘𝑊)
∈ ℕ)) |
28 | 27 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈
ℕ)) |
29 | | zmodfzp1 12694 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧
(#‘𝑊) ∈ ℕ)
→ (𝑁 mod
(#‘𝑊)) ∈
(0...(#‘𝑊))) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊))) |
31 | | lencl 13324 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
32 | | nn0fz0 12437 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
ℕ0 ↔ (#‘𝑊) ∈ (0...(#‘𝑊))) |
33 | 31, 32 | sylib 208 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈ (0...(#‘𝑊))) |
34 | 33 | adantr 481 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → (#‘𝑊) ∈ (0...(#‘𝑊))) |
35 | | swrdlen 13423 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊)) ∧ (#‘𝑊) ∈ (0...(#‘𝑊))) → (#‘(𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) = ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) |
36 | 26, 30, 34, 35 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → (#‘(𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) = ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) |
37 | | zmodcl 12690 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧
(#‘𝑊) ∈ ℕ)
→ (𝑁 mod
(#‘𝑊)) ∈
ℕ0) |
38 | 37 | ancoms 469 |
. . . . . . . . . 10
⊢
(((#‘𝑊) ∈
ℕ ∧ 𝑁 ∈
ℤ) → (𝑁 mod
(#‘𝑊)) ∈
ℕ0) |
39 | 38 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → (𝑁 mod (#‘𝑊)) ∈
ℕ0) |
40 | | 0elfz 12436 |
. . . . . . . . 9
⊢ ((𝑁 mod (#‘𝑊)) ∈ ℕ0 → 0
∈ (0...(𝑁 mod
(#‘𝑊)))) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → 0 ∈
(0...(𝑁 mod (#‘𝑊)))) |
42 | | swrdlen 13423 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 ∈ (0...(𝑁 mod (#‘𝑊))) ∧ (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊))) → (#‘(𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)) = ((𝑁 mod (#‘𝑊)) − 0)) |
43 | 26, 41, 30, 42 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → (#‘(𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉)) = ((𝑁 mod (#‘𝑊)) − 0)) |
44 | 36, 43 | oveq12d 6668 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → ((#‘(𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) + (#‘(𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + ((𝑁 mod (#‘𝑊)) − 0))) |
45 | 37 | nn0cnd 11353 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧
(#‘𝑊) ∈ ℕ)
→ (𝑁 mod
(#‘𝑊)) ∈
ℂ) |
46 | 45 | ancoms 469 |
. . . . . . . . 9
⊢
(((#‘𝑊) ∈
ℕ ∧ 𝑁 ∈
ℤ) → (𝑁 mod
(#‘𝑊)) ∈
ℂ) |
47 | 46 | adantl 482 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → (𝑁 mod (#‘𝑊)) ∈ ℂ) |
48 | 47 | subid1d 10381 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → ((𝑁 mod (#‘𝑊)) − 0) = (𝑁 mod (#‘𝑊))) |
49 | 48 | oveq2d 6666 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + ((𝑁 mod (#‘𝑊)) − 0)) = (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) |
50 | 31 | nn0cnd 11353 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈ ℂ) |
51 | | npcan 10290 |
. . . . . . 7
⊢
(((#‘𝑊) ∈
ℂ ∧ (𝑁 mod
(#‘𝑊)) ∈
ℂ) → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) = (#‘𝑊)) |
52 | 50, 46, 51 | syl2an 494 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) = (#‘𝑊)) |
53 | 44, 49, 52 | 3eqtrd 2660 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ)) → ((#‘(𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) + (#‘(𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = (#‘𝑊)) |
54 | 25, 53 | syl 17 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → ((#‘(𝑊 substr 〈(𝑁 mod (#‘𝑊)), (#‘𝑊)〉)) + (#‘(𝑊 substr 〈0, (𝑁 mod (#‘𝑊))〉))) = (#‘𝑊)) |
55 | 11, 17, 54 | 3eqtrd 2660 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) ∧ 𝑊 ≠ ∅) → (#‘(𝑊 cyclShift 𝑁)) = (#‘𝑊)) |
56 | 55 | expcom 451 |
. 2
⊢ (𝑊 ≠ ∅ → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (#‘(𝑊 cyclShift 𝑁)) = (#‘𝑊))) |
57 | 8, 56 | pm2.61ine 2877 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (#‘(𝑊 cyclShift 𝑁)) = (#‘𝑊)) |