Proof of Theorem cshwidxmod
Step | Hyp | Ref
| Expression |
1 | | elfzo0 13169 |
. . . 4
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
↔ (𝐼 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊))) |
2 | | nnne0 11750 |
. . . . . 6
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ≠ 0) |
3 | | eqneqall 2945 |
. . . . . 6
⊢
((♯‘𝑊) =
0 → ((♯‘𝑊)
≠ 0 → ((𝑊 cyclShift
𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))) |
4 | 2, 3 | syl5com 31 |
. . . . 5
⊢
((♯‘𝑊)
∈ ℕ → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))) |
5 | 4 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐼 <
(♯‘𝑊)) →
((♯‘𝑊) = 0
→ ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))) |
6 | 1, 5 | sylbi 220 |
. . 3
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ ((♯‘𝑊) =
0 → ((𝑊 cyclShift
𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))) |
7 | 6 | 3ad2ant3 1136 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))) |
8 | | lencl 13974 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
9 | | elnnne0 11990 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℕ ↔ ((♯‘𝑊) ∈ ℕ0 ∧
(♯‘𝑊) ≠
0)) |
10 | | simprl 771 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → 𝑁 ∈ ℤ) |
11 | | cshword 14242 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
12 | 10, 11 | sylan2 596 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊 cyclShift 𝑁) = ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))) |
13 | 12 | fveq1d 6676 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼)) |
14 | | swrdcl 14096 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ∈ Word 𝑉) |
15 | 14 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ∈ Word 𝑉) |
16 | | pfxcl 14128 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉) |
17 | 16 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉) |
18 | | simpl 486 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → 𝑊 ∈ Word 𝑉) |
19 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(0..^(♯‘𝑊)))
→ 𝑁 ∈
ℤ) |
20 | 19 | anim2i 620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈
ℤ)) |
21 | 20 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) →
((♯‘𝑊) ∈
ℕ ∧ 𝑁 ∈
ℤ)) |
22 | 21 | ancomd 465 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ)) |
23 | | zmodfzp1 13354 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝑁 mod
(♯‘𝑊)) ∈
(0...(♯‘𝑊))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊))) |
25 | | nn0fz0 13096 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
26 | 8, 25 | sylib 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
27 | 26 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) →
(♯‘𝑊) ∈
(0...(♯‘𝑊))) |
28 | | swrdlen 14098 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘𝑊)))
→ (♯‘(𝑊
substr 〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)) =
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) |
29 | 18, 24, 27, 28 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) →
(♯‘(𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)) =
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) |
30 | 20 | ancomd 465 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ)) |
31 | 30, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊))) |
32 | | pfxlen 14134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))) = (𝑁 mod (♯‘𝑊))) |
33 | 31, 32 | sylan2 596 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) →
(♯‘(𝑊 prefix
(𝑁 mod (♯‘𝑊)))) = (𝑁 mod (♯‘𝑊))) |
34 | 29, 33 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) →
((♯‘(𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)) +
(♯‘(𝑊 prefix
(𝑁 mod (♯‘𝑊))))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) |
35 | 29, 34 | oveq12d 7188 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) →
((♯‘(𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉))..^((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))))) |
36 | 35 | eleq2d 2818 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝐼 ∈ ((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉))..^((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) ↔ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))) |
37 | 36 | biimparc 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → 𝐼 ∈ ((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉))..^((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊))))))) |
38 | | ccatval2 14021 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ∈ Word 𝑉 ∧ (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉 ∧ 𝐼 ∈ ((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉))..^((♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊))))))) → (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − (♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉))))) |
39 | 15, 17, 37, 38 | syl2an23an 1424 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − (♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉))))) |
40 | 26 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) →
(♯‘𝑊) ∈
(0...(♯‘𝑊))) |
41 | 18, 24, 40, 28 | syl2an23an 1424 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) →
(♯‘(𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)) =
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) |
42 | 41 | oveq2d 7186 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − (♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉))) = (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) |
43 | 42 | fveq2d 6678 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − (♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)))) = ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))) |
44 | | elfzo2 13132 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ↔ (𝐼 ∈
(ℤ≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∧ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))))) |
45 | | eluz2 12330 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐼 ∈
(ℤ≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ↔ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼)) |
46 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ)) → 𝐼 ∈
ℤ) |
47 | | nnz 12085 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ∈ ℤ) |
48 | 47 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (♯‘𝑊) ∈ ℤ) |
49 | | zmodcl 13350 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝑁 mod
(♯‘𝑊)) ∈
ℕ0) |
50 | 49 | nn0zd 12166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝑁 mod
(♯‘𝑊)) ∈
ℤ) |
51 | 48, 50 | zsubcld 12173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ) |
52 | 51 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ)) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ) |
53 | 46, 52 | zsubcld 12173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ)) → (𝐼 −
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) ∈
ℤ) |
54 | 53 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐼 ∈ ℤ ∧
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ) |
55 | | zre 12066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝐼 ∈ ℤ → 𝐼 ∈
ℝ) |
56 | | nnre 11723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ∈ ℝ) |
57 | 56 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (♯‘𝑊) ∈ ℝ) |
58 | 49 | nn0red 12037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝑁 mod
(♯‘𝑊)) ∈
ℝ) |
59 | 57, 58 | resubcld 11146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℝ) |
60 | | subge0 11231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐼 ∈ ℝ ∧
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ∈ ℝ) → (0
≤ (𝐼 −
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) ↔
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼)) |
61 | 55, 59, 60 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ)) → (0 ≤ (𝐼
− ((♯‘𝑊)
− (𝑁 mod
(♯‘𝑊)))) ↔
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼)) |
62 | 61 | exbiri 811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐼 ∈ ℤ → ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼 → 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))) |
63 | 62 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐼 ∈ ℤ →
(((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼 → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → 0 ≤
(𝐼 −
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))))))) |
64 | 63 | imp31 421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐼 ∈ ℤ ∧
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → 0 ≤
(𝐼 −
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))))) |
65 | | elnn0uz 12365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℕ0 ↔
(𝐼 −
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) ∈
(ℤ≥‘0)) |
66 | | elnn0z 12075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℕ0 ↔
((𝐼 −
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) ∈ ℤ ∧ 0 ≤
(𝐼 −
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))))) |
67 | 65, 66 | bitr3i 280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ≥‘0)
↔ ((𝐼 −
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) ∈ ℤ ∧ 0 ≤
(𝐼 −
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))))) |
68 | 54, 64, 67 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐼 ∈ ℤ ∧
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈
(ℤ≥‘0)) |
69 | 68 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐼 ∈ ℤ ∧
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈
(ℤ≥‘0)) |
70 | 50 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐼 ∈ ℤ ∧
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝑁 mod (♯‘𝑊)) ∈
ℤ) |
71 | 55 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ)) → 𝐼 ∈
ℝ) |
72 | 59 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ)) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℝ) |
73 | 58 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ)) → (𝑁 mod
(♯‘𝑊)) ∈
ℝ) |
74 | 71, 72, 73 | ltsubadd2d 11316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ)) → ((𝐼
− ((♯‘𝑊)
− (𝑁 mod
(♯‘𝑊)))) <
(𝑁 mod (♯‘𝑊)) ↔ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))))) |
75 | 74 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐼 ∈ ℤ ∧
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) →
((𝐼 −
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)) ↔ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))))) |
76 | 75 | exbiri 811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐼 ∈ ℤ ∧
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊))))) |
77 | 76 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐼 ∈ ℤ ∧
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊))))) |
78 | 77 | imp31 421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐼 ∈ ℤ ∧
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊))) |
79 | | elfzo2 13132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))) ↔ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ≥‘0)
∧ (𝑁 mod
(♯‘𝑊)) ∈
ℤ ∧ (𝐼 −
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)))) |
80 | 69, 70, 78, 79 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐼 ∈ ℤ ∧
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))) |
81 | 80 | exp31 423 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐼 ∈ ℤ ∧
((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) ≤ 𝐼) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))) |
82 | 81 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((♯‘𝑊)
− (𝑁 mod
(♯‘𝑊))) ∈
ℤ ∧ 𝐼 ∈
ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))) |
83 | 45, 82 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐼 ∈
(ℤ≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))) |
84 | 83 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐼 ∈
(ℤ≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))) |
85 | 84 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈
(ℤ≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∧ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))) |
86 | 44, 85 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))) |
87 | 86 | expdcom 418 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℤ →
((♯‘𝑊) ∈
ℕ → (𝐼 ∈
(((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))) |
88 | 87 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(0..^(♯‘𝑊)))
→ ((♯‘𝑊)
∈ ℕ → (𝐼
∈ (((♯‘𝑊)
− (𝑁 mod
(♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))) |
89 | 88 | impcom 411 |
. . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))) |
90 | 89 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))) |
91 | 90 | impcom 411 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))) |
92 | | pfxfv 14133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))) |
93 | 18, 24, 91, 92 | syl2an23an 1424 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))) |
94 | | elfzoelz 13129 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ 𝐼 ∈
ℤ) |
95 | 94 | zcnd 12169 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ 𝐼 ∈
ℂ) |
96 | 95 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → 𝐼 ∈ ℂ) |
97 | | nncn 11724 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ∈ ℂ) |
98 | 97 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → (♯‘𝑊) ∈ ℂ) |
99 | 30, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈
ℕ0) |
100 | 99 | nn0cnd 12038 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ ℂ) |
101 | 96, 98, 100 | subsub3d 11105 |
. . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) = ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊))) |
102 | 101 | ad2antll 729 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) = ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊))) |
103 | 30 | ad2antll 729 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ)) |
104 | 97 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (♯‘𝑊) ∈ ℂ) |
105 | 49 | nn0cnd 12038 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝑁 mod
(♯‘𝑊)) ∈
ℂ) |
106 | 104, 105 | npcand 11079 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)) |
107 | 106 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℤ →
((♯‘𝑊) ∈
ℕ → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊))) |
108 | 107 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(0..^(♯‘𝑊)))
→ ((♯‘𝑊)
∈ ℕ → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊))) |
109 | 108 | impcom 411 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)) |
110 | 109 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) →
(((♯‘𝑊) −
(𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)) |
111 | 110 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) →
(((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) |
112 | 111 | eleq2d 2818 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ↔ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)))) |
113 | 112 | biimpac 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) |
114 | | modaddmodup 13393 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝐼 ∈
(((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)) = ((𝐼 + 𝑁) mod (♯‘𝑊)))) |
115 | 103, 113,
114 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)) = ((𝐼 + 𝑁) mod (♯‘𝑊))) |
116 | 102, 115 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) = ((𝐼 + 𝑁) mod (♯‘𝑊))) |
117 | 116 | fveq2d 6678 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝑊‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))) |
118 | 93, 117 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))) |
119 | 39, 43, 118 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))) |
120 | 119 | ex 416 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))) |
121 | 112 | notbid 321 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ↔ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)))) |
122 | 14 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ∈ Word 𝑉) |
123 | 16 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉) |
124 | 49 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → (𝑁
mod (♯‘𝑊))
∈ ℕ0) |
125 | 124 | nn0zd 12166 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((♯‘𝑊)
∈ ℕ ∧ 𝑁
∈ ℤ) → (𝑁
mod (♯‘𝑊))
∈ ℤ) |
126 | 125 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ ℤ) |
127 | | zre 12066 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
128 | 127 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(0..^(♯‘𝑊)))
→ 𝑁 ∈
ℝ) |
129 | | nnrp 12483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ∈
ℝ+) |
130 | | modlt 13339 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℝ ∧
(♯‘𝑊) ∈
ℝ+) → (𝑁 mod (♯‘𝑊)) < (♯‘𝑊)) |
131 | 128, 129,
130 | syl2anr 600 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑊)
∈ ℕ ∧ (𝑁
∈ ℤ ∧ 𝐼
∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) < (♯‘𝑊)) |
132 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → 𝐼 ∈ (0..^(♯‘𝑊))) |
133 | | fzonfzoufzol 13231 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 mod (♯‘𝑊)) ∈ ℤ ∧ (𝑁 mod (♯‘𝑊)) < (♯‘𝑊) ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))) |
134 | 126, 131,
132, 133 | syl2an23an 1424 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))) |
135 | 134 | imp 410 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) |
136 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → 𝑊 ∈ Word 𝑉) |
137 | 24 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊))) |
138 | 26 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
139 | 136, 137,
138, 28 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) |
140 | 139 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (0..^(♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉))) = (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) |
141 | 135, 140 | eleqtrrd 2836 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → 𝐼 ∈ (0..^(♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)))) |
142 | | ccatval1 14019 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ∈ Word 𝑉 ∧ (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘(𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)))) → (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)‘𝐼)) |
143 | 122, 123,
141, 142 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)‘𝐼)) |
144 | | swrdfv 14099 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘𝑊)))
∧ 𝐼 ∈
(0..^((♯‘𝑊)
− (𝑁 mod
(♯‘𝑊)))))
→ ((𝑊 substr
〈(𝑁 mod
(♯‘𝑊)),
(♯‘𝑊)〉)‘𝐼) = (𝑊‘(𝐼 + (𝑁 mod (♯‘𝑊))))) |
145 | 136, 137,
138, 135, 144 | syl31anc 1374 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → ((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉)‘𝐼) = (𝑊‘(𝐼 + (𝑁 mod (♯‘𝑊))))) |
146 | 30 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ)) |
147 | | modaddmodlo 13394 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ) → (𝐼 ∈
(0..^((♯‘𝑊)
− (𝑁 mod
(♯‘𝑊)))) →
(𝐼 + (𝑁 mod (♯‘𝑊))) = ((𝐼 + 𝑁) mod (♯‘𝑊)))) |
148 | 146, 135,
147 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝐼 + (𝑁 mod (♯‘𝑊))) = ((𝐼 + 𝑁) mod (♯‘𝑊))) |
149 | 148 | fveq2d 6678 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑊‘(𝐼 + (𝑁 mod (♯‘𝑊)))) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))) |
150 | 143, 145,
149 | 3eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))) |
151 | 150 | ex 416 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))) |
152 | 121, 151 | sylbid 243 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))) |
153 | 152 | com12 32 |
. . . . . . . . . . . 12
⊢ (¬
𝐼 ∈
(((♯‘𝑊) −
(𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))) |
154 | 120, 153 | pm2.61i 185 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((𝑊 substr 〈(𝑁 mod (♯‘𝑊)), (♯‘𝑊)〉) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))) |
155 | 13, 154 | eqtrd 2773 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))) |
156 | 155 | exp32 424 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) ∈ ℕ → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))) |
157 | 156 | com12 32 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℕ → (𝑊
∈ Word 𝑉 →
((𝑁 ∈ ℤ ∧
𝐼 ∈
(0..^(♯‘𝑊)))
→ ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))) |
158 | 9, 157 | sylbir 238 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ (♯‘𝑊) ≠ 0) → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))) |
159 | 158 | ex 416 |
. . . . . 6
⊢
((♯‘𝑊)
∈ ℕ0 → ((♯‘𝑊) ≠ 0 → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))) |
160 | 159 | com23 86 |
. . . . 5
⊢
((♯‘𝑊)
∈ ℕ0 → (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) ≠ 0 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))) |
161 | 8, 160 | mpcom 38 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) ≠ 0 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))) |
162 | 161 | com23 86 |
. . 3
⊢ (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))) |
163 | 162 | 3impib 1117 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))) |
164 | 7, 163 | pm2.61dne 3020 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))) |