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 14954

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 13835	. . . 4 ⊢ (𝐼 ∈ (0..^(♯‘𝑊)) ↔ (𝐼 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊)))
2		nnne0 12372	. . . . . 6 ⊢ ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ≠ 0)
3		eqneqall 2966	. . . . . 6 ⊢ ((♯‘𝑊) = 0 → ((♯‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
4	2, 3	syl5com 32	. . . . 5 ⊢ ((♯‘𝑊) ∈ ℕ → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
5	4	3ad2ant2 1152	. . . 4 ⊢ ((𝐼 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊)) → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
6	1, 5	sylbi 220	. . 3 ⊢ (𝐼 ∈ (0..^(♯‘𝑊)) → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
7	6	3ad2ant3 1153	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
8		lencl 14678	. . . . 5 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℕ₀)
9		elnnne0 12620	. . . . . . . 8 ⊢ ((♯‘𝑊) ∈ ℕ ↔ ((♯‘𝑊) ∈ ℕ₀ ∧ (♯‘𝑊) ≠ 0))
10		simprl 783	. . . . . . . . . . . . 13 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → 𝑁 ∈ ℤ)
11		cshword 14942	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))))
12	10, 11	sylan2 605	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))))
13	12	fveq1d 6887	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼))
14		swrdcl 14793	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉)
15	14	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉)
16		pfxcl 14827	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉)
17	16	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉)
18		simpl 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → 𝑊 ∈ Word 𝑉)
19		simpl 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → 𝑁 ∈ ℤ)
20	19	anim2i 629	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))
21	20	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))
22	21	ancomd 467	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ))
23		zmodfzp1 14035	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)))
24	22, 23	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)))
25		nn0fz0 13759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝑊) ∈ ℕ₀ ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊)))
26	8, 25	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
27	26	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
28		swrdlen 14795	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))
29	18, 24, 27, 28	syl3anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))
30	20	ancomd 467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ))
31	30, 23	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)))
32		pfxlen 14833	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))) = (𝑁 mod (♯‘𝑊)))
33	31, 32	sylan2 605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))) = (𝑁 mod (♯‘𝑊)))
34	29, 33	oveq12d 7438	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊))))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))))
35	29, 34	oveq12d 7438	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))..^((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))
36	35	eleq2d 2846	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝐼 ∈ ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))..^((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) ↔ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))))))
37	36	biimparc 485	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → 𝐼 ∈ ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))..^((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))))
38		ccatval2 14723	. . . . . . . . . . . . . . 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 1450	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)))))
40	26	ad2antrl 741	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
41	18, 24, 40, 28	syl2an23an 1450	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))
42	41	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))) = (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))
43	42	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)))) = ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
44		elfzo2 13796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ↔ (𝐼 ∈ (ℤ_≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∧ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))
45		eluz2 12971	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐼 ∈ (ℤ_≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ↔ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼))
46		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → 𝐼 ∈ ℤ)
47		nnz 12714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ∈ ℤ)
48	47	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (♯‘𝑊) ∈ ℤ)
49		zmodcl 14031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ ℕ₀)
50	49	nn0zd 12718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ ℤ)
51	48, 50	zsubcld 12808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ)
52	51	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ)
53	46, 52	zsubcld 12808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ)
54	53	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ)
55		zre 12697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ ℝ)
56		nnre 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ∈ ℝ)
57	56	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (♯‘𝑊) ∈ ℝ)
58	49	nn0red 12668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ ℝ)
59	57, 58	resubcld 11744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℝ)
60		subge0 11829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐼 ∈ ℝ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℝ) → (0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ↔ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼))
61	55, 59, 60	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ↔ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼))
62	61	exbiri 823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐼 ∈ ℤ → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼 → 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))))
63	62	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐼 ∈ ℤ → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼 → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))))
64	63	imp31 423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))
65		elnn0uz 13006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℕ₀ ↔ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ_≥‘0))
66		elnn0z 12706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℕ₀ ↔ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ ∧ 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
67	65, 66	bitr3i 280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ_≥‘0) ↔ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ ∧ 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
68	54, 64, 67	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ_≥‘0))
69	68	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ_≥‘0))
70	50	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝑁 mod (♯‘𝑊)) ∈ ℤ)
71	55	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → 𝐼 ∈ ℝ)
72	59	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℝ)
73	58	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝑁 mod (♯‘𝑊)) ∈ ℝ)
74	71, 72, 73	ltsubadd2d 11914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)) ↔ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))
75	74	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)) ↔ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))
76	75	exbiri 823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)))))
77	76	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)))))
78	77	imp31 423	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)))
79		elfzo2 13796	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))) ↔ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ_≥‘0) ∧ (𝑁 mod (♯‘𝑊)) ∈ ℤ ∧ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊))))
80	69, 70, 78, 79	syl3anbrc 1362	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))
81	80	exp31 425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
82	81	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
83	45, 82	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐼 ∈ (ℤ_≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
84	83	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐼 ∈ (ℤ_≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
85	84	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ (ℤ_≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∧ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
86	44, 85	sylbi 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
87	86	expdcom 420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℤ → ((♯‘𝑊) ∈ ℕ → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
88	87	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ∈ ℕ → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
89	88	impcom 413	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
90	89	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
91	90	impcom 413	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))
92		pfxfv 14832	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
93	18, 24, 91, 92	syl2an23an 1450	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
94		elfzoelz 13793	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐼 ∈ (0..^(♯‘𝑊)) → 𝐼 ∈ ℤ)
95	94	zcnd 12804	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ (0..^(♯‘𝑊)) → 𝐼 ∈ ℂ)
96	95	ad2antll 742	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → 𝐼 ∈ ℂ)
97		nncn 12343	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ∈ ℂ)
98	97	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (♯‘𝑊) ∈ ℂ)
99	30, 49	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ ℕ₀)
100	99	nn0cnd 12669	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ ℂ)
101	96, 98, 100	subsub3d 11699	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) = ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)))
102	101	ad2antll 742	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) = ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)))
103	30	ad2antll 742	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ))
104	97	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (♯‘𝑊) ∈ ℂ)
105	49	nn0cnd 12669	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ ℂ)
106	104, 105	npcand 11673	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊))
107	106	ex 418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℤ → ((♯‘𝑊) ∈ ℕ → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)))
108	107	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ∈ ℕ → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)))
109	108	impcom 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊))
110	109	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊))
111	110	oveq2d 7436	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)))
112	111	eleq2d 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ↔ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))))
113	112	biimpac 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)))
114		modaddmodup 14077	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)) = ((𝐼 + 𝑁) mod (♯‘𝑊))))
115	103, 113, 114	sylc 66	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)) = ((𝐼 + 𝑁) mod (♯‘𝑊)))
116	102, 115	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) = ((𝐼 + 𝑁) mod (♯‘𝑊)))
117	116	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝑊‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
118	93, 117	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
119	39, 43, 118	3eqtrd 2799	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
120	119	ex 418	. . . . . . . . . . . 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 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉)
123	16	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉)
124	49	ancoms 464	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑁 mod (♯‘𝑊)) ∈ ℕ₀)
125	124	nn0zd 12718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑁 mod (♯‘𝑊)) ∈ ℤ)
126	125	adantrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ ℤ)
127		zre 12697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
128	127	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → 𝑁 ∈ ℝ)
129		nnrp 13132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ∈ ℝ⁺)
130		modlt 14020	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ⁺) → (𝑁 mod (♯‘𝑊)) < (♯‘𝑊))
131	128, 129, 130	syl2anr 609	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) < (♯‘𝑊))
132		simprrr 794	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → 𝐼 ∈ (0..^(♯‘𝑊)))
133		fzonfzoufzol 13906	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 mod (♯‘𝑊)) ∈ ℤ ∧ (𝑁 mod (♯‘𝑊)) < (♯‘𝑊) ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
134	126, 131, 132, 133	syl2an23an 1450	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
135	134	imp 412	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))
136		simpll 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → 𝑊 ∈ Word 𝑉)
137	24	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)))
138	26	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
139	136, 137, 138, 28	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))
140	139	oveq2d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (0..^(♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))) = (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))
141	135, 140	eleqtrrd 2863	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → 𝐼 ∈ (0..^(♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))))
142		ccatval1 14722	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉 ∧ (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)‘𝐼))
143	122, 123, 141, 142	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)‘𝐼))
144		swrdfv 14796	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈ (0...(♯‘𝑊))) ∧ 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) → ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)‘𝐼) = (𝑊‘(𝐼 + (𝑁 mod (♯‘𝑊)))))
145	136, 137, 138, 135, 144	syl31anc 1400	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)‘𝐼) = (𝑊‘(𝐼 + (𝑁 mod (♯‘𝑊)))))
146	30	ad2antlr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ))
147		modaddmodlo 14078	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) → (𝐼 + (𝑁 mod (♯‘𝑊))) = ((𝐼 + 𝑁) mod (♯‘𝑊))))
148	146, 135, 147	sylc 66	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝐼 + (𝑁 mod (♯‘𝑊))) = ((𝐼 + 𝑁) mod (♯‘𝑊)))
149	148	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑊‘(𝐼 + (𝑁 mod (♯‘𝑊)))) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
150	143, 145, 149	3eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
151	150	ex 418	. . . . . . . . . . . . . 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 33	. . . . . . . . . . . 12 ⊢ (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
154	120, 153	pm2.61i 184	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
155	13, 154	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
156	155	exp32 426	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) ∈ ℕ → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
157	156	com12 33	. . . . . . . 8 ⊢ ((♯‘𝑊) ∈ ℕ → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
158	9, 157	sylbir 238	. . . . . . 7 ⊢ (((♯‘𝑊) ∈ ℕ₀ ∧ (♯‘𝑊) ≠ 0) → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
159	158	ex 418	. . . . . 6 ⊢ ((♯‘𝑊) ∈ ℕ₀ → ((♯‘𝑊) ≠ 0 → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))))
160	159	com23 87	. . . . 5 ⊢ ((♯‘𝑊) ∈ ℕ₀ → (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) ≠ 0 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))))
161	8, 160	mpcom 39	. . . 4 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) ≠ 0 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
162	161	com23 87	. . 3 ⊢ (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
163	162	3impib 1134	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
164	7, 163	pm2.61dne 3041	1 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ⟨cop 4589 class class class wbr 5102 ‘cfv 6538 (class class class)co 7420 ℂcc 11198 ℝcr 11199 0cc0 11200 + caddc 11203 < clt 11343 ≤ cle 11344 − cmin 11541 ℕcn 12335 ℕ₀cn0 12606 ℤcz 12693 ℤ_≥cuz 12965 ℝ⁺crp 13120 ...cfz 13639 ..^cfzo 13788 mod cmo 14009 ♯chash 14474 Word cword 14658 ++ cconcat 14715 substr csubstr 14788 prefix cpfx 14820 cyclShift ccsh 14939

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-er 8717 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-sup 9434 df-inf 9435 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-n0 12607 df-z 12694 df-uz 12966 df-rp 13121 df-fz 13640 df-fzo 13789 df-fl 13932 df-mod 14010 df-hash 14475 df-word 14659 df-concat 14716 df-substr 14789 df-pfx 14821 df-csh 14940

This theorem is used by: cshwidxmodr 14955 cshwidx0mod 14956 cshwidxm1 14958 cshwidxm 14959 cshwidxn 14960 cshf1 14961 2cshw 14964 cshweqrep 14972 cshimadifsn 14980 cshimadifsn0 14981 cshco 14987 crctcshwlkn0lem4 30402 crctcshwlkn0lem5 30403 crctcshwlkn0lem6 30404 clwwisshclwwslem 30605 eucrctshift 30844 cycpmfv1 33716 cycpmfv2 33717

W3C validator