Proof of Theorem repswcshw
Step | Hyp | Ref
| Expression |
1 | | 0csh0 13390 |
. . . . 5
⊢ (∅
cyclShift 𝐼) =
∅ |
2 | | repsw0 13375 |
. . . . . 6
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 0) = ∅) |
3 | 2 | oveq1d 6564 |
. . . . 5
⊢ (𝑆 ∈ 𝑉 → ((𝑆 repeatS 0) cyclShift 𝐼) = (∅ cyclShift 𝐼)) |
4 | 1, 3, 2 | 3eqtr4a 2670 |
. . . 4
⊢ (𝑆 ∈ 𝑉 → ((𝑆 repeatS 0) cyclShift 𝐼) = (𝑆 repeatS 0)) |
5 | 4 | 3ad2ant1 1075 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 0) cyclShift 𝐼) = (𝑆 repeatS 0)) |
6 | | oveq2 6557 |
. . . . 5
⊢ (𝑁 = 0 → (𝑆 repeatS 𝑁) = (𝑆 repeatS 0)) |
7 | 6 | oveq1d 6564 |
. . . 4
⊢ (𝑁 = 0 → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = ((𝑆 repeatS 0) cyclShift 𝐼)) |
8 | 7, 6 | eqeq12d 2625 |
. . 3
⊢ (𝑁 = 0 → (((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁) ↔ ((𝑆 repeatS 0) cyclShift 𝐼) = (𝑆 repeatS 0))) |
9 | 5, 8 | syl5ibr 235 |
. 2
⊢ (𝑁 = 0 → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁))) |
10 | | idd 24 |
. . . 4
⊢ (¬
𝑁 = 0 → (𝑆 ∈ 𝑉 → 𝑆 ∈ 𝑉)) |
11 | | df-ne 2782 |
. . . . 5
⊢ (𝑁 ≠ 0 ↔ ¬ 𝑁 = 0) |
12 | | elnnne0 11183 |
. . . . . 6
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0
∧ 𝑁 ≠
0)) |
13 | 12 | simplbi2com 655 |
. . . . 5
⊢ (𝑁 ≠ 0 → (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ)) |
14 | 11, 13 | sylbir 224 |
. . . 4
⊢ (¬
𝑁 = 0 → (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ)) |
15 | | idd 24 |
. . . 4
⊢ (¬
𝑁 = 0 → (𝐼 ∈ ℤ → 𝐼 ∈
ℤ)) |
16 | 10, 14, 15 | 3anim123d 1398 |
. . 3
⊢ (¬
𝑁 = 0 → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → (𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ))) |
17 | | nnnn0 11176 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
18 | 17 | anim2i 591 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑆 ∈ 𝑉 ∧ 𝑁 ∈
ℕ0)) |
19 | | repsw 13373 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑆 repeatS 𝑁) ∈ Word 𝑉) |
21 | | cshword 13388 |
. . . . 5
⊢ (((𝑆 repeatS 𝑁) ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (((𝑆 repeatS 𝑁) substr 〈(𝐼 mod (#‘(𝑆 repeatS 𝑁))), (#‘(𝑆 repeatS 𝑁))〉) ++ ((𝑆 repeatS 𝑁) substr 〈0, (𝐼 mod (#‘(𝑆 repeatS 𝑁)))〉))) |
22 | 20, 21 | stoic3 1692 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (((𝑆 repeatS 𝑁) substr 〈(𝐼 mod (#‘(𝑆 repeatS 𝑁))), (#‘(𝑆 repeatS 𝑁))〉) ++ ((𝑆 repeatS 𝑁) substr 〈0, (𝐼 mod (#‘(𝑆 repeatS 𝑁)))〉))) |
23 | | repswlen 13374 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(#‘(𝑆 repeatS 𝑁)) = 𝑁) |
24 | 18, 23 | syl 17 |
. . . . . . . . 9
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (#‘(𝑆 repeatS 𝑁)) = 𝑁) |
25 | 24 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝐼 mod (#‘(𝑆 repeatS 𝑁))) = (𝐼 mod 𝑁)) |
26 | 25, 24 | opeq12d 4348 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 〈(𝐼 mod (#‘(𝑆 repeatS 𝑁))), (#‘(𝑆 repeatS 𝑁))〉 = 〈(𝐼 mod 𝑁), 𝑁〉) |
27 | 26 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑆 repeatS 𝑁) substr 〈(𝐼 mod (#‘(𝑆 repeatS 𝑁))), (#‘(𝑆 repeatS 𝑁))〉) = ((𝑆 repeatS 𝑁) substr 〈(𝐼 mod 𝑁), 𝑁〉)) |
28 | 25 | opeq2d 4347 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 〈0, (𝐼 mod (#‘(𝑆 repeatS 𝑁)))〉 = 〈0, (𝐼 mod 𝑁)〉) |
29 | 28 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑆 repeatS 𝑁) substr 〈0, (𝐼 mod (#‘(𝑆 repeatS 𝑁)))〉) = ((𝑆 repeatS 𝑁) substr 〈0, (𝐼 mod 𝑁)〉)) |
30 | 27, 29 | oveq12d 6567 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (((𝑆 repeatS 𝑁) substr 〈(𝐼 mod (#‘(𝑆 repeatS 𝑁))), (#‘(𝑆 repeatS 𝑁))〉) ++ ((𝑆 repeatS 𝑁) substr 〈0, (𝐼 mod (#‘(𝑆 repeatS 𝑁)))〉)) = (((𝑆 repeatS 𝑁) substr 〈(𝐼 mod 𝑁), 𝑁〉) ++ ((𝑆 repeatS 𝑁) substr 〈0, (𝐼 mod 𝑁)〉))) |
31 | 30 | 3adant3 1074 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (((𝑆 repeatS 𝑁) substr 〈(𝐼 mod (#‘(𝑆 repeatS 𝑁))), (#‘(𝑆 repeatS 𝑁))〉) ++ ((𝑆 repeatS 𝑁) substr 〈0, (𝐼 mod (#‘(𝑆 repeatS 𝑁)))〉)) = (((𝑆 repeatS 𝑁) substr 〈(𝐼 mod 𝑁), 𝑁〉) ++ ((𝑆 repeatS 𝑁) substr 〈0, (𝐼 mod 𝑁)〉))) |
32 | 18 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝑆 ∈ 𝑉 ∧ 𝑁 ∈
ℕ0)) |
33 | | zmodcl 12552 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐼 mod 𝑁) ∈
ℕ0) |
34 | 33 | ancoms 468 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ∈
ℕ0) |
35 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → 𝑁 ∈
ℕ0) |
36 | 34, 35 | jca 553 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝐼 mod 𝑁) ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
37 | 36 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝐼 mod 𝑁) ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
38 | | nnre 10904 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
39 | 38 | leidd 10473 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ 𝑁) |
40 | 39 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → 𝑁 ≤ 𝑁) |
41 | | repswswrd 13382 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ ((𝐼 mod 𝑁) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝑁 ≤ 𝑁) → ((𝑆 repeatS 𝑁) substr 〈(𝐼 mod 𝑁), 𝑁〉) = (𝑆 repeatS (𝑁 − (𝐼 mod 𝑁)))) |
42 | 32, 37, 40, 41 | syl3anc 1318 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) substr 〈(𝐼 mod 𝑁), 𝑁〉) = (𝑆 repeatS (𝑁 − (𝐼 mod 𝑁)))) |
43 | | 0nn0 11184 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
44 | 34, 43 | jctil 558 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (0
∈ ℕ0 ∧ (𝐼 mod 𝑁) ∈
ℕ0)) |
45 | 44 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (0 ∈
ℕ0 ∧ (𝐼 mod 𝑁) ∈
ℕ0)) |
46 | | zre 11258 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℤ → 𝐼 ∈
ℝ) |
47 | | nnrp 11718 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
48 | | modcl 12534 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (𝐼 mod 𝑁) ∈
ℝ) |
49 | 46, 47, 48 | syl2anr 494 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℝ) |
50 | 38 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → 𝑁 ∈
ℝ) |
51 | | modlt 12541 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (𝐼 mod 𝑁) < 𝑁) |
52 | 46, 47, 51 | syl2anr 494 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) < 𝑁) |
53 | 49, 50, 52 | ltled 10064 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ≤ 𝑁) |
54 | 53 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ≤ 𝑁) |
55 | | repswswrd 13382 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (0 ∈
ℕ0 ∧ (𝐼 mod 𝑁) ∈ ℕ0) ∧ (𝐼 mod 𝑁) ≤ 𝑁) → ((𝑆 repeatS 𝑁) substr 〈0, (𝐼 mod 𝑁)〉) = (𝑆 repeatS ((𝐼 mod 𝑁) − 0))) |
56 | 32, 45, 54, 55 | syl3anc 1318 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) substr 〈0, (𝐼 mod 𝑁)〉) = (𝑆 repeatS ((𝐼 mod 𝑁) − 0))) |
57 | 42, 56 | oveq12d 6567 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (((𝑆 repeatS 𝑁) substr 〈(𝐼 mod 𝑁), 𝑁〉) ++ ((𝑆 repeatS 𝑁) substr 〈0, (𝐼 mod 𝑁)〉)) = ((𝑆 repeatS (𝑁 − (𝐼 mod 𝑁))) ++ (𝑆 repeatS ((𝐼 mod 𝑁) − 0)))) |
58 | | simp1 1054 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → 𝑆 ∈ 𝑉) |
59 | 33 | nn0red 11229 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐼 mod 𝑁) ∈ ℝ) |
60 | 59 | ancoms 468 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ∈ ℝ) |
61 | 60, 50, 52 | ltled 10064 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ≤ 𝑁) |
62 | 61 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ≤ 𝑁) |
63 | 34 | 3adant1 1072 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝐼 mod 𝑁) ∈
ℕ0) |
64 | 17 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → 𝑁 ∈
ℕ0) |
65 | | nn0sub 11220 |
. . . . . . . 8
⊢ (((𝐼 mod 𝑁) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ ((𝐼 mod 𝑁) ≤ 𝑁 ↔ (𝑁 − (𝐼 mod 𝑁)) ∈
ℕ0)) |
66 | 63, 64, 65 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝐼 mod 𝑁) ≤ 𝑁 ↔ (𝑁 − (𝐼 mod 𝑁)) ∈
ℕ0)) |
67 | 62, 66 | mpbid 221 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝑁 − (𝐼 mod 𝑁)) ∈
ℕ0) |
68 | 33 | nn0ge0d 11231 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 ≤
(𝐼 mod 𝑁)) |
69 | 68 | ancoms 468 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → 0 ≤
(𝐼 mod 𝑁)) |
70 | 69 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → 0 ≤ (𝐼 mod 𝑁)) |
71 | 63, 43 | jctil 558 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (0 ∈
ℕ0 ∧ (𝐼 mod 𝑁) ∈
ℕ0)) |
72 | | nn0sub 11220 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ (𝐼 mod 𝑁) ∈ ℕ0) → (0 ≤
(𝐼 mod 𝑁) ↔ ((𝐼 mod 𝑁) − 0) ∈
ℕ0)) |
73 | 71, 72 | syl 17 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (0 ≤ (𝐼 mod 𝑁) ↔ ((𝐼 mod 𝑁) − 0) ∈
ℕ0)) |
74 | 70, 73 | mpbid 221 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝐼 mod 𝑁) − 0) ∈
ℕ0) |
75 | | repswccat 13383 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 − (𝐼 mod 𝑁)) ∈ ℕ0 ∧ ((𝐼 mod 𝑁) − 0) ∈ ℕ0)
→ ((𝑆 repeatS (𝑁 − (𝐼 mod 𝑁))) ++ (𝑆 repeatS ((𝐼 mod 𝑁) − 0))) = (𝑆 repeatS ((𝑁 − (𝐼 mod 𝑁)) + ((𝐼 mod 𝑁) − 0)))) |
76 | 58, 67, 74, 75 | syl3anc 1318 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS (𝑁 − (𝐼 mod 𝑁))) ++ (𝑆 repeatS ((𝐼 mod 𝑁) − 0))) = (𝑆 repeatS ((𝑁 − (𝐼 mod 𝑁)) + ((𝐼 mod 𝑁) − 0)))) |
77 | | nncn 10905 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
78 | 77 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) |
79 | 33 | nn0cnd 11230 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐼 mod 𝑁) ∈ ℂ) |
80 | | 0cnd 9912 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 0 ∈
ℂ) |
81 | 78, 79, 80 | npncand 10295 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 − (𝐼 mod 𝑁)) + ((𝐼 mod 𝑁) − 0)) = (𝑁 − 0)) |
82 | 77 | subid1d 10260 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑁 − 0) = 𝑁) |
83 | 82 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑁 − 0) = 𝑁) |
84 | 81, 83 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑁 − (𝐼 mod 𝑁)) + ((𝐼 mod 𝑁) − 0)) = 𝑁) |
85 | 84 | ancoms 468 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑁 − (𝐼 mod 𝑁)) + ((𝐼 mod 𝑁) − 0)) = 𝑁) |
86 | 85 | 3adant1 1072 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑁 − (𝐼 mod 𝑁)) + ((𝐼 mod 𝑁) − 0)) = 𝑁) |
87 | 86 | oveq2d 6565 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (𝑆 repeatS ((𝑁 − (𝐼 mod 𝑁)) + ((𝐼 mod 𝑁) − 0))) = (𝑆 repeatS 𝑁)) |
88 | 57, 76, 87 | 3eqtrd 2648 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → (((𝑆 repeatS 𝑁) substr 〈(𝐼 mod 𝑁), 𝑁〉) ++ ((𝑆 repeatS 𝑁) substr 〈0, (𝐼 mod 𝑁)〉)) = (𝑆 repeatS 𝑁)) |
89 | 22, 31, 88 | 3eqtrd 2648 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁)) |
90 | 16, 89 | syl6 34 |
. 2
⊢ (¬
𝑁 = 0 → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁))) |
91 | 9, 90 | pm2.61i 175 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁)) |