Step | Hyp | Ref
| Expression |
1 | | 0csh0 14743 |
. . . 4
⊢ (∅
cyclShift 𝑁) =
∅ |
2 | | oveq1 7416 |
. . . 4
⊢ (𝑊 = ∅ → (𝑊 cyclShift 𝑁) = (∅ cyclShift 𝑁)) |
3 | | oveq1 7416 |
. . . . 5
⊢ (𝑊 = ∅ → (𝑊 cyclShift (𝑁 mod (♯‘𝑊))) = (∅ cyclShift (𝑁 mod (♯‘𝑊)))) |
4 | | 0csh0 14743 |
. . . . 5
⊢ (∅
cyclShift (𝑁 mod
(♯‘𝑊))) =
∅ |
5 | 3, 4 | eqtrdi 2789 |
. . . 4
⊢ (𝑊 = ∅ → (𝑊 cyclShift (𝑁 mod (♯‘𝑊))) = ∅) |
6 | 1, 2, 5 | 3eqtr4a 2799 |
. . 3
⊢ (𝑊 = ∅ → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (♯‘𝑊)))) |
7 | 6 | a1d 25 |
. 2
⊢ (𝑊 = ∅ → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (♯‘𝑊))))) |
8 | | lennncl 14484 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈
ℕ) |
9 | 8 | ex 414 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ → (♯‘𝑊) ∈
ℕ)) |
10 | 9 | adantr 482 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 ≠ ∅ → (♯‘𝑊) ∈
ℕ)) |
11 | 10 | impcom 409 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) →
(♯‘𝑊) ∈
ℕ) |
12 | | simprr 772 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℤ) |
13 | | zre 12562 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
14 | | nnrp 12985 |
. . . . . . . . 9
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ∈
ℝ+) |
15 | | modabs2 13870 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧
(♯‘𝑊) ∈
ℝ+) → ((𝑁 mod (♯‘𝑊)) mod (♯‘𝑊)) = (𝑁 mod (♯‘𝑊))) |
16 | 13, 14, 15 | syl2anr 598 |
. . . . . . . 8
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → ((𝑁
mod (♯‘𝑊)) mod
(♯‘𝑊)) = (𝑁 mod (♯‘𝑊))) |
17 | 16 | opeq1d 4880 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → ⟨((𝑁 mod (♯‘𝑊)) mod (♯‘𝑊)), (♯‘𝑊)⟩ = ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) |
18 | 17 | oveq2d 7425 |
. . . . . 6
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → (𝑊
substr ⟨((𝑁 mod
(♯‘𝑊)) mod
(♯‘𝑊)),
(♯‘𝑊)⟩) =
(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) |
19 | 16 | oveq2d 7425 |
. . . . . 6
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → (𝑊
prefix ((𝑁 mod
(♯‘𝑊)) mod
(♯‘𝑊))) =
(𝑊 prefix (𝑁 mod (♯‘𝑊)))) |
20 | 18, 19 | oveq12d 7427 |
. . . . 5
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → ((𝑊
substr ⟨((𝑁 mod
(♯‘𝑊)) mod
(♯‘𝑊)),
(♯‘𝑊)⟩) ++
(𝑊 prefix ((𝑁 mod (♯‘𝑊)) mod (♯‘𝑊)))) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
21 | 11, 12, 20 | syl2anc 585 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → ((𝑊 substr ⟨((𝑁 mod (♯‘𝑊)) mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix ((𝑁 mod (♯‘𝑊)) mod (♯‘𝑊)))) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
22 | | simprl 770 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → 𝑊 ∈ Word 𝑉) |
23 | 12, 11 | zmodcld 13857 |
. . . . . 6
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑁 mod (♯‘𝑊)) ∈
ℕ0) |
24 | 23 | nn0zd 12584 |
. . . . 5
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑁 mod (♯‘𝑊)) ∈ ℤ) |
25 | | cshword 14741 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ ℤ) → (𝑊 cyclShift (𝑁 mod (♯‘𝑊))) = ((𝑊 substr ⟨((𝑁 mod (♯‘𝑊)) mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix ((𝑁 mod (♯‘𝑊)) mod (♯‘𝑊))))) |
26 | 22, 24, 25 | syl2anc 585 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑊 cyclShift (𝑁 mod (♯‘𝑊))) = ((𝑊 substr ⟨((𝑁 mod (♯‘𝑊)) mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix ((𝑁 mod (♯‘𝑊)) mod (♯‘𝑊))))) |
27 | | cshword 14741 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
28 | 27 | adantl 483 |
. . . 4
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
29 | 21, 26, 28 | 3eqtr4rd 2784 |
. . 3
⊢ ((𝑊 ≠ ∅ ∧ (𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ)) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (♯‘𝑊)))) |
30 | 29 | ex 414 |
. 2
⊢ (𝑊 ≠ ∅ → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (♯‘𝑊))))) |
31 | 7, 30 | pm2.61ine 3026 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (♯‘𝑊)))) |