Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) → (#‘𝑊) ∈
ℙ) |
2 | 1 | adantr 480 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (#‘𝑊) ∈ ℙ) |
3 | | simp1 1054 |
. . . . . . . . 9
⊢ ((𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝐿 ∈ ℤ) |
4 | 3 | adantl 481 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → 𝐿 ∈ ℤ) |
5 | | simpr2 1061 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 mod (#‘𝑊)) ≠ 0) |
6 | 2, 4, 5 | 3jca 1235 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → ((#‘𝑊) ∈ ℙ ∧ 𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0)) |
7 | 6 | adantr 480 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((#‘𝑊) ∈ ℙ ∧ 𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0)) |
8 | | simpr 476 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → 𝑖 ∈ (0..^(#‘𝑊))) |
9 | | modprmn0modprm0 15350 |
. . . . . 6
⊢
(((#‘𝑊) ∈
ℙ ∧ 𝐿 ∈
ℤ ∧ (𝐿 mod
(#‘𝑊)) ≠ 0) →
(𝑖 ∈
(0..^(#‘𝑊)) →
∃𝑗 ∈
(0..^(#‘𝑊))((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0)) |
10 | 7, 8, 9 | sylc 63 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ∃𝑗 ∈ (0..^(#‘𝑊))((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0) |
11 | | elfzonn0 12380 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (0..^(#‘𝑊)) → 𝑗 ∈ ℕ0) |
12 | 11 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝑗 ∈ (0..^(#‘𝑊)) ∧ ((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊)))) → 𝑗 ∈ ℕ0) |
13 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) → 𝑊 ∈ Word 𝑉) |
14 | 13, 3 | anim12i 588 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ)) |
15 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ)) |
16 | 15 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ (0..^(#‘𝑊)) ∧ ((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊)))) → (𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ)) |
17 | | simpr3 1062 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝑊 cyclShift 𝐿) = 𝑊) |
18 | 17 | anim1i 590 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝑖 ∈ (0..^(#‘𝑊)))) |
19 | 18 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ (0..^(#‘𝑊)) ∧ ((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊)))) → ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝑖 ∈ (0..^(#‘𝑊)))) |
20 | | cshweqrep 13418 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝑖 ∈ (0..^(#‘𝑊))) → ∀𝑘 ∈ ℕ0 (𝑊‘𝑖) = (𝑊‘((𝑖 + (𝑘 · 𝐿)) mod (#‘𝑊))))) |
21 | 16, 19, 20 | sylc 63 |
. . . . . . . . 9
⊢ (((𝑗 ∈ (0..^(#‘𝑊)) ∧ ((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊)))) → ∀𝑘 ∈ ℕ0 (𝑊‘𝑖) = (𝑊‘((𝑖 + (𝑘 · 𝐿)) mod (#‘𝑊)))) |
22 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → (𝑘 · 𝐿) = (𝑗 · 𝐿)) |
23 | 22 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → (𝑖 + (𝑘 · 𝐿)) = (𝑖 + (𝑗 · 𝐿))) |
24 | 23 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → ((𝑖 + (𝑘 · 𝐿)) mod (#‘𝑊)) = ((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊))) |
25 | 24 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → (𝑊‘((𝑖 + (𝑘 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)))) |
26 | 25 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → ((𝑊‘𝑖) = (𝑊‘((𝑖 + (𝑘 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊‘𝑖) = (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊))))) |
27 | 26 | rspcva 3280 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
ℕ0 (𝑊‘𝑖) = (𝑊‘((𝑖 + (𝑘 · 𝐿)) mod (#‘𝑊)))) → (𝑊‘𝑖) = (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)))) |
28 | 12, 21, 27 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑗 ∈ (0..^(#‘𝑊)) ∧ ((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝑖) = (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)))) |
29 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0 → (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊))) = (𝑊‘0)) |
30 | 29 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (0..^(#‘𝑊)) ∧ ((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0) → (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊))) = (𝑊‘0)) |
31 | 30 | adantr 480 |
. . . . . . . 8
⊢ (((𝑗 ∈ (0..^(#‘𝑊)) ∧ ((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊)))) → (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊))) = (𝑊‘0)) |
32 | 28, 31 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝑗 ∈ (0..^(#‘𝑊)) ∧ ((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊)))) → (𝑊‘𝑖) = (𝑊‘0)) |
33 | 32 | ex 449 |
. . . . . 6
⊢ ((𝑗 ∈ (0..^(#‘𝑊)) ∧ ((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0) → ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝑊‘𝑖) = (𝑊‘0))) |
34 | 33 | rexlimiva 3010 |
. . . . 5
⊢
(∃𝑗 ∈
(0..^(#‘𝑊))((𝑖 + (𝑗 · 𝐿)) mod (#‘𝑊)) = 0 → ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝑊‘𝑖) = (𝑊‘0))) |
35 | 10, 34 | mpcom 37 |
. . . 4
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(#‘𝑊))) → (𝑊‘𝑖) = (𝑊‘0)) |
36 | 35 | ralrimiva 2949 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
37 | | repswsymballbi 13378 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) ↔ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
38 | 37 | ad2antrr 758 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) ↔ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
39 | 36, 38 | mpbird 246 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → 𝑊 = ((𝑊‘0) repeatS (#‘𝑊))) |
40 | 39 | ex 449 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) → ((𝐿 ∈ ℤ ∧ (𝐿 mod (#‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝑊 = ((𝑊‘0) repeatS (#‘𝑊)))) |