Proof of Theorem cshwidxmodr
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfzo0 13740 | . . . . . . 7
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
↔ (𝐼 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊))) | 
| 2 |  | nn0z 12638 | . . . . . . . . . . 11
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℤ) | 
| 3 | 2 | 3ad2ant1 1134 | . . . . . . . . . 10
⊢ ((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐼 <
(♯‘𝑊)) →
𝐼 ∈
ℤ) | 
| 4 |  | zsubcl 12659 | . . . . . . . . . 10
⊢ ((𝐼 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐼 − 𝑁) ∈ ℤ) | 
| 5 | 3, 4 | sylan 580 | . . . . . . . . 9
⊢ (((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐼 <
(♯‘𝑊)) ∧
𝑁 ∈ ℤ) →
(𝐼 − 𝑁) ∈
ℤ) | 
| 6 |  | simpl2 1193 | . . . . . . . . 9
⊢ (((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐼 <
(♯‘𝑊)) ∧
𝑁 ∈ ℤ) →
(♯‘𝑊) ∈
ℕ) | 
| 7 | 5, 6 | jca 511 | . . . . . . . 8
⊢ (((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐼 <
(♯‘𝑊)) ∧
𝑁 ∈ ℤ) →
((𝐼 − 𝑁) ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ)) | 
| 8 | 7 | ex 412 | . . . . . . 7
⊢ ((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐼 <
(♯‘𝑊)) →
(𝑁 ∈ ℤ →
((𝐼 − 𝑁) ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ))) | 
| 9 | 1, 8 | sylbi 217 | . . . . . 6
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ (𝑁 ∈ ℤ
→ ((𝐼 − 𝑁) ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ))) | 
| 10 | 9 | impcom 407 | . . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(0..^(♯‘𝑊)))
→ ((𝐼 − 𝑁) ∈ ℤ ∧
(♯‘𝑊) ∈
ℕ)) | 
| 11 | 10 | 3adant1 1131 | . . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝐼 − 𝑁) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ)) | 
| 12 |  | zmodfzo 13934 | . . . 4
⊢ (((𝐼 − 𝑁) ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → ((𝐼 − 𝑁) mod (♯‘𝑊)) ∈ (0..^(♯‘𝑊))) | 
| 13 | 11, 12 | syl 17 | . . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝐼 − 𝑁) mod (♯‘𝑊)) ∈ (0..^(♯‘𝑊))) | 
| 14 |  | cshwidxmod 14841 | . . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ ((𝐼 − 𝑁) mod (♯‘𝑊)) ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((𝐼 − 𝑁) mod (♯‘𝑊))) = (𝑊‘((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊)))) | 
| 15 | 13, 14 | syld3an3 1411 | . 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((𝐼 − 𝑁) mod (♯‘𝑊))) = (𝑊‘((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊)))) | 
| 16 |  | elfzoelz 13699 | . . . . . . . . . . . . . . 15
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ 𝐼 ∈
ℤ) | 
| 17 | 16 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) → 𝐼 ∈ ℤ) | 
| 18 | 17, 4 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) ∧ 𝑁 ∈ ℤ) → (𝐼 − 𝑁) ∈ ℤ) | 
| 19 | 18 | zred 12722 | . . . . . . . . . . . 12
⊢ ((((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) ∧ 𝑁 ∈ ℤ) → (𝐼 − 𝑁) ∈ ℝ) | 
| 20 |  | zre 12617 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) | 
| 21 | 20 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ) | 
| 22 |  | nnrp 13046 | . . . . . . . . . . . . 13
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ∈
ℝ+) | 
| 23 | 22 | ad3antlr 731 | . . . . . . . . . . . 12
⊢ ((((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) ∧ 𝑁 ∈ ℤ) → (♯‘𝑊) ∈
ℝ+) | 
| 24 |  | modaddmod 13950 | . . . . . . . . . . . 12
⊢ (((𝐼 − 𝑁) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ+)
→ ((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊)) = (((𝐼 − 𝑁) + 𝑁) mod (♯‘𝑊))) | 
| 25 | 19, 21, 23, 24 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) ∧ 𝑁 ∈ ℤ) → ((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊)) = (((𝐼 − 𝑁) + 𝑁) mod (♯‘𝑊))) | 
| 26 |  | nn0cn 12536 | . . . . . . . . . . . . . 14
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℂ) | 
| 27 | 26 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) → 𝐼 ∈ ℂ) | 
| 28 |  | zcn 12618 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) | 
| 29 |  | npcan 11517 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝐼 − 𝑁) + 𝑁) = 𝐼) | 
| 30 | 27, 28, 29 | syl2an 596 | . . . . . . . . . . . 12
⊢ ((((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) ∧ 𝑁 ∈ ℤ) → ((𝐼 − 𝑁) + 𝑁) = 𝐼) | 
| 31 | 30 | oveq1d 7446 | . . . . . . . . . . 11
⊢ ((((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) ∧ 𝑁 ∈ ℤ) → (((𝐼 − 𝑁) + 𝑁) mod (♯‘𝑊)) = (𝐼 mod (♯‘𝑊))) | 
| 32 |  | zmodidfzoimp 13941 | . . . . . . . . . . . 12
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ (𝐼 mod
(♯‘𝑊)) = 𝐼) | 
| 33 | 32 | ad2antlr 727 | . . . . . . . . . . 11
⊢ ((((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) ∧ 𝑁 ∈ ℤ) → (𝐼 mod (♯‘𝑊)) = 𝐼) | 
| 34 | 25, 31, 33 | 3eqtrd 2781 | . . . . . . . . . 10
⊢ ((((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) ∧ 𝑁 ∈ ℤ) → ((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊)) = 𝐼) | 
| 35 | 34 | fveq2d 6910 | . . . . . . . . 9
⊢ ((((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) ∧ 𝑁 ∈ ℤ) → (𝑊‘((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊))) = (𝑊‘𝐼)) | 
| 36 | 35 | ex 412 | . . . . . . . 8
⊢ (((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐼
∈ (0..^(♯‘𝑊))) → (𝑁 ∈ ℤ → (𝑊‘((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊))) = (𝑊‘𝐼))) | 
| 37 | 36 | ex 412 | . . . . . . 7
⊢ ((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) → (𝐼
∈ (0..^(♯‘𝑊)) → (𝑁 ∈ ℤ → (𝑊‘((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊))) = (𝑊‘𝐼)))) | 
| 38 | 37 | 3adant3 1133 | . . . . . 6
⊢ ((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐼 <
(♯‘𝑊)) →
(𝐼 ∈
(0..^(♯‘𝑊))
→ (𝑁 ∈ ℤ
→ (𝑊‘((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊))) = (𝑊‘𝐼)))) | 
| 39 | 1, 38 | sylbi 217 | . . . . 5
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ (𝐼 ∈
(0..^(♯‘𝑊))
→ (𝑁 ∈ ℤ
→ (𝑊‘((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊))) = (𝑊‘𝐼)))) | 
| 40 | 39 | pm2.43i 52 | . . . 4
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ (𝑁 ∈ ℤ
→ (𝑊‘((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊))) = (𝑊‘𝐼))) | 
| 41 | 40 | impcom 407 | . . 3
⊢ ((𝑁 ∈ ℤ ∧ 𝐼 ∈
(0..^(♯‘𝑊)))
→ (𝑊‘((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊))) = (𝑊‘𝐼)) | 
| 42 | 41 | 3adant1 1131 | . 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊‘((((𝐼 − 𝑁) mod (♯‘𝑊)) + 𝑁) mod (♯‘𝑊))) = (𝑊‘𝐼)) | 
| 43 | 15, 42 | eqtrd 2777 | 1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((𝐼 − 𝑁) mod (♯‘𝑊))) = (𝑊‘𝐼)) |