| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥 · 𝐿) = (0 · 𝐿)) |
| 2 | 1 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (0 · 𝐿))) |
| 3 | 2 | fvoveq1d 7453 |
. . . . . . 7
⊢ (𝑥 = 0 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (♯‘𝑊))) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (♯‘𝑊)))) |
| 4 | 3 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑥 = 0 → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (♯‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (♯‘𝑊))))) |
| 5 | 4 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 0 → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (♯‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (♯‘𝑊)))))) |
| 6 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 · 𝐿) = (𝑦 · 𝐿)) |
| 7 | 6 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (𝑦 · 𝐿))) |
| 8 | 7 | fvoveq1d 7453 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (♯‘𝑊))) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)))) |
| 9 | 8 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (♯‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊))))) |
| 10 | 9 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (♯‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)))))) |
| 11 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · 𝐿) = ((𝑦 + 1) · 𝐿)) |
| 12 | 11 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + ((𝑦 + 1) · 𝐿))) |
| 13 | 12 | fvoveq1d 7453 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (♯‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊)))) |
| 14 | 13 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (♯‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))))) |
| 15 | 14 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (♯‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊)))))) |
| 16 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑗 → (𝑥 · 𝐿) = (𝑗 · 𝐿)) |
| 17 | 16 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑥 = 𝑗 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (𝑗 · 𝐿))) |
| 18 | 17 | fvoveq1d 7453 |
. . . . . . 7
⊢ (𝑥 = 𝑗 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (♯‘𝑊))) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (♯‘𝑊)))) |
| 19 | 18 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑥 = 𝑗 → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (♯‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (♯‘𝑊))))) |
| 20 | 19 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 𝑗 → ((((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (♯‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (♯‘𝑊)))))) |
| 21 | | zcn 12618 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℂ) |
| 22 | 21 | mul02d 11459 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ ℤ → (0
· 𝐿) =
0) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (0 · 𝐿) = 0) |
| 24 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (0 · 𝐿) = 0) |
| 25 | 24 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝐼 + (0 · 𝐿)) = (𝐼 + 0)) |
| 26 | | elfzoelz 13699 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ 𝐼 ∈
ℤ) |
| 27 | 26 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ 𝐼 ∈
ℂ) |
| 28 | 27 | addridd 11461 |
. . . . . . . . . 10
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ (𝐼 + 0) = 𝐼) |
| 29 | 28 | ad2antll 729 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝐼 + 0) = 𝐼) |
| 30 | 25, 29 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝐼 + (0 · 𝐿)) = 𝐼) |
| 31 | 30 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → ((𝐼 + (0 · 𝐿)) mod (♯‘𝑊)) = (𝐼 mod (♯‘𝑊))) |
| 32 | | zmodidfzoimp 13941 |
. . . . . . . 8
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ (𝐼 mod
(♯‘𝑊)) = 𝐼) |
| 33 | 32 | ad2antll 729 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝐼 mod (♯‘𝑊)) = 𝐼) |
| 34 | 31, 33 | eqtr2d 2778 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → 𝐼 = ((𝐼 + (0 · 𝐿)) mod (♯‘𝑊))) |
| 35 | 34 | fveq2d 6910 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (♯‘𝑊)))) |
| 36 | | fveq1 6905 |
. . . . . . . . . . . . 13
⊢ (𝑊 = (𝑊 cyclShift 𝐿) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)))) |
| 37 | 36 | eqcoms 2745 |
. . . . . . . . . . . 12
⊢ ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)))) |
| 38 | 37 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)))) |
| 39 | 38 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)))) |
| 40 | | simprll 779 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → 𝑊 ∈ Word 𝑉) |
| 41 | | simprlr 780 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → 𝐿 ∈ ℤ) |
| 42 | | elfzo0 13740 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
↔ (𝐼 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐼 < (♯‘𝑊))) |
| 43 | | nn0z 12638 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℤ) |
| 44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) → 𝐼
∈ ℤ) |
| 45 | | nn0z 12638 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℤ) |
| 46 | | zmulcl 12666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑦 · 𝐿) ∈ ℤ) |
| 47 | 45, 46 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝑦 · 𝐿) ∈
ℤ) |
| 48 | 47 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ (𝑦 · 𝐿) ∈
ℤ) |
| 49 | | zaddcl 12657 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐼 ∈ ℤ ∧ (𝑦 · 𝐿) ∈ ℤ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℤ) |
| 50 | 44, 48, 49 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝐿
∈ ℤ ∧ 𝑦
∈ ℕ0)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℤ) |
| 51 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝐿
∈ ℤ ∧ 𝑦
∈ ℕ0)) → (♯‘𝑊) ∈ ℕ) |
| 52 | 50, 51 | jca 511 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ (𝐿
∈ ℤ ∧ 𝑦
∈ ℕ0)) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ)) |
| 53 | 52 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) → ((𝐿
∈ ℤ ∧ 𝑦
∈ ℕ0) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ))) |
| 54 | 53 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐼 <
(♯‘𝑊)) →
((𝐿 ∈ ℤ ∧
𝑦 ∈
ℕ0) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ))) |
| 55 | 42, 54 | sylbi 217 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ ((𝐿 ∈ ℤ
∧ 𝑦 ∈
ℕ0) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ))) |
| 56 | 55 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ))) |
| 57 | 56 | expd 415 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝐿 ∈ ℤ → (𝑦 ∈ ℕ0 → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ)))) |
| 58 | 57 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ ℤ → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑦 ∈ ℕ0 → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ)))) |
| 59 | 58 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑦 ∈ ℕ0 → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ)))) |
| 60 | 59 | imp 406 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑦 ∈ ℕ0 → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ))) |
| 61 | 60 | impcom 407 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (♯‘𝑊) ∈
ℕ)) |
| 62 | | zmodfzo 13934 |
. . . . . . . . . . . 12
⊢ (((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (♯‘𝑊) ∈ ℕ) → ((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) ∈ (0..^(♯‘𝑊))) |
| 63 | 61, 62 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) ∈ (0..^(♯‘𝑊))) |
| 64 | | cshwidxmod 14841 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ ∧ ((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊))) = (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)))) |
| 65 | 40, 41, 63, 64 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊))) = (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)))) |
| 66 | | nn0re 12535 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℝ) |
| 67 | | zre 12617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℝ) |
| 68 | | nn0re 12535 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℝ) |
| 69 | | nnrp 13046 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ∈
ℝ+) |
| 70 | | remulcl 11240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑦 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℝ) |
| 71 | 70 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℝ) |
| 72 | | readdcl 11238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐼 ∈ ℝ ∧ (𝑦 · 𝐿) ∈ ℝ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ) |
| 73 | 71, 72 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐼 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ) |
| 74 | 73 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ) |
| 75 | 74 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((♯‘𝑊)
∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ) |
| 76 | | simprll 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((♯‘𝑊)
∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → 𝐿 ∈ ℝ) |
| 77 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((♯‘𝑊)
∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) →
(♯‘𝑊) ∈
ℝ+) |
| 78 | | modaddmod 13950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐼 + (𝑦 · 𝐿)) ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ+)
→ ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (♯‘𝑊))) |
| 79 | 75, 76, 77, 78 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((♯‘𝑊)
∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (♯‘𝑊))) |
| 80 | | recn 11245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐼 ∈ ℝ → 𝐼 ∈
ℂ) |
| 81 | 80 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → 𝐼 ∈
ℂ) |
| 82 | 70 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑦 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ) |
| 83 | 82 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ) |
| 84 | 83 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ) |
| 85 | | recn 11245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝐿 ∈ ℝ → 𝐿 ∈
ℂ) |
| 86 | 85 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝐿 ∈
ℂ) |
| 87 | 86 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → 𝐿 ∈
ℂ) |
| 88 | 81, 84, 87 | addassd 11283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 · 𝐿) + 𝐿))) |
| 89 | | recn 11245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
| 90 | 89 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℂ) |
| 91 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 1 ∈
ℂ) |
| 92 | 90, 91, 86 | adddird 11286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 + 1) · 𝐿) = ((𝑦 · 𝐿) + (1 · 𝐿))) |
| 93 | 85 | mullidd 11279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝐿 ∈ ℝ → (1
· 𝐿) = 𝐿) |
| 94 | 93 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (1
· 𝐿) = 𝐿) |
| 95 | 94 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 · 𝐿) + (1 · 𝐿)) = ((𝑦 · 𝐿) + 𝐿)) |
| 96 | 92, 95 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 · 𝐿) + 𝐿) = ((𝑦 + 1) · 𝐿)) |
| 97 | 96 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝑦 · 𝐿) + 𝐿) = ((𝑦 + 1) · 𝐿)) |
| 98 | 97 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝐼 + ((𝑦 · 𝐿) + 𝐿)) = (𝐼 + ((𝑦 + 1) · 𝐿))) |
| 99 | 88, 98 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 + 1) · 𝐿))) |
| 100 | 99 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((♯‘𝑊)
∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 + 1) · 𝐿))) |
| 101 | 100 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((♯‘𝑊)
∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))) |
| 102 | 79, 101 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((♯‘𝑊)
∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))) |
| 103 | 102 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝑊)
∈ ℝ+ → (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊)))) |
| 104 | 69, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((♯‘𝑊)
∈ ℕ → (((𝐿
∈ ℝ ∧ 𝑦
∈ ℝ) ∧ 𝐼
∈ ℝ) → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊)))) |
| 105 | 104 | expd 415 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝑊)
∈ ℕ → ((𝐿
∈ ℝ ∧ 𝑦
∈ ℝ) → (𝐼
∈ ℝ → ((((𝐼
+ (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))))) |
| 106 | 105 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
((♯‘𝑊) ∈
ℕ → (𝐼 ∈
ℝ → ((((𝐼 +
(𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))))) |
| 107 | 67, 68, 106 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0)
→ ((♯‘𝑊)
∈ ℕ → (𝐼
∈ ℝ → ((((𝐼
+ (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))))) |
| 108 | 107 | com13 88 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ ℝ →
((♯‘𝑊) ∈
ℕ → ((𝐿 ∈
ℤ ∧ 𝑦 ∈
ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))))) |
| 109 | 66, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐼 ∈ ℕ0
→ ((♯‘𝑊)
∈ ℕ → ((𝐿
∈ ℤ ∧ 𝑦
∈ ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))))) |
| 110 | 109 | imp 406 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) → ((𝐿
∈ ℤ ∧ 𝑦
∈ ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊)))) |
| 111 | 110 | 3adant3 1133 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐼 <
(♯‘𝑊)) →
((𝐿 ∈ ℤ ∧
𝑦 ∈
ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊)))) |
| 112 | 42, 111 | sylbi 217 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ ((𝐿 ∈ ℤ
∧ 𝑦 ∈
ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊)))) |
| 113 | 112 | expd 415 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ (𝐿 ∈ ℤ
→ (𝑦 ∈
ℕ0 → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))))) |
| 114 | 113 | adantld 490 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈
(0..^(♯‘𝑊))
→ ((𝑊 ∈ Word
𝑉 ∧ 𝐿 ∈ ℤ) → (𝑦 ∈ ℕ0 → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))))) |
| 115 | 114 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (𝑦 ∈ ℕ0 → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))))) |
| 116 | 115 | impcom 407 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑦 ∈ ℕ0 → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊)))) |
| 117 | 116 | impcom 407 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))) |
| 118 | 117 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)) + 𝐿) mod (♯‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊)))) |
| 119 | 39, 65, 118 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊)))) |
| 120 | 119 | eqeq2d 2748 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊))) ↔ (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))))) |
| 121 | 120 | biimpd 229 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ0
∧ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))))) → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊))))) |
| 122 | 121 | ex 412 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ (((𝑊 ∈ Word
𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → ((𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊)))))) |
| 123 | 122 | a2d 29 |
. . . . 5
⊢ (𝑦 ∈ ℕ0
→ ((((𝑊 ∈ Word
𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (♯‘𝑊)))) → (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (♯‘𝑊)))))) |
| 124 | 5, 10, 15, 20, 35, 123 | nn0ind 12713 |
. . . 4
⊢ (𝑗 ∈ ℕ0
→ (((𝑊 ∈ Word
𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (♯‘𝑊))))) |
| 125 | 124 | com12 32 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → (𝑗 ∈ ℕ0 → (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (♯‘𝑊))))) |
| 126 | 125 | ralrimiv 3145 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊)))) → ∀𝑗 ∈ ℕ0
(𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (♯‘𝑊)))) |
| 127 | 126 | ex 412 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ∀𝑗 ∈ ℕ0
(𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (♯‘𝑊))))) |