cshwidxmod - Metamath Proof Explorer

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

Theorem cshwidxmod 14254

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**
Step	Hyp	Ref	Expression
1		elfzo0 13169	. . . 4 ⊢ (𝐼 ∈ (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 → ((𝑊 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 𝑉 → (♯‘𝑊) ∈ ℕ₀)
9		elnnne0 11990	. . . . . . . 8 ⊢ ((♯‘𝑊) ∈ ℕ ↔ ((♯‘𝑊) ∈ ℕ₀ ∧ (♯‘𝑊) ≠ 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...(♯‘𝑊)))
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 (♯‘𝑊)) ∈ ℕ₀)
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 (♯‘𝑊)))) ∈ ℕ₀ ↔ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ_≥‘0))
66		elnn0z 12075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℕ₀ ↔ ((𝐼 − ((♯‘𝑊) − (𝑁 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 (♯‘𝑊)) ∈ ℕ₀)
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 (♯‘𝑊)) ∈ ℕ₀)
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) → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
159	158	ex 416	. . . . . 6 ⊢ ((♯‘𝑊) ∈ ℕ₀ → ((♯‘𝑊) ≠ 0 → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))))
160	159	com23 86	. . . . 5 ⊢ ((♯‘𝑊) ∈ ℕ₀ → (𝑊 ∈ 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 (♯‘𝑊))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ∈ wcel 2114 ≠ wne 2934 ⟨cop 4522 class class class wbr 5030 ‘cfv 6339 (class class class)co 7170 ℂcc 10613 ℝcr 10614 0cc0 10615 + caddc 10618 < clt 10753 ≤ cle 10754 − cmin 10948 ℕcn 11716 ℕ₀cn0 11976 ℤcz 12062 ℤ_≥cuz 12324 ℝ⁺crp 12472 ...cfz 12981 ..^cfzo 13124 mod cmo 13328 ♯chash 13782 Word cword 13955 ++ cconcat 14011 substr csubstr 14091 prefix cpfx 14121 cyclShift ccsh 14239

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7479 ax-cnex 10671 ax-resscn 10672 ax-1cn 10673 ax-icn 10674 ax-addcl 10675 ax-addrcl 10676 ax-mulcl 10677 ax-mulrcl 10678 ax-mulcom 10679 ax-addass 10680 ax-mulass 10681 ax-distr 10682 ax-i2m1 10683 ax-1ne0 10684 ax-1rid 10685 ax-rnegex 10686 ax-rrecex 10687 ax-cnre 10688 ax-pre-lttri 10689 ax-pre-lttrn 10690 ax-pre-ltadd 10691 ax-pre-mulgt0 10692 ax-pre-sup 10693

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-pss 3862 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-tp 4521 df-op 4523 df-uni 4797 df-int 4837 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5429 df-eprel 5434 df-po 5442 df-so 5443 df-fr 5483 df-we 5485 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-pred 6129 df-ord 6175 df-on 6176 df-lim 6177 df-suc 6178 df-iota 6297 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-riota 7127 df-ov 7173 df-oprab 7174 df-mpo 7175 df-om 7600 df-1st 7714 df-2nd 7715 df-wrecs 7976 df-recs 8037 df-rdg 8075 df-1o 8131 df-er 8320 df-en 8556 df-dom 8557 df-sdom 8558 df-fin 8559 df-sup 8979 df-inf 8980 df-card 9441 df-pnf 10755 df-mnf 10756 df-xr 10757 df-ltxr 10758 df-le 10759 df-sub 10950 df-neg 10951 df-div 11376 df-nn 11717 df-2 11779 df-n0 11977 df-z 12063 df-uz 12325 df-rp 12473 df-fz 12982 df-fzo 13125 df-fl 13253 df-mod 13329 df-hash 13783 df-word 13956 df-concat 14012 df-substr 14092 df-pfx 14122 df-csh 14240

This theorem is referenced by: cshwidxmodr 14255 cshwidx0mod 14256 cshwidxm1 14258 cshwidxm 14259 cshwidxn 14260 cshf1 14261 2cshw 14264 cshweqrep 14272 cshimadifsn 14280 cshimadifsn0 14281 cshco 14287 crctcshwlkn0lem4 27751 crctcshwlkn0lem5 27752 crctcshwlkn0lem6 27753 clwwisshclwwslem 27951 eucrctshift 28180 cycpmfv1 30957 cycpmfv2 30958

W3C validator