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 13400

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.)

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

**Proof of Theorem cshwidxmod**
Step	Hyp	Ref	Expression
1		elfzo0 12376	. . . 4 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) ↔ (𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)))
2		nnne0 10930	. . . . . 6 ⊢ ((#‘𝑊) ∈ ℕ → (#‘𝑊) ≠ 0)
3		eqneqall 2793	. . . . . . 7 ⊢ ((#‘𝑊) = 0 → ((#‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))
4	3	com12 32	. . . . . 6 ⊢ ((#‘𝑊) ≠ 0 → ((#‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))
5	2, 4	syl 17	. . . . 5 ⊢ ((#‘𝑊) ∈ ℕ → ((#‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))
6	5	3ad2ant2 1076	. . . 4 ⊢ ((𝐼 ∈ ℕ₀ ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)) → ((#‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))
7	1, 6	sylbi 206	. . 3 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → ((#‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))
8	7	3ad2ant3 1077	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((#‘𝑊) = 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))
9		lencl 13179	. . . . 5 ⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈ ℕ₀)
10		elnnne0 11183	. . . . . . . 8 ⊢ ((#‘𝑊) ∈ ℕ ↔ ((#‘𝑊) ∈ ℕ₀ ∧ (#‘𝑊) ≠ 0))
11		simpl 472	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 𝑁 ∈ ℤ)
12	11	adantl 481	. . . . . . . . . . . . 13 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → 𝑁 ∈ ℤ)
13		cshword 13388	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)))
14	12, 13	sylan2 490	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)))
15	14	fveq1d 6105	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))‘𝐼))
16		swrdcl 13271	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ∈ Word 𝑉)
17	16	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ∈ Word 𝑉)
18	17	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ∈ Word 𝑉)
19		swrdcl 13271	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩) ∈ Word 𝑉)
20	19	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩) ∈ Word 𝑉)
21	20	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩) ∈ Word 𝑉)
22		simpl 472	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → 𝑊 ∈ Word 𝑉)
23	11	anim2i 591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))
24	23	ancomd 466	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
25		zmodfzp1 12556	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊)))
26	24, 25	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊)))
27	26	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊)))
28		nn0fz0 12306	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((#‘𝑊) ∈ ℕ₀ ↔ (#‘𝑊) ∈ (0...(#‘𝑊)))
29	9, 28	sylib 207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈ (0...(#‘𝑊)))
30	29	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (#‘𝑊) ∈ (0...(#‘𝑊)))
31		swrdlen 13275	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊)) ∧ (#‘𝑊) ∈ (0...(#‘𝑊))) → (#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)) = ((#‘𝑊) − (𝑁 mod (#‘𝑊))))
32	22, 27, 30, 31	syl3anc 1318	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)) = ((#‘𝑊) − (𝑁 mod (#‘𝑊))))
33	32	eqcomd 2616	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((#‘𝑊) − (𝑁 mod (#‘𝑊))) = (#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)))
34		swrd0len 13274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊))) → (#‘(𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)) = (𝑁 mod (#‘𝑊)))
35	26, 34	sylan2 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (#‘(𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)) = (𝑁 mod (#‘𝑊)))
36	35	eqcomd 2616	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑁 mod (#‘𝑊)) = (#‘(𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)))
37	33, 36	oveq12d 6567	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) = ((#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)) + (#‘(𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))))
38	33, 37	oveq12d 6567	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) = ((#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩))..^((#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)) + (#‘(𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)))))
39	38	eleq2d 2673	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ↔ 𝐼 ∈ ((#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩))..^((#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)) + (#‘(𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))))))
40	39	biimpac 502	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → 𝐼 ∈ ((#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩))..^((#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)) + (#‘(𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)))))
41		ccatval2 13215	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ∈ Word 𝑉 ∧ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩) ∈ Word 𝑉 ∧ 𝐼 ∈ ((#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩))..^((#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)) + (#‘(𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))))) → (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))‘𝐼) = ((𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)‘(𝐼 − (#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)))))
42	18, 21, 40, 41	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))‘𝐼) = ((𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)‘(𝐼 − (#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)))))
43	22	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → 𝑊 ∈ Word 𝑉)
44	27	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊)))
45	30	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (#‘𝑊) ∈ (0...(#‘𝑊)))
46	43, 44, 45, 31	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)) = ((#‘𝑊) − (𝑁 mod (#‘𝑊))))
47	46	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (𝐼 − (#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩))) = (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))))
48	47	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → ((𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)‘(𝐼 − (#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)))) = ((𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)‘(𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊))))))
49		elfzo2 12342	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ↔ (𝐼 ∈ (ℤ_≥‘((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∧ (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) ∈ ℤ ∧ 𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))))
50		eluz2 11569	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐼 ∈ (ℤ_≥‘((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ↔ (((#‘𝑊) − (𝑁 mod (#‘𝑊))) ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼))
51		simpl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → 𝐼 ∈ ℤ)
52		nnz 11276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((#‘𝑊) ∈ ℕ → (#‘𝑊) ∈ ℤ)
53	52	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (#‘𝑊) ∈ ℤ)
54		zmodcl 12552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝑁 mod (#‘𝑊)) ∈ ℕ₀)
55	54	nn0zd 11356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝑁 mod (#‘𝑊)) ∈ ℤ)
56	53, 55	zsubcld 11363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ∈ ℤ)
57	56	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ∈ ℤ)
58	51, 57	zsubcld 11363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ ℤ)
59	58	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ ℤ)
60		zre 11258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ ℝ)
61		nnre 10904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((#‘𝑊) ∈ ℕ → (#‘𝑊) ∈ ℝ)
62	61	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (#‘𝑊) ∈ ℝ)
63	54	nn0red 11229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝑁 mod (#‘𝑊)) ∈ ℝ)
64	62, 63	resubcld 10337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ∈ ℝ)
65		subge0 10420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐼 ∈ ℝ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ∈ ℝ) → (0 ≤ (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ↔ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼))
66	60, 64, 65	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → (0 ≤ (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ↔ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼))
67	66	exbiri 650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝐼 ∈ ℤ → ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼 → 0 ≤ (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))))))
68	67	com23 84	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐼 ∈ ℤ → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼 → ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → 0 ≤ (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))))))
69	68	imp31 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → 0 ≤ (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))))
70		elnn0uz 11601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ ℕ₀ ↔ (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (ℤ_≥‘0))
71		elnn0z 11267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ ℕ₀ ↔ ((𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ ℤ ∧ 0 ≤ (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊))))))
72	70, 71	bitr3i 265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (ℤ_≥‘0) ↔ ((𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ ℤ ∧ 0 ≤ (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊))))))
73	59, 69, 72	sylanbrc 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (ℤ_≥‘0))
74	73	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (ℤ_≥‘0))
75	55	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → (𝑁 mod (#‘𝑊)) ∈ ℤ)
76	60	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → 𝐼 ∈ ℝ)
77	64	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ∈ ℝ)
78	63	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → (𝑁 mod (#‘𝑊)) ∈ ℝ)
79	76, 77, 78	3jca 1235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐼 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → (𝐼 ∈ ℝ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ∈ ℝ ∧ (𝑁 mod (#‘𝑊)) ∈ ℝ))
80	79	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → (𝐼 ∈ ℝ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ∈ ℝ ∧ (𝑁 mod (#‘𝑊)) ∈ ℝ))
81		ltsubadd2 10378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐼 ∈ ℝ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ∈ ℝ ∧ (𝑁 mod (#‘𝑊)) ∈ ℝ) → ((𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) < (𝑁 mod (#‘𝑊)) ↔ 𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))))
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → ((𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) < (𝑁 mod (#‘𝑊)) ↔ 𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))))
83	82	exbiri 650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) → ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) < (𝑁 mod (#‘𝑊)))))
84	83	com23 84	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) → (𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) → ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) < (𝑁 mod (#‘𝑊)))))
85	84	imp31 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) < (𝑁 mod (#‘𝑊)))
86		elfzo2 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊))) ↔ ((𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (ℤ_≥‘0) ∧ (𝑁 mod (#‘𝑊)) ∈ ℤ ∧ (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) < (𝑁 mod (#‘𝑊))))
87	74, 75, 85, 86	syl3anbrc 1239	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) ∧ 𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊))))
88	87	exp31 628	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) → (𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) → ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊))))))
89	88	3adant1 1072	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((#‘𝑊) − (𝑁 mod (#‘𝑊))) ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ ((#‘𝑊) − (𝑁 mod (#‘𝑊))) ≤ 𝐼) → (𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) → ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊))))))
90	50, 89	sylbi 206	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐼 ∈ (ℤ_≥‘((#‘𝑊) − (𝑁 mod (#‘𝑊)))) → (𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) → ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊))))))
91	90	imp 444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐼 ∈ (ℤ_≥‘((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∧ 𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊)))))
92	91	3adant2 1073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐼 ∈ (ℤ_≥‘((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∧ (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) ∈ ℤ ∧ 𝐼 < (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊)))))
93	49, 92	sylbi 206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) → ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊)))))
94	93	com12 32	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊)))))
95	94	ex 449	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℤ → ((#‘𝑊) ∈ ℕ → (𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊))))))
96	95	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((#‘𝑊) ∈ ℕ → (𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊))))))
97	96	impcom 445	. . . . . . . . . . . . . . . . . 18 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊)))))
98	97	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊)))))
99	98	impcom 445	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊))))
100		swrd0fv 13291	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊)) ∧ (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) ∈ (0..^(𝑁 mod (#‘𝑊)))) → ((𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)‘(𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊))))) = (𝑊‘(𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊))))))
101	43, 44, 99, 100	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → ((𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)‘(𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊))))) = (𝑊‘(𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊))))))
102		elfzoelz 12339	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈ ℤ)
103	102	zcnd 11359	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈ ℂ)
104	103	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 𝐼 ∈ ℂ)
105	104	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → 𝐼 ∈ ℂ)
106		nncn 10905	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((#‘𝑊) ∈ ℕ → (#‘𝑊) ∈ ℂ)
107	106	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (#‘𝑊) ∈ ℂ)
108	24, 54	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑁 mod (#‘𝑊)) ∈ ℕ₀)
109	108	nn0cnd 11230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑁 mod (#‘𝑊)) ∈ ℂ)
110	105, 107, 109	3jca 1235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 ∈ ℂ ∧ (#‘𝑊) ∈ ℂ ∧ (𝑁 mod (#‘𝑊)) ∈ ℂ))
111	110	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝐼 ∈ ℂ ∧ (#‘𝑊) ∈ ℂ ∧ (𝑁 mod (#‘𝑊)) ∈ ℂ))
112	111	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (𝐼 ∈ ℂ ∧ (#‘𝑊) ∈ ℂ ∧ (𝑁 mod (#‘𝑊)) ∈ ℂ))
113		subsub3 10192	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ ℂ ∧ (#‘𝑊) ∈ ℂ ∧ (𝑁 mod (#‘𝑊)) ∈ ℂ) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) = ((𝐼 + (𝑁 mod (#‘𝑊))) − (#‘𝑊)))
114	112, 113	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) = ((𝐼 + (𝑁 mod (#‘𝑊))) − (#‘𝑊)))
115	24	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
116	115	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
117	107, 109	jca 553	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → ((#‘𝑊) ∈ ℂ ∧ (𝑁 mod (#‘𝑊)) ∈ ℂ))
118	117	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((#‘𝑊) ∈ ℂ ∧ (𝑁 mod (#‘𝑊)) ∈ ℂ))
119		npcan 10169	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((#‘𝑊) ∈ ℂ ∧ (𝑁 mod (#‘𝑊)) ∈ ℂ) → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) = (#‘𝑊))
120	118, 119	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) = (#‘𝑊))
121	120	oveq2d 6565	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) = (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊)))
122	121	eleq2d 2673	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ↔ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))))
123	122	biimpac 502	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊)))
124		modaddmodup 12595	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊)) → ((𝐼 + (𝑁 mod (#‘𝑊))) − (#‘𝑊)) = ((𝐼 + 𝑁) mod (#‘𝑊))))
125	116, 123, 124	sylc 63	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → ((𝐼 + (𝑁 mod (#‘𝑊))) − (#‘𝑊)) = ((𝐼 + 𝑁) mod (#‘𝑊)))
126	114, 125	eqtrd 2644	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊)))) = ((𝐼 + 𝑁) mod (#‘𝑊)))
127	126	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (𝑊‘(𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊))))) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))
128	101, 127	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → ((𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩)‘(𝐼 − ((#‘𝑊) − (𝑁 mod (#‘𝑊))))) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))
129	42, 48, 128	3eqtrd 2648	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ∧ (𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))))) → (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))
130	129	ex 449	. . . . . . . . . . . 12 ⊢ (𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) → ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))
131	106	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (#‘𝑊) ∈ ℂ)
132	54	nn0cnd 11230	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝑁 mod (#‘𝑊)) ∈ ℂ)
133	131, 132	npcand 10275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) = (#‘𝑊))
134	133	ex 449	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℤ → ((#‘𝑊) ∈ ℕ → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) = (#‘𝑊)))
135	134	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((#‘𝑊) ∈ ℕ → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) = (#‘𝑊)))
136	135	impcom 445	. . . . . . . . . . . . . . . . . 18 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) = (#‘𝑊))
137	136	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊))) = (#‘𝑊))
138	137	oveq2d 6565	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) = (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊)))
139	138	eleq2d 2673	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ↔ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))))
140	139	notbid 307	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) ↔ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))))
141	17	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → (𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ∈ Word 𝑉)
142	20	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩) ∈ Word 𝑉)
143	108	nn0zd 11356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑁 mod (#‘𝑊)) ∈ ℤ)
144	143	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑁 mod (#‘𝑊)) ∈ ℤ)
145		zre 11258	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
146	145	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → 𝑁 ∈ ℝ)
147		nnrp 11718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((#‘𝑊) ∈ ℕ → (#‘𝑊) ∈ ℝ⁺)
148		modlt 12541	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑁 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ⁺) → (𝑁 mod (#‘𝑊)) < (#‘𝑊))
149	146, 147, 148	syl2anr 494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑁 mod (#‘𝑊)) < (#‘𝑊))
150	149	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑁 mod (#‘𝑊)) < (#‘𝑊))
151		simprrr 801	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → 𝐼 ∈ (0..^(#‘𝑊)))
152		fzonfzoufzol 12437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 mod (#‘𝑊)) ∈ ℤ ∧ (𝑁 mod (#‘𝑊)) < (#‘𝑊) ∧ 𝐼 ∈ (0..^(#‘𝑊))) → (¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊)) → 𝐼 ∈ (0..^((#‘𝑊) − (𝑁 mod (#‘𝑊))))))
153	144, 150, 151, 152	syl3anc 1318	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊)) → 𝐼 ∈ (0..^((#‘𝑊) − (𝑁 mod (#‘𝑊))))))
154	153	imp 444	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → 𝐼 ∈ (0..^((#‘𝑊) − (𝑁 mod (#‘𝑊)))))
155	22	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → 𝑊 ∈ Word 𝑉)
156	27	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊)))
157	30	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → (#‘𝑊) ∈ (0...(#‘𝑊)))
158	155, 156, 157, 31	syl3anc 1318	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → (#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)) = ((#‘𝑊) − (𝑁 mod (#‘𝑊))))
159	158	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → (0..^(#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩))) = (0..^((#‘𝑊) − (𝑁 mod (#‘𝑊)))))
160	154, 159	eleqtrrd 2691	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → 𝐼 ∈ (0..^(#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩))))
161		ccatval1 13214	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ∈ Word 𝑉 ∧ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩) ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(#‘(𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)))) → (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))‘𝐼) = ((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)‘𝐼))
162	141, 142, 160, 161	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))‘𝐼) = ((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)‘𝐼))
163	23	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ))
164	163	ancomd 466	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
165	164, 25	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊)))
166	165	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊)))
167		swrdfv 13276	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑁 mod (#‘𝑊)) ∈ (0...(#‘𝑊)) ∧ (#‘𝑊) ∈ (0...(#‘𝑊))) ∧ 𝐼 ∈ (0..^((#‘𝑊) − (𝑁 mod (#‘𝑊))))) → ((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)‘𝐼) = (𝑊‘(𝐼 + (𝑁 mod (#‘𝑊)))))
168	155, 166, 157, 154, 167	syl31anc 1321	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → ((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩)‘𝐼) = (𝑊‘(𝐼 + (𝑁 mod (#‘𝑊)))))
169	115	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → (𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
170	54	ancoms 468	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑁 mod (#‘𝑊)) ∈ ℕ₀)
171	170	nn0zd 11356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((#‘𝑊) ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑁 mod (#‘𝑊)) ∈ ℤ)
172	171	adantrr 749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊)))) → (𝑁 mod (#‘𝑊)) ∈ ℤ)
173	172	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (𝑁 mod (#‘𝑊)) ∈ ℤ)
174	173, 150, 151, 152	syl3anc 1318	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊)) → 𝐼 ∈ (0..^((#‘𝑊) − (𝑁 mod (#‘𝑊))))))
175	174	imp 444	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → 𝐼 ∈ (0..^((#‘𝑊) − (𝑁 mod (#‘𝑊)))))
176		modaddmodlo 12596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → (𝐼 ∈ (0..^((#‘𝑊) − (𝑁 mod (#‘𝑊)))) → (𝐼 + (𝑁 mod (#‘𝑊))) = ((𝐼 + 𝑁) mod (#‘𝑊))))
177	169, 175, 176	sylc 63	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → (𝐼 + (𝑁 mod (#‘𝑊))) = ((𝐼 + 𝑁) mod (#‘𝑊)))
178	177	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → (𝑊‘(𝐼 + (𝑁 mod (#‘𝑊)))) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))
179	162, 168, 178	3eqtrd 2648	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) ∧ ¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊))) → (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))
180	179	ex 449	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(#‘𝑊)) → (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))
181	140, 180	sylbid 229	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) → (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))
182	181	com12 32	. . . . . . . . . . . 12 ⊢ (¬ 𝐼 ∈ (((#‘𝑊) − (𝑁 mod (#‘𝑊)))..^(((#‘𝑊) − (𝑁 mod (#‘𝑊))) + (𝑁 mod (#‘𝑊)))) → ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))
183	130, 182	pm2.61i 175	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → (((𝑊 substr ⟨(𝑁 mod (#‘𝑊)), (#‘𝑊)⟩) ++ (𝑊 substr ⟨0, (𝑁 mod (#‘𝑊))⟩))‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))
184	15, 183	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))
185	184	exp32 629	. . . . . . . . 9 ⊢ (𝑊 ∈ Word 𝑉 → ((#‘𝑊) ∈ ℕ → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))))
186	185	com12 32	. . . . . . . 8 ⊢ ((#‘𝑊) ∈ ℕ → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))))
187	10, 186	sylbir 224	. . . . . . 7 ⊢ (((#‘𝑊) ∈ ℕ₀ ∧ (#‘𝑊) ≠ 0) → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))))
188	187	ex 449	. . . . . 6 ⊢ ((#‘𝑊) ∈ ℕ₀ → ((#‘𝑊) ≠ 0 → (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))))
189	188	com23 84	. . . . 5 ⊢ ((#‘𝑊) ∈ ℕ₀ → (𝑊 ∈ Word 𝑉 → ((#‘𝑊) ≠ 0 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))))
190	9, 189	mpcom 37	. . . 4 ⊢ (𝑊 ∈ Word 𝑉 → ((#‘𝑊) ≠ 0 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))))
191	190	com23 84	. . 3 ⊢ (𝑊 ∈ Word 𝑉 → ((𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((#‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))))
192	191	3impib 1254	. 2 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((#‘𝑊) ≠ 0 → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊)))))
193	8, 192	pm2.61dne 2868	1 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (#‘𝑊))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ⟨cop 4131 class class class wbr 4583 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 0cc0 9815 + caddc 9818 < clt 9953 ≤ cle 9954 − cmin 10145 ℕcn 10897 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ℝ⁺crp 11708 ...cfz 12197 ..^cfzo 12334 mod cmo 12530 #chash 12979 Word cword 13146 ++ cconcat 13148 substr csubstr 13150 cyclShift ccsh 13385

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-inf 8232 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-fz 12198 df-fzo 12335 df-fl 12455 df-mod 12531 df-hash 12980 df-word 13154 df-concat 13156 df-substr 13158 df-csh 13386

This theorem is referenced by: cshwidxmodr 13401 cshwidx0mod 13402 cshwidxm1 13404 cshwidxm 13405 cshwidxn 13406 cshf1 13407 2cshw 13410 cshweqrep 13418 cshimadifsn 13426 cshimadifsn0 13427 cshco 13433 clwwisshclwwlem 26334 crctcsh1wlkn0lem4 41016 crctcsh1wlkn0lem5 41017 crctcsh1wlkn0lem6 41018 clwwisshclwwslem 41234 eucrctshift 41411

W3C validator