Step | Hyp | Ref
| Expression |
1 | | 0csh0 14708 |
. . . . 5
⊢ (∅
cyclShift 𝐼) =
∅ |
2 | | repsw0 14692 |
. . . . . 6
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 0) = ∅) |
3 | 2 | oveq1d 7392 |
. . . . 5
⊢ (𝑆 ∈ 𝑉 → ((𝑆 repeatS 0) cyclShift 𝐼) = (∅ cyclShift 𝐼)) |
4 | 1, 3, 2 | 3eqtr4a 2797 |
. . . 4
⊢ (𝑆 ∈ 𝑉 → ((𝑆 repeatS 0) cyclShift 𝐼) = (𝑆 repeatS 0)) |
5 | 4 | 3ad2ant1 1133 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 0) cyclShift 𝐼) = (𝑆 repeatS 0)) |
6 | | oveq2 7385 |
. . . . 5
⊢ (𝑁 = 0 → (𝑆 repeatS 𝑁) = (𝑆 repeatS 0)) |
7 | 6 | oveq1d 7392 |
. . . 4
⊢ (𝑁 = 0 → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = ((𝑆 repeatS 0) cyclShift 𝐼)) |
8 | 7, 6 | eqeq12d 2747 |
. . 3
⊢ (𝑁 = 0 → (((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁) ↔ ((𝑆 repeatS 0) cyclShift 𝐼) = (𝑆 repeatS 0))) |
9 | 5, 8 | imbitrrid 245 |
. 2
⊢ (𝑁 = 0 → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁))) |
10 | | idd 24 |
. . . 4
⊢ (¬
𝑁 = 0 → (𝑆 ∈ 𝑉 → 𝑆 ∈ 𝑉)) |
11 | | df-ne 2940 |
. . . . 5
⊢ (𝑁 ≠ 0 ↔ ¬ 𝑁 = 0) |
12 | | elnnne0 12451 |
. . . . . 6
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0
∧ 𝑁 ≠
0)) |
13 | 12 | simplbi2com 503 |
. . . . 5
⊢ (𝑁 ≠ 0 → (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ)) |
14 | 11, 13 | sylbir 234 |
. . . 4
⊢ (¬
𝑁 = 0 → (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ)) |
15 | | idd 24 |
. . . 4
⊢ (¬
𝑁 = 0 → (𝐼 ∈ ℤ → 𝐼 ∈
ℤ)) |
16 | 10, 14, 15 | 3anim123d 1443 |
. . 3
⊢ (¬
𝑁 = 0 → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → (𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ))) |
17 | | nnnn0 12444 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
18 | 17 | anim2i 617 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑆 ∈ 𝑉 ∧ 𝑁 ∈
ℕ0)) |
19 | | repsw 14690 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
21 | | cshword 14706 |
. . . . 5
⊢ (((𝑆 repeatS 𝑁) ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (((𝑆 repeatS 𝑁) substr ⟨(𝐼 mod (♯‘(𝑆 repeatS 𝑁))), (♯‘(𝑆 repeatS 𝑁))⟩) ++ ((𝑆 repeatS 𝑁) prefix (𝐼 mod (♯‘(𝑆 repeatS 𝑁)))))) |
22 | 20, 21 | stoic3 1778 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (((𝑆 repeatS 𝑁) substr ⟨(𝐼 mod (♯‘(𝑆 repeatS 𝑁))), (♯‘(𝑆 repeatS 𝑁))⟩) ++ ((𝑆 repeatS 𝑁) prefix (𝐼 mod (♯‘(𝑆 repeatS 𝑁)))))) |
23 | | repswlen 14691 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(♯‘(𝑆 repeatS
𝑁)) = 𝑁) |
24 | 18, 23 | syl 17 |
. . . . . . . . 9
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) →
(♯‘(𝑆 repeatS
𝑁)) = 𝑁) |
25 | 24 | oveq2d 7393 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝐼 mod (♯‘(𝑆 repeatS 𝑁))) = (𝐼 mod 𝑁)) |
26 | 25, 24 | opeq12d 4858 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ⟨(𝐼 mod (♯‘(𝑆 repeatS 𝑁))), (♯‘(𝑆 repeatS 𝑁))⟩ = ⟨(𝐼 mod 𝑁), 𝑁⟩) |
27 | 26 | oveq2d 7393 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑆 repeatS 𝑁) substr ⟨(𝐼 mod (♯‘(𝑆 repeatS 𝑁))), (♯‘(𝑆 repeatS 𝑁))⟩) = ((𝑆 repeatS 𝑁) substr ⟨(𝐼 mod 𝑁), 𝑁⟩)) |
28 | 25 | oveq2d 7393 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑆 repeatS 𝑁) prefix (𝐼 mod (♯‘(𝑆 repeatS 𝑁)))) = ((𝑆 repeatS 𝑁) prefix (𝐼 mod 𝑁))) |
29 | 27, 28 | oveq12d 7395 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((𝑆 repeatS 𝑁) substr ⟨(𝐼 mod (♯‘(𝑆 repeatS 𝑁))), (♯‘(𝑆 repeatS 𝑁))⟩) ++ ((𝑆 repeatS 𝑁) prefix (𝐼 mod (♯‘(𝑆 repeatS 𝑁))))) = (((𝑆 repeatS 𝑁) substr ⟨(𝐼 mod 𝑁), 𝑁⟩) ++ ((𝑆 repeatS 𝑁) prefix (𝐼 mod 𝑁)))) |
30 | 29 | 3adant3 1132 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (((𝑆 repeatS 𝑁) substr ⟨(𝐼 mod (♯‘(𝑆 repeatS 𝑁))), (♯‘(𝑆 repeatS 𝑁))⟩) ++ ((𝑆 repeatS 𝑁) prefix (𝐼 mod (♯‘(𝑆 repeatS 𝑁))))) = (((𝑆 repeatS 𝑁) substr ⟨(𝐼 mod 𝑁), 𝑁⟩) ++ ((𝑆 repeatS 𝑁) prefix (𝐼 mod 𝑁)))) |
31 | 18 | 3adant3 1132 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝑆 ∈ 𝑉 ∧ 𝑁 ∈
ℕ0)) |
32 | | zmodcl 13821 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐼 mod 𝑁) ∈
ℕ0) |
33 | 32 | ancoms 459 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ∈
ℕ0) |
34 | 17 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → 𝑁 ∈
ℕ0) |
35 | 33, 34 | jca 512 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝐼 mod 𝑁) ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
36 | 35 | 3adant1 1130 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝐼 mod 𝑁) ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
37 | | nnre 12184 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
38 | 37 | leidd 11745 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ 𝑁) |
39 | 38 | 3ad2ant2 1134 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → 𝑁 ≤ 𝑁) |
40 | | repswswrd 14699 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ ((𝐼 mod 𝑁) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝑁 ≤ 𝑁) → ((𝑆 repeatS 𝑁) substr ⟨(𝐼 mod 𝑁), 𝑁⟩) = (𝑆 repeatS (𝑁 − (𝐼 mod 𝑁)))) |
41 | 31, 36, 39, 40 | syl3anc 1371 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) substr ⟨(𝐼 mod 𝑁), 𝑁⟩) = (𝑆 repeatS (𝑁 − (𝐼 mod 𝑁)))) |
42 | | simp1 1136 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → 𝑆 ∈ 𝑉) |
43 | 17 | 3ad2ant2 1134 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → 𝑁 ∈
ℕ0) |
44 | | zmodfzp1 13825 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐼 mod 𝑁) ∈ (0...𝑁)) |
45 | 44 | ancoms 459 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ∈ (0...𝑁)) |
46 | 45 | 3adant1 1130 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ∈ (0...𝑁)) |
47 | | repswpfx 14700 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ (𝐼 mod 𝑁) ∈ (0...𝑁)) → ((𝑆 repeatS 𝑁) prefix (𝐼 mod 𝑁)) = (𝑆 repeatS (𝐼 mod 𝑁))) |
48 | 42, 43, 46, 47 | syl3anc 1371 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) prefix (𝐼 mod 𝑁)) = (𝑆 repeatS (𝐼 mod 𝑁))) |
49 | 41, 48 | oveq12d 7395 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (((𝑆 repeatS 𝑁) substr ⟨(𝐼 mod 𝑁), 𝑁⟩) ++ ((𝑆 repeatS 𝑁) prefix (𝐼 mod 𝑁))) = ((𝑆 repeatS (𝑁 − (𝐼 mod 𝑁))) ++ (𝑆 repeatS (𝐼 mod 𝑁)))) |
50 | 32 | nn0red 12498 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐼 mod 𝑁) ∈ ℝ) |
51 | 50 | ancoms 459 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℝ) |
52 | 37 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → 𝑁 ∈
ℝ) |
53 | | zre 12527 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℤ → 𝐼 ∈
ℝ) |
54 | | nnrp 12950 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
55 | | modlt 13810 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (𝐼 mod 𝑁) < 𝑁) |
56 | 53, 54, 55 | syl2anr 597 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) < 𝑁) |
57 | 51, 52, 56 | ltled 11327 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ≤ 𝑁) |
58 | 57 | 3adant1 1130 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ≤ 𝑁) |
59 | 33 | 3adant1 1130 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ∈
ℕ0) |
60 | | nn0sub 12487 |
. . . . . . . 8
⊢ (((𝐼 mod 𝑁) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ ((𝐼 mod 𝑁) ≤ 𝑁 ↔ (𝑁 − (𝐼 mod 𝑁)) ∈
ℕ0)) |
61 | 59, 43, 60 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝐼 mod 𝑁) ≤ 𝑁 ↔ (𝑁 − (𝐼 mod 𝑁)) ∈
ℕ0)) |
62 | 58, 61 | mpbid 231 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝑁 − (𝐼 mod 𝑁)) ∈
ℕ0) |
63 | | repswccat 14701 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 − (𝐼 mod 𝑁)) ∈ ℕ0 ∧ (𝐼 mod 𝑁) ∈ ℕ0) → ((𝑆 repeatS (𝑁 − (𝐼 mod 𝑁))) ++ (𝑆 repeatS (𝐼 mod 𝑁))) = (𝑆 repeatS ((𝑁 − (𝐼 mod 𝑁)) + (𝐼 mod 𝑁)))) |
64 | 42, 62, 59, 63 | syl3anc 1371 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS (𝑁 − (𝐼 mod 𝑁))) ++ (𝑆 repeatS (𝐼 mod 𝑁))) = (𝑆 repeatS ((𝑁 − (𝐼 mod 𝑁)) + (𝐼 mod 𝑁)))) |
65 | | nncn 12185 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
66 | 65 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
67 | 32 | nn0cnd 12499 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐼 mod 𝑁) ∈ ℂ) |
68 | 66, 67 | npcand 11540 |
. . . . . . . 8
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 − (𝐼 mod 𝑁)) + (𝐼 mod 𝑁)) = 𝑁) |
69 | 68 | ancoms 459 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑁 − (𝐼 mod 𝑁)) + (𝐼 mod 𝑁)) = 𝑁) |
70 | 69 | 3adant1 1130 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑁 − (𝐼 mod 𝑁)) + (𝐼 mod 𝑁)) = 𝑁) |
71 | 70 | oveq2d 7393 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝑆 repeatS ((𝑁 − (𝐼 mod 𝑁)) + (𝐼 mod 𝑁))) = (𝑆 repeatS 𝑁)) |
72 | 49, 64, 71 | 3eqtrd 2775 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (((𝑆 repeatS 𝑁) substr ⟨(𝐼 mod 𝑁), 𝑁⟩) ++ ((𝑆 repeatS 𝑁) prefix (𝐼 mod 𝑁))) = (𝑆 repeatS 𝑁)) |
73 | 22, 30, 72 | 3eqtrd 2775 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁)) |
74 | 16, 73 | syl6 35 |
. 2
⊢ (¬
𝑁 = 0 → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁))) |
75 | 9, 74 | pm2.61i 182 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁)) |