Metamath Proof Explorer

Theorem cshwidxmod

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)

Ref Expression
Assertion cshwidxmod ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 elfzo0 ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) )
2 nnne0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ≠ 0 )
3 eqneqall ⊢ ( ( ♯ ‘ 𝑊 ) = 0 → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
4 2 3 syl5com ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ♯ ‘ 𝑊 ) = 0 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
5 4 3ad2ant2 ⊢ ( ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) = 0 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
6 1 5 sylbi ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) = 0 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
7 6 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ 𝑊 ) = 0 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
8 lencl ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
9 elnnne0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) )
10 simprl ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → 𝑁 ∈ ℤ )
11 cshword ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
12 10 11 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝑊 cyclShift 𝑁 ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
13 12 fveq1d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ‘ 𝐼 ) )
14 swrdcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝑉 )
15 14 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝑉 )
16 pfxcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ Word 𝑉 )
17 16 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ Word 𝑉 )
18 simpl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → 𝑊 ∈ Word 𝑉 )
19 simpl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℤ )
20 19 anim2i ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) )
21 20 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) )
22 21 ancomd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
23 zmodfzp1 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
24 22 23 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
25 nn0fz0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
26 8 25 sylib ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
27 26 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
28 swrdlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
29 18 24 27 28 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
30 20 ancomd ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
31 30 23 syl ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
32 pfxlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) = ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) )
33 31 32 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ♯ ‘ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) = ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) )
34 29 33 oveq12d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) + ( ♯ ‘ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) = ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
35 29 34 oveq12d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) + ( ♯ ‘ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) ) = ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
36 35 eleq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝐼 ∈ ( ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) + ( ♯ ‘ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) ) ↔ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
37 36 biimparc ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → 𝐼 ∈ ( ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ..^ ( ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) + ( ♯ ‘ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
38 ccatval2 ⊢ ( ( ( 𝑊 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 ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ‘ 𝐼 ) = ( ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ‘ ( 𝐼 − ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) )
40 26 ad2antrl ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
41 18 24 40 28 syl2an23an ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
42 41 oveq2d ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( 𝐼 − ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
43 42 fveq2d ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ‘ ( 𝐼 − ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) = ( ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ‘ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
44 elfzo2 ⊢ ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ↔ ( 𝐼 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ ℤ ∧ 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
45 eluz2 ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ↔ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) )
46 simpl ⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → 𝐼 ∈ ℤ )
47 nnz ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℤ )
48 47 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
49 zmodcl ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℕ0 )
50 49 nn0zd ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℤ )
51 48 50 zsubcld ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ ℤ )
52 51 adantl ⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ ℤ )
53 46 52 zsubcld ⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℤ )
54 53 adantlr ⊢ ( ( ( 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℤ )
55 zre ⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ ℝ )
56 nnre ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℝ )
57 56 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ♯ ‘ 𝑊 ) ∈ ℝ )
58 49 nn0red ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℝ )
59 57 58 resubcld ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ ℝ )
60 subge0 ⊢ ( ( 𝐼 ∈ ℝ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ ℝ ) → ( 0 ≤ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ↔ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) )
61 55 59 60 syl2an ⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( 0 ≤ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ↔ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) )
62 61 exbiri ⊢ ( 𝐼 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 → 0 ≤ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
63 62 com23 ⊢ ( 𝐼 ∈ ℤ → ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 → ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → 0 ≤ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
64 63 imp31 ⊢ ( ( ( 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → 0 ≤ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
65 elnn0uz ⊢ ( ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℕ0 ↔ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( ℤ≥ ‘ 0 ) )
66 elnn0z ⊢ ( ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℕ0 ↔ ( ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℤ ∧ 0 ≤ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
67 65 66 bitr3i ⊢ ( ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( ℤ≥ ‘ 0 ) ↔ ( ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ℤ ∧ 0 ≤ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
68 54 64 67 sylanbrc ⊢ ( ( ( 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( ℤ≥ ‘ 0 ) )
69 68 adantlr ⊢ ( ( ( ( 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) ∧ 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( ℤ≥ ‘ 0 ) )
70 50 adantl ⊢ ( ( ( ( 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) ∧ 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℤ )
71 55 adantr ⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → 𝐼 ∈ ℝ )
72 59 adantl ⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ ℝ )
73 58 adantl ⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℝ )
74 71 72 73 ltsubadd2d ⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) < ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ↔ 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
75 74 adantlr ⊢ ( ( ( 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) < ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ↔ 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
76 75 exbiri ⊢ ( ( 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) → ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) < ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
77 76 com23 ⊢ ( ( 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) → ( 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) < ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
78 77 imp31 ⊢ ( ( ( ( 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) ∧ 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) < ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) )
79 elfzo2 ⊢ ( ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ↔ ( ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℤ ∧ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) < ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
80 69 70 78 79 syl3anbrc ⊢ ( ( ( ( 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) ∧ 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
81 80 exp31 ⊢ ( ( 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) → ( 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
82 81 3adant1 ⊢ ( ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ≤ 𝐼 ) → ( 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
83 45 82 sylbi ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
84 83 imp ⊢ ( ( 𝐼 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
85 84 3adant2 ⊢ ( ( 𝐼 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ ℤ ∧ 𝐼 < ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
86 44 85 sylbi ⊢ ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
87 86 expdcom ⊢ ( 𝑁 ∈ ℤ → ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
88 87 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
89 88 impcom ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
90 89 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
91 90 impcom ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
92 pfxfv ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∈ ( 0 ..^ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ‘ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) = ( 𝑊 ‘ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
93 18 24 91 92 syl2an23an ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ‘ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) = ( 𝑊 ‘ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
94 elfzoelz ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ℤ )
95 94 zcnd ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ℂ )
96 95 ad2antll ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → 𝐼 ∈ ℂ )
97 nncn ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℂ )
98 97 adantr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
99 30 49 syl ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℕ0 )
100 99 nn0cnd ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℂ )
101 96 98 100 subsub3d ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) = ( ( 𝐼 + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) − ( ♯ ‘ 𝑊 ) ) )
102 101 ad2antll ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) = ( ( 𝐼 + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) − ( ♯ ‘ 𝑊 ) ) )
103 30 ad2antll ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
104 97 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
105 49 nn0cnd ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℂ )
106 104 105 npcand ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
107 106 ex ⊢ ( 𝑁 ∈ ℤ → ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) ) )
108 107 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) ) )
109 108 impcom ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
110 109 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( ♯ ‘ 𝑊 ) )
111 110 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) = ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) )
112 111 eleq2d ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ↔ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) )
113 112 biimpac ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) )
114 modaddmodup ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝐼 + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) − ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
115 103 113 114 sylc ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( ( 𝐼 + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) − ( ♯ ‘ 𝑊 ) ) = ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
116 102 115 eqtrd ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) = ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
117 116 fveq2d ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( 𝑊 ‘ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
118 93 117 eqtrd ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ‘ ( 𝐼 − ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
119 39 43 118 3eqtrd ⊢ ( ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ) → ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
120 119 ex ⊢ ( 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
121 112 notbid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ↔ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) )
122 14 ad2antrr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝑉 )
123 16 ad2antrr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ Word 𝑉 )
124 49 ancoms ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℕ0 )
125 124 nn0zd ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℤ )
126 125 adantrr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℤ )
127 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
128 127 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℝ )
129 nnrp ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ♯ ‘ 𝑊 ) ∈ ℝ+ )
130 modlt ⊢ ( ( 𝑁 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ+ ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) < ( ♯ ‘ 𝑊 ) )
131 128 129 130 syl2anr ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) < ( ♯ ‘ 𝑊 ) )
132 simprrr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
133 fzonfzoufzol ⊢ ( ( ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ℤ ∧ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) < ( ♯ ‘ 𝑊 ) ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
134 126 131 132 133 syl2an23an ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
135 134 imp ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
136 simpll ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝑉 )
137 24 adantr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
138 26 ad2antrr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
139 136 137 138 28 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) )
140 139 oveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
141 135 140 eleqtrrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
142 ccatval1 ⊢ ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝑉 ∧ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ∈ Word 𝑉 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) → ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ‘ 𝐼 ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ 𝐼 ) )
143 122 123 141 142 syl3anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ‘ 𝐼 ) = ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ 𝐼 ) )
144 swrdfv ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ ( 𝐼 + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
145 136 137 138 135 144 syl31anc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ 𝐼 ) = ( 𝑊 ‘ ( 𝐼 + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) )
146 30 ad2antlr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
147 modaddmodlo ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ) → ( 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝐼 + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
148 146 135 147 sylc ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐼 + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) = ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) )
149 148 fveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( 𝐼 + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
150 143 145 149 3eqtrd ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) ∧ ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
151 150 ex ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
152 121 151 sylbid ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
153 152 com12 ⊢ ( ¬ 𝐼 ∈ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ..^ ( ( ( ♯ ‘ 𝑊 ) − ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) + ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
154 120 153 pm2.61i ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( ( 𝑊 substr ⟨ ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix ( 𝑁 mod ( ♯ ‘ 𝑊 ) ) ) ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
155 13 154 eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )
156 155 exp32 ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
157 156 com12 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
158 9 157 sylbir ⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≠ 0 ) → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
159 158 ex ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( 𝑊 ∈ Word 𝑉 → ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
160 159 com23 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
161 8 160 mpcom ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
162 161 com23 ⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) ) )
163 162 3impib ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ 𝑊 ) ≠ 0 → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) ) )
164 7 163 pm2.61dne ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑁 ) ‘ 𝐼 ) = ( 𝑊 ‘ ( ( 𝐼 + 𝑁 ) mod ( ♯ ‘ 𝑊 ) ) ) )