| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) →
(♯‘𝑊) ∈
ℙ) |
| 2 | 1 | adantr 480 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (♯‘𝑊) ∈ ℙ) |
| 3 | | simp1 1137 |
. . . . . . . . 9
⊢ ((𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝐿 ∈ ℤ) |
| 4 | 3 | adantl 481 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → 𝐿 ∈ ℤ) |
| 5 | | simpr2 1196 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 mod (♯‘𝑊)) ≠ 0) |
| 6 | 2, 4, 5 | 3jca 1129 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → ((♯‘𝑊) ∈ ℙ ∧ 𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0)) |
| 7 | 6 | adantr 480 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((♯‘𝑊) ∈ ℙ ∧ 𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0)) |
| 8 | | simpr 484 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → 𝑖 ∈ (0..^(♯‘𝑊))) |
| 9 | | modprmn0modprm0 16845 |
. . . . . 6
⊢
(((♯‘𝑊)
∈ ℙ ∧ 𝐿
∈ ℤ ∧ (𝐿 mod
(♯‘𝑊)) ≠ 0)
→ (𝑖 ∈
(0..^(♯‘𝑊))
→ ∃𝑗 ∈
(0..^(♯‘𝑊))((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0)) |
| 10 | 7, 8, 9 | sylc 65 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ∃𝑗 ∈ (0..^(♯‘𝑊))((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0) |
| 11 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝑘 · 𝐿) = (𝑗 · 𝐿)) |
| 12 | 11 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → (𝑖 + (𝑘 · 𝐿)) = (𝑖 + (𝑗 · 𝐿))) |
| 13 | 12 | fvoveq1d 7453 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝑊‘((𝑖 + (𝑘 · 𝐿)) mod (♯‘𝑊))) = (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)))) |
| 14 | 13 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝑊‘𝑖) = (𝑊‘((𝑖 + (𝑘 · 𝐿)) mod (♯‘𝑊))) ↔ (𝑊‘𝑖) = (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊))))) |
| 15 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝑊 ∈ Word 𝑉) |
| 16 | 15, 3 | anim12i 613 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ)) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ)) |
| 18 | 17 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑗 ∈
(0..^(♯‘𝑊))
∧ ((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊)))) → (𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ)) |
| 19 | | simpr3 1197 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝑊 cyclShift 𝐿) = 𝑊) |
| 20 | 19 | anim1i 615 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝑖 ∈ (0..^(♯‘𝑊)))) |
| 21 | 20 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑗 ∈
(0..^(♯‘𝑊))
∧ ((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊)))) → ((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝑖 ∈ (0..^(♯‘𝑊)))) |
| 22 | | cshweqrep 14859 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ∀𝑘 ∈ ℕ0 (𝑊‘𝑖) = (𝑊‘((𝑖 + (𝑘 · 𝐿)) mod (♯‘𝑊))))) |
| 23 | 18, 21, 22 | sylc 65 |
. . . . . . . . 9
⊢ (((𝑗 ∈
(0..^(♯‘𝑊))
∧ ((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊)))) → ∀𝑘 ∈ ℕ0 (𝑊‘𝑖) = (𝑊‘((𝑖 + (𝑘 · 𝐿)) mod (♯‘𝑊)))) |
| 24 | | elfzonn0 13747 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(0..^(♯‘𝑊))
→ 𝑗 ∈
ℕ0) |
| 25 | 24 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑗 ∈
(0..^(♯‘𝑊))
∧ ((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊)))) → 𝑗 ∈ ℕ0) |
| 26 | 14, 23, 25 | rspcdva 3623 |
. . . . . . . 8
⊢ (((𝑗 ∈
(0..^(♯‘𝑊))
∧ ((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝑖) = (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)))) |
| 27 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0 → (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊))) = (𝑊‘0)) |
| 28 | 27 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑗 ∈
(0..^(♯‘𝑊))
∧ ((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0) → (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊))) = (𝑊‘0)) |
| 29 | 28 | adantr 480 |
. . . . . . . 8
⊢ (((𝑗 ∈
(0..^(♯‘𝑊))
∧ ((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊)))) → (𝑊‘((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊))) = (𝑊‘0)) |
| 30 | 26, 29 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝑗 ∈
(0..^(♯‘𝑊))
∧ ((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0) ∧ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊)))) → (𝑊‘𝑖) = (𝑊‘0)) |
| 31 | 30 | ex 412 |
. . . . . 6
⊢ ((𝑗 ∈
(0..^(♯‘𝑊))
∧ ((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0) → ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (𝑊‘𝑖) = (𝑊‘0))) |
| 32 | 31 | rexlimiva 3147 |
. . . . 5
⊢
(∃𝑗 ∈
(0..^(♯‘𝑊))((𝑖 + (𝑗 · 𝐿)) mod (♯‘𝑊)) = 0 → ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (𝑊‘𝑖) = (𝑊‘0))) |
| 33 | 10, 32 | mpcom 38 |
. . . 4
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → (𝑊‘𝑖) = (𝑊‘0)) |
| 34 | 33 | ralrimiva 3146 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
| 35 | | repswsymballbi 14818 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 36 | 35 | ad2antrr 726 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 37 | 34, 36 | mpbird 257 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ (𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) |
| 38 | 37 | ex 412 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → ((𝐿 ∈ ℤ ∧ (𝐿 mod (♯‘𝑊)) ≠ 0 ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))) |