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 14785

Description: The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 13-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.) (Proof shortened by AV, 12-Oct-2022.)

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

**Proof of Theorem cshwidxmod**
Step	Hyp	Ref	Expression
1		elfzo0 13705	. . . 4 ⊢ (𝐼 ∈ (0..^(♯‘𝑊)) ↔ (𝐼 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊)))
2		nnne0 12276	. . . . . 6 ⊢ ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ≠ 0)
3		eqneqall 2941	. . . . . 6 ⊢ ((♯‘𝑊) = 0 → ((♯‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
4	2, 3	syl5com 31	. . . . 5 ⊢ ((♯‘𝑊) ∈ ℕ → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
5	4	3ad2ant2 1131	. . . 4 ⊢ ((𝐼 ∈ ℕ₀ ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊)) → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
6	1, 5	sylbi 216	. . 3 ⊢ (𝐼 ∈ (0..^(♯‘𝑊)) → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
7	6	3ad2ant3 1132	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
8		lencl 14515	. . . . 5 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℕ₀)
9		elnnne0 12516	. . . . . . . 8 ⊢ ((♯‘𝑊) ∈ ℕ ↔ ((♯‘𝑊) ∈ ℕ₀ ∧ (♯‘𝑊) ≠ 0))
10		simprl 769	. . . . . . . . . . . . 13 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → 𝑁 ∈ ℤ)
11		cshword 14773	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))))
12	10, 11	sylan2 591	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))))
13	12	fveq1d 6896	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼))
14		swrdcl 14627	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉)
15	14	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉)
16		pfxcl 14659	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉)
17	16	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉)
18		simpl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → 𝑊 ∈ Word 𝑉)
19		simpl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → 𝑁 ∈ ℤ)
20	19	anim2i 615	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))
21	20	adantl 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))
22	21	ancomd 460	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ))
23		zmodfzp1 13892	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)))
24	22, 23	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)))
25		nn0fz0 13631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝑊) ∈ ℕ₀ ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊)))
26	8, 25	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
27	26	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
28		swrdlen 14629	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))
29	18, 24, 27, 28	syl3anc 1368	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))
30	20	ancomd 460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ))
31	30, 23	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)))
32		pfxlen 14665	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))) = (𝑁 mod (♯‘𝑊)))
33	31, 32	sylan2 591	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))) = (𝑁 mod (♯‘𝑊)))
34	29, 33	oveq12d 7435	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊))))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))))
35	29, 34	oveq12d 7435	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))..^((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))
36	35	eleq2d 2811	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝐼 ∈ ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))..^((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))) ↔ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))))))
37	36	biimparc 478	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → 𝐼 ∈ ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))..^((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊)))))))
38		ccatval2 14560	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉 ∧ (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉 ∧ 𝐼 ∈ ((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))..^((♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) + (♯‘(𝑊 prefix (𝑁 mod (♯‘𝑊))))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)))))
39	15, 17, 37, 38	syl2an23an 1420	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)))))
40	26	ad2antrl 726	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
41	18, 24, 40, 28	syl2an23an 1420	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))
42	41	oveq2d 7433	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))) = (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))
43	42	fveq2d 6898	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)))) = ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
44		elfzo2 13667	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ↔ (𝐼 ∈ (ℤ_≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∧ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))
45		eluz2 12858	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐼 ∈ (ℤ_≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ↔ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼))
46		simpl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → 𝐼 ∈ ℤ)
47		nnz 12609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ∈ ℤ)
48	47	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (♯‘𝑊) ∈ ℤ)
49		zmodcl 13888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ ℕ₀)
50	49	nn0zd 12614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ ℤ)
51	48, 50	zsubcld 12701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ)
52	51	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ)
53	46, 52	zsubcld 12701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ)
54	53	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ)
55		zre 12592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ ℝ)
56		nnre 12249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ∈ ℝ)
57	56	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (♯‘𝑊) ∈ ℝ)
58	49	nn0red 12563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ ℝ)
59	57, 58	resubcld 11672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℝ)
60		subge0 11757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐼 ∈ ℝ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℝ) → (0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ↔ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼))
61	55, 59, 60	syl2an 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ↔ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼))
62	61	exbiri 809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐼 ∈ ℤ → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼 → 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))))
63	62	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐼 ∈ ℤ → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼 → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))))
64	63	imp31 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))
65		elnn0uz 12897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℕ₀ ↔ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ_≥‘0))
66		elnn0z 12601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℕ₀ ↔ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ ∧ 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
67	65, 66	bitr3i 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ_≥‘0) ↔ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ ℤ ∧ 0 ≤ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
68	54, 64, 67	sylanbrc 581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ_≥‘0))
69	68	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ_≥‘0))
70	50	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝑁 mod (♯‘𝑊)) ∈ ℤ)
71	55	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → 𝐼 ∈ ℝ)
72	59	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℝ)
73	58	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝑁 mod (♯‘𝑊)) ∈ ℝ)
74	71, 72, 73	ltsubadd2d 11842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)) ↔ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))
75	74	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)) ↔ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))))
76	75	exbiri 809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)))))
77	76	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)))))
78	77	imp31 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊)))
79		elfzo2 13667	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))) ↔ ((𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (ℤ_≥‘0) ∧ (𝑁 mod (♯‘𝑊)) ∈ ℤ ∧ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) < (𝑁 mod (♯‘𝑊))))
80	69, 70, 78, 79	syl3anbrc 1340	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ)) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))
81	80	exp31 418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
82	81	3adant1 1127	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) ≤ 𝐼) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
83	45, 82	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐼 ∈ (ℤ_≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) → (𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
84	83	imp 405	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐼 ∈ (ℤ_≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
85	84	3adant2 1128	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 ∈ (ℤ_≥‘((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∧ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) ∈ ℤ ∧ 𝐼 < (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
86	44, 85	sylbi 216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
87	86	expdcom 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℤ → ((♯‘𝑊) ∈ ℕ → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
88	87	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ∈ ℕ → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))))
89	88	impcom 406	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
90	89	adantl 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))))
91	90	impcom 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊))))
92		pfxfv 14664	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) ∈ (0..^(𝑁 mod (♯‘𝑊)))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
93	18, 24, 91, 92	syl2an23an 1420	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
94		elfzoelz 13664	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐼 ∈ (0..^(♯‘𝑊)) → 𝐼 ∈ ℤ)
95	94	zcnd 12697	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ (0..^(♯‘𝑊)) → 𝐼 ∈ ℂ)
96	95	ad2antll 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → 𝐼 ∈ ℂ)
97		nncn 12250	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ∈ ℂ)
98	97	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (♯‘𝑊) ∈ ℂ)
99	30, 49	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ ℕ₀)
100	99	nn0cnd 12564	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ ℂ)
101	96, 98, 100	subsub3d 11631	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) = ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)))
102	101	ad2antll 727	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) = ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)))
103	30	ad2antll 727	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ))
104	97	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (♯‘𝑊) ∈ ℂ)
105	49	nn0cnd 12564	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝑁 mod (♯‘𝑊)) ∈ ℂ)
106	104, 105	npcand 11605	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊))
107	106	ex 411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℤ → ((♯‘𝑊) ∈ ℕ → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)))
108	107	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ∈ ℕ → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊)))
109	108	impcom 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊))
110	109	adantl 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊))) = (♯‘𝑊))
111	110	oveq2d 7433	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) = (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)))
112	111	eleq2d 2811	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ↔ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))))
113	112	biimpac 477	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)))
114		modaddmodup 13931	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)) = ((𝐼 + 𝑁) mod (♯‘𝑊))))
115	103, 113, 114	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝐼 + (𝑁 mod (♯‘𝑊))) − (♯‘𝑊)) = ((𝐼 + 𝑁) mod (♯‘𝑊)))
116	102, 115	eqtrd 2765	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) = ((𝐼 + 𝑁) mod (♯‘𝑊)))
117	116	fveq2d 6898	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (𝑊‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
118	93, 117	eqtrd 2765	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → ((𝑊 prefix (𝑁 mod (♯‘𝑊)))‘(𝐼 − ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
119	39, 43, 118	3eqtrd 2769	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
120	119	ex 411	. . . . . . . . . . . 12 ⊢ (𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) → ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
121	112	notbid 317	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(((♯‘𝑊) − (𝑁 mod (♯‘𝑊))) + (𝑁 mod (♯‘𝑊)))) ↔ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))))
122	14	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉)
123	16	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉)
124	49	ancoms 457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑁 mod (♯‘𝑊)) ∈ ℕ₀)
125	124	nn0zd 12614	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((♯‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑁 mod (♯‘𝑊)) ∈ ℤ)
126	125	adantrr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) ∈ ℤ)
127		zre 12592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
128	127	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → 𝑁 ∈ ℝ)
129		nnrp 13017	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝑊) ∈ ℕ → (♯‘𝑊) ∈ ℝ⁺)
130		modlt 13877	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ⁺) → (𝑁 mod (♯‘𝑊)) < (♯‘𝑊))
131	128, 129, 130	syl2anr 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑁 mod (♯‘𝑊)) < (♯‘𝑊))
132		simprrr 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → 𝐼 ∈ (0..^(♯‘𝑊)))
133		fzonfzoufzol 13767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 mod (♯‘𝑊)) ∈ ℤ ∧ (𝑁 mod (♯‘𝑊)) < (♯‘𝑊) ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
134	126, 131, 132, 133	syl2an23an 1420	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))))
135	134	imp 405	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))
136		simpll 765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → 𝑊 ∈ Word 𝑉)
137	24	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)))
138	26	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (♯‘𝑊) ∈ (0...(♯‘𝑊)))
139	136, 137, 138, 28	syl3anc 1368	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)) = ((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))
140	139	oveq2d 7433	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (0..^(♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))) = (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))))
141	135, 140	eleqtrrd 2828	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → 𝐼 ∈ (0..^(♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩))))
142		ccatval1 14559	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ∈ Word 𝑉 ∧ (𝑊 prefix (𝑁 mod (♯‘𝑊))) ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘(𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)‘𝐼))
143	122, 123, 141, 142	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)‘𝐼))
144		swrdfv 14630	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (♯‘𝑊)) ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈ (0...(♯‘𝑊))) ∧ 𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊))))) → ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)‘𝐼) = (𝑊‘(𝐼 + (𝑁 mod (♯‘𝑊)))))
145	136, 137, 138, 135, 144	syl31anc 1370	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩)‘𝐼) = (𝑊‘(𝐼 + (𝑁 mod (♯‘𝑊)))))
146	30	ad2antlr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ))
147		modaddmodlo 13932	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → (𝐼 ∈ (0..^((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))) → (𝐼 + (𝑁 mod (♯‘𝑊))) = ((𝐼 + 𝑁) mod (♯‘𝑊))))
148	146, 135, 147	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝐼 + (𝑁 mod (♯‘𝑊))) = ((𝐼 + 𝑁) mod (♯‘𝑊)))
149	148	fveq2d 6898	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (𝑊‘(𝐼 + (𝑁 mod (♯‘𝑊)))) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
150	143, 145, 149	3eqtrd 2769	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) ∧ ¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
151	150	ex 411	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (¬ 𝐼 ∈ (((♯‘𝑊) − (𝑁 mod (♯‘𝑊)))..^(♯‘𝑊)) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
152	121, 151	sylbid 239	. . . . . . . . . . . . 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 182	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
155	13, 154	eqtrd 2765	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
156	155	exp32 419	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) ∈ ℕ → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
157	156	com12 32	. . . . . . . 8 ⊢ ((♯‘𝑊) ∈ ℕ → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
158	9, 157	sylbir 234	. . . . . . 7 ⊢ (((♯‘𝑊) ∈ ℕ₀ ∧ (♯‘𝑊) ≠ 0) → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))))
159	158	ex 411	. . . . . 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 1113	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊)))))
164	7, 163	pm2.61dne 3018	1 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ≠ wne 2930 ⟨cop 4635 class class class wbr 5148 ‘cfv 6547 (class class class)co 7417 ℂcc 11136 ℝcr 11137 0cc0 11138 + caddc 11141 < clt 11278 ≤ cle 11279 − cmin 11474 ℕcn 12242 ℕ₀cn0 12502 ℤcz 12588 ℤ_≥cuz 12852 ℝ⁺crp 13006 ...cfz 13516 ..^cfzo 13659 mod cmo 13866 ♯chash 14321 Word cword 14496 ++ cconcat 14552 substr csubstr 14622 prefix cpfx 14652 cyclShift ccsh 14770

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5364 ax-pr 5428 ax-un 7739 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215 ax-pre-sup 11216

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3965 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-int 4950 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6305 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6499 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-riota 7373 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7870 df-1st 7992 df-2nd 7993 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-er 8723 df-en 8963 df-dom 8964 df-sdom 8965 df-fin 8966 df-sup 9465 df-inf 9466 df-card 9962 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11476 df-neg 11477 df-div 11902 df-nn 12243 df-2 12305 df-n0 12503 df-z 12589 df-uz 12853 df-rp 13007 df-fz 13517 df-fzo 13660 df-fl 13789 df-mod 13867 df-hash 14322 df-word 14497 df-concat 14553 df-substr 14623 df-pfx 14653 df-csh 14771

This theorem is referenced by: cshwidxmodr 14786 cshwidx0mod 14787 cshwidxm1 14789 cshwidxm 14790 cshwidxn 14791 cshf1 14792 2cshw 14795 cshweqrep 14803 cshimadifsn 14812 cshimadifsn0 14813 cshco 14819 crctcshwlkn0lem4 29680 crctcshwlkn0lem5 29681 crctcshwlkn0lem6 29682 clwwisshclwwslem 29880 eucrctshift 30109 cycpmfv1 32891 cycpmfv2 32892

W3C validator