MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cshwidxmod Structured version   Visualization version   GIF version

Theorem cshwidxmod 14785
Description: The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 13-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.) (Proof shortened by AV, 12-Oct-2022.)
Assertion
Ref Expression
cshwidxmod ((𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))

Proof of Theorem cshwidxmod
StepHypRef Expression
1 elfzo0 13705 . . . 4 (𝐼 ∈ (0..^(♯‘𝑊)) ↔ (𝐼 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊)))
2 nnne0 12276 . . . . . 6 ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ≠ 0)
3 eqneqall 2948 . . . . . 6 ((♯‘𝑊) = 0 → ((♯‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
42, 3syl5com 31 . . . . 5 ((♯‘𝑊) ∈ ℕ → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
543ad2ant2 1132 . . . 4 ((𝐼 ∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊)) → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
61, 5sylbi 216 . . 3 (𝐼 ∈ (0..^(♯‘𝑊)) → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
763ad2ant3 1133 . 2 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
8 lencl 14515 . . . . 5 (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℕ0)
9 elnnne0 12516 . . . . . . . 8 ((♯‘𝑊) ∈ ℕ ↔ ((♯‘𝑊) ∈ ℕ0 ∧ (♯‘𝑊) ≠ 0))
10 simprl 770 . . . . . . . . . . . . 13 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → 𝑁 ∈ ℤ)
11 cshword 14773 . . . . . . . . . . . . 13 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))))
1210, 11sylan2 592 . . . . . . . . . . . 12 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))))
1312fveq1d 6899 . . . . . . . . . . 11 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼))
14 swrdcl 14627 . . . . . . . . . . . . . . . 16 (𝑊 ∈ Word 𝑉 → (𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉)
1514adantr 480 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉)
16 pfxcl 14659 . . . . . . . . . . . . . . . 16 (𝑊 ∈ Word 𝑉 → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉)
1716adantr 480 . . . . . . . . . . . . . . 15 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉)
18 simpl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → 𝑊 ∈ Word 𝑉)
19 simpl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → 𝑁 ∈ ℤ)
2019anim2i 616 . . . . . . . . . . . . . . . . . . . . . 22 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))
2120adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))
2221ancomd 461 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ))
23 zmodfzp1 13892 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)))
2422, 23syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)))
25 nn0fz0 13631 . . . . . . . . . . . . . . . . . . . . 21 ((♯‘𝑊) ∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊)))
268, 25sylib 217 . . . . . . . . . . . . . . . . . . . 20 (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
2726adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
28 swrdlen 14629 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))
2918, 24, 27, 28syl3anc 1369 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))
3020ancomd 461 . . . . . . . . . . . . . . . . . . . . 21 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ))
3130, 23syl 17 . . . . . . . . . . . . . . . . . . . 20 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)))
32 pfxlen 14665 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))) = (𝑁 mod (♯‘𝑊)))
3331, 32sylan2 592 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))) = (𝑁 mod (♯‘𝑊)))
3429, 33oveq12d 7438 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊))))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))))
3529, 34oveq12d 7438 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))..^((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))
3635eleq2d 2815 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝐼 ∈ ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))..^((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) ↔ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))))))
3736biimparc 479 . . . . . . . . . . . . . . 15 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → 𝐼 ∈ ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))..^((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))))
38 ccatval2 14560 . . . . . . . . . . . . . . 15 (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉 ∧ (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉𝐼 ∈ ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))..^((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊))))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)))))
3915, 17, 37, 38syl2an23an 1421 . . . . . . . . . . . . . 14 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)))))
4026ad2antrl 727 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
4118, 24, 40, 28syl2an23an 1421 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))
4241oveq2d 7436 . . . . . . . . . . . . . . 15 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))) = (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))
4342fveq2d 6901 . . . . . . . . . . . . . 14 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)))) = ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
44 elfzo2 13667 . . . . . . . . . . . . . . . . . . . . . 22 (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ↔ (𝐼 ∈ (ℤ‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∧ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))
45 eluz2 12858 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐼 ∈ (ℤ‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ↔ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼))
46 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → 𝐼 ∈ ℤ)
47 nnz 12609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ∈ ℤ)
4847adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (♯‘𝑊) ∈ ℤ)
49 zmodcl 13888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ ℕ0)
5049nn0zd 12614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ ℤ)
5148, 50zsubcld 12701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ)
5251adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ)
5346, 52zsubcld 12701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ)
5453adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ)
55 zre 12592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐼 ∈ ℤ → 𝐼 ∈ ℝ)
56 nnre 12249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ∈ ℝ)
5756adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (♯‘𝑊) ∈ ℝ)
5849nn0red 12563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ ℝ)
5957, 58resubcld 11672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℝ)
60 subge0 11757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐼 ∈ ℝ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℝ) → (0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ↔ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼))
6155, 59, 60syl2an 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ↔ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼))
6261exbiri 810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐼 ∈ ℤ → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼 → 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))))
6362com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝐼 ∈ ℤ → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼 → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))))
6463imp31 417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))
65 elnn0uz 12897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℕ0 ↔ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ‘0))
66 elnn0z 12601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℕ0 ↔ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ ∧ 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
6765, 66bitr3i 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ‘0) ↔ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ ∧ 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
6854, 64, 67sylanbrc 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ‘0))
6968adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ‘0))
7050adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝑁 mod (♯‘𝑊)) ∈ ℤ)
7155adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → 𝐼 ∈ ℝ)
7259adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℝ)
7358adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝑁 mod (♯‘𝑊)) ∈ ℝ)
7471, 72, 73ltsubadd2d 11842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)) ↔ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))
7574adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)) ↔ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))
7675exbiri 810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)))))
7776com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)))))
7877imp31 417 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)))
79 elfzo2 13667 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))) ↔ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ‘0) ∧ (𝑁 mod (♯‘𝑊)) ∈ ℤ ∧ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊))))
8069, 70, 78, 79syl3anbrc 1341 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))
8180exp31 419 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
82813adant1 1128 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
8345, 82sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐼 ∈ (ℤ‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
8483imp 406 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐼 ∈ (ℤ‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
85843adant2 1129 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐼 ∈ (ℤ‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∧ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
8644, 85sylbi 216 . . . . . . . . . . . . . . . . . . . . 21 (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
8786expdcom 414 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℤ → ((♯‘𝑊) ∈ ℕ → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
8887adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ∈ ℕ → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
8988impcom 407 . . . . . . . . . . . . . . . . . 18 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
9089adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
9190impcom 407 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))
92 pfxfv 14664 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
9318, 24, 91, 92syl2an23an 1421 . . . . . . . . . . . . . . 15 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
94 elfzoelz 13664 . . . . . . . . . . . . . . . . . . . . 21 (𝐼 ∈ (0..^(♯‘𝑊)) → 𝐼 ∈ ℤ)
9594zcnd 12697 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ (0..^(♯‘𝑊)) → 𝐼 ∈ ℂ)
9695ad2antll 728 . . . . . . . . . . . . . . . . . . 19 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → 𝐼 ∈ ℂ)
97 nncn 12250 . . . . . . . . . . . . . . . . . . . 20 ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ∈ ℂ)
9897adantr 480 . . . . . . . . . . . . . . . . . . 19 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (♯‘𝑊) ∈ ℂ)
9930, 49syl 17 . . . . . . . . . . . . . . . . . . . 20 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ ℕ0)
10099nn0cnd 12564 . . . . . . . . . . . . . . . . . . 19 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ ℂ)
10196, 98, 100subsub3d 11631 . . . . . . . . . . . . . . . . . 18 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) = ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)))
102101ad2antll 728 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) = ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)))
10330ad2antll 728 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ))
10497adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (♯‘𝑊) ∈ ℂ)
10549nn0cnd 12564 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ ℂ)
106104, 105npcand 11605 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊))
107106ex 412 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℤ → ((♯‘𝑊) ∈ ℕ → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)))
108107adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ∈ ℕ → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)))
109108impcom 407 . . . . . . . . . . . . . . . . . . . . . 22 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊))
110109adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊))
111110oveq2d 7436 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)))
112111eleq2d 2815 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ↔ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))))
113112biimpac 478 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)))
114 modaddmodup 13931 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)) = ((𝐼 + 𝑁) mod (♯‘𝑊))))
115103, 113, 114sylc 65 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)) = ((𝐼 + 𝑁) mod (♯‘𝑊)))
116102, 115eqtrd 2768 . . . . . . . . . . . . . . . 16 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) = ((𝐼 + 𝑁) mod (♯‘𝑊)))
117116fveq2d 6901 . . . . . . . . . . . . . . 15 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝑊‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
11893, 117eqtrd 2768 . . . . . . . . . . . . . 14 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
11939, 43, 1183eqtrd 2772 . . . . . . . . . . . . 13 ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
120119ex 412 . . . . . . . . . . . 12 (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
121112notbid 318 . . . . . . . . . . . . . 14 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ↔ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))))
12214ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉)
12316ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉)
12449ancoms 458 . . . . . . . . . . . . . . . . . . . . . 22 (((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑁 mod (♯‘𝑊)) ∈ ℕ0)
125124nn0zd 12614 . . . . . . . . . . . . . . . . . . . . 21 (((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑁 mod (♯‘𝑊)) ∈ ℤ)
126125adantrr 716 . . . . . . . . . . . . . . . . . . . 20 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ ℤ)
127 zre 12592 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
128127adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → 𝑁 ∈ ℝ)
129 nnrp 13017 . . . . . . . . . . . . . . . . . . . . 21 ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ∈ ℝ+)
130 modlt 13877 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ+) → (𝑁 mod (♯‘𝑊)) < (♯‘𝑊))
131128, 129, 130syl2anr 596 . . . . . . . . . . . . . . . . . . . 20 (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) < (♯‘𝑊))
132 simprrr 781 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → 𝐼 ∈ (0..^(♯‘𝑊)))
133 fzonfzoufzol 13767 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 mod (♯‘𝑊)) ∈ ℤ ∧ (𝑁 mod (♯‘𝑊)) < (♯‘𝑊) ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
134126, 131, 132, 133syl2an23an 1421 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
135134imp 406 . . . . . . . . . . . . . . . . . 18 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))
136 simpll 766 . . . . . . . . . . . . . . . . . . . 20 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → 𝑊 ∈ Word 𝑉)
13724adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)))
13826ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
139136, 137, 138, 28syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))
140139oveq2d 7436 . . . . . . . . . . . . . . . . . 18 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (0..^(♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))) = (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))
141135, 140eleqtrrd 2832 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → 𝐼 ∈ (0..^(♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))))
142 ccatval1 14559 . . . . . . . . . . . . . . . . 17 (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉 ∧ (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉𝐼 ∈ (0..^(♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)‘𝐼))
143122, 123, 141, 142syl3anc 1369 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)‘𝐼))
144 swrdfv 14630 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈ (0...(♯‘𝑊))) ∧ 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) → ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)‘𝐼) = (𝑊‘(𝐼 + (𝑁 mod (♯‘𝑊)))))
145136, 137, 138, 135, 144syl31anc 1371 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)‘𝐼) = (𝑊‘(𝐼 + (𝑁 mod (♯‘𝑊)))))
14630ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ))
147 modaddmodlo 13932 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) → (𝐼 + (𝑁 mod (♯‘𝑊))) = ((𝐼 + 𝑁) mod (♯‘𝑊))))
148146, 135, 147sylc 65 . . . . . . . . . . . . . . . . 17 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝐼 + (𝑁 mod (♯‘𝑊))) = ((𝐼 + 𝑁) mod (♯‘𝑊)))
149148fveq2d 6901 . . . . . . . . . . . . . . . 16 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑊‘(𝐼 + (𝑁 mod (♯‘𝑊)))) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
150143, 145, 1493eqtrd 2772 . . . . . . . . . . . . . . 15 (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
151150ex 412 . . . . . . . . . . . . . 14 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
152121, 151sylbid 239 . . . . . . . . . . . . 13 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
153152com12 32 . . . . . . . . . . . 12 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
154120, 153pm2.61i 182 . . . . . . . . . . 11 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
15513, 154eqtrd 2768 . . . . . . . . . 10 ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
156155exp32 420 . . . . . . . . 9 (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) ∈ ℕ → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
157156com12 32 . . . . . . . 8 ((♯‘𝑊) ∈ ℕ → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
1589, 157sylbir 234 . . . . . . 7 (((♯‘𝑊) ∈ ℕ0 ∧ (♯‘𝑊) ≠ 0) → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
159158ex 412 . . . . . 6 ((♯‘𝑊) ∈ ℕ0 → ((♯‘𝑊) ≠ 0 → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))))
160159com23 86 . . . . 5 ((♯‘𝑊) ∈ ℕ0 → (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) ≠ 0 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))))
1618, 160mpcom 38 . . . 4 (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) ≠ 0 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
162161com23 86 . . 3 (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
1631623impib 1114 . 2 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
1647, 163pm2.61dne 3025 1 ((𝑊 ∈ Word 𝑉𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1085   = wceq 1534  wcel 2099  wne 2937  cop 4635   class class class wbr 5148  cfv 6548  (class class class)co 7420  cc 11136  cr 11137  0cc0 11138   + caddc 11141   < clt 11278  cle 11279  cmin 11474  cn 12242  0cn0 12502  cz 12588  cuz 12852  +crp 13006  ...cfz 13516  ..^cfzo 13659   mod cmo 13866  chash 14321  Word cword 14496   ++ cconcat 14552   substr csubstr 14622   prefix cpfx 14652   cyclShift ccsh 14770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215  ax-pre-sup 11216
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7871  df-1st 7993  df-2nd 7994  df-frecs 8286  df-wrecs 8317  df-recs 8391  df-rdg 8430  df-1o 8486  df-er 8724  df-en 8964  df-dom 8965  df-sdom 8966  df-fin 8967  df-sup 9465  df-inf 9466  df-card 9962  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-div 11902  df-nn 12243  df-2 12305  df-n0 12503  df-z 12589  df-uz 12853  df-rp 13007  df-fz 13517  df-fzo 13660  df-fl 13789  df-mod 13867  df-hash 14322  df-word 14497  df-concat 14553  df-substr 14623  df-pfx 14653  df-csh 14771
This theorem is referenced by:  cshwidxmodr  14786  cshwidx0mod  14787  cshwidxm1  14789  cshwidxm  14790  cshwidxn  14791  cshf1  14792  2cshw  14795  cshweqrep  14803  cshimadifsn  14812  cshimadifsn0  14813  cshco  14819  crctcshwlkn0lem4  29623  crctcshwlkn0lem5  29624  crctcshwlkn0lem6  29625  clwwisshclwwslem  29823  eucrctshift  30052  cycpmfv1  32834  cycpmfv2  32835
  Copyright terms: Public domain W3C validator