Proof of Theorem cshwshashlem1
| Step | Hyp | Ref
| Expression |
| 1 | | df-ne 2941 |
. . . . . . 7
⊢ ((𝑊‘𝑖) ≠ (𝑊‘0) ↔ ¬ (𝑊‘𝑖) = (𝑊‘0)) |
| 2 | 1 | rexbii 3094 |
. . . . . 6
⊢
(∃𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ↔ ∃𝑖 ∈ (0..^(♯‘𝑊)) ¬ (𝑊‘𝑖) = (𝑊‘0)) |
| 3 | | rexnal 3100 |
. . . . . 6
⊢
(∃𝑖 ∈
(0..^(♯‘𝑊))
¬ (𝑊‘𝑖) = (𝑊‘0) ↔ ¬ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
| 4 | 2, 3 | bitri 275 |
. . . . 5
⊢
(∃𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ↔ ¬ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
| 5 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝜑) |
| 6 | | fzo0ss1 13729 |
. . . . . . . . . . . . . 14
⊢
(1..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊)) |
| 7 | | fzossfz 13718 |
. . . . . . . . . . . . . 14
⊢
(0..^(♯‘𝑊)) ⊆ (0...(♯‘𝑊)) |
| 8 | 6, 7 | sstri 3993 |
. . . . . . . . . . . . 13
⊢
(1..^(♯‘𝑊)) ⊆ (0...(♯‘𝑊)) |
| 9 | 8 | sseli 3979 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈
(1..^(♯‘𝑊))
→ 𝐿 ∈
(0...(♯‘𝑊))) |
| 10 | 9 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝐿 ∈ (0...(♯‘𝑊))) |
| 11 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝑊 cyclShift 𝐿) = 𝑊) |
| 12 | | cshwshash.0 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ)) |
| 13 | | simpll 767 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → 𝑊 ∈ Word 𝑉) |
| 14 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) →
(♯‘𝑊) ∈
ℙ) |
| 15 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (♯‘𝑊) ∈
ℙ) |
| 16 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ 𝐿 ∈
ℤ) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → 𝐿 ∈ ℤ) |
| 18 | | cshwsidrepswmod0 17132 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ ∧ 𝐿 ∈ ℤ) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))) |
| 19 | 13, 15, 17, 18 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))) |
| 20 | 19 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → (𝐿 ∈ (0...(♯‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))) |
| 21 | 20 | 3imp 1111 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))) |
| 22 | | olc 869 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 = (♯‘𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊))) |
| 23 | 22 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 = (♯‘𝑊) → (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)))) |
| 24 | | fzofzim 13749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐿 ≠ (♯‘𝑊) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → 𝐿 ∈ (0..^(♯‘𝑊))) |
| 25 | | zmodidfzoimp 13941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐿 ∈
(0..^(♯‘𝑊))
→ (𝐿 mod
(♯‘𝑊)) = 𝐿) |
| 26 | | eqtr2 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐿 mod (♯‘𝑊)) = 𝐿 ∧ (𝐿 mod (♯‘𝑊)) = 0) → 𝐿 = 0) |
| 27 | 26 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐿 mod (♯‘𝑊)) = 𝐿 ∧ (𝐿 mod (♯‘𝑊)) = 0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0)) |
| 28 | 27 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐿 mod (♯‘𝑊)) = 𝐿 → ((𝐿 mod (♯‘𝑊)) = 0 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0))) |
| 29 | 25, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐿 ∈
(0..^(♯‘𝑊))
→ ((𝐿 mod
(♯‘𝑊)) = 0
→ ((𝑊 ∈ Word
𝑉 ∧
(♯‘𝑊) ∈
ℙ) → 𝐿 =
0))) |
| 30 | 24, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐿 ≠ (♯‘𝑊) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝐿 mod (♯‘𝑊)) = 0 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0))) |
| 31 | 30 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ (𝐿 ≠
(♯‘𝑊) →
((𝐿 mod
(♯‘𝑊)) = 0
→ ((𝑊 ∈ Word
𝑉 ∧
(♯‘𝑊) ∈
ℙ) → 𝐿 =
0)))) |
| 32 | 31 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ ((𝑊 ∈ Word
𝑉 ∧
(♯‘𝑊) ∈
ℙ) → ((𝐿 mod
(♯‘𝑊)) = 0
→ (𝐿 ≠
(♯‘𝑊) →
𝐿 = 0)))) |
| 33 | 32 | impcom 407 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝐿 mod (♯‘𝑊)) = 0 → (𝐿 ≠ (♯‘𝑊) → 𝐿 = 0))) |
| 34 | 33 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ((𝐿 mod (♯‘𝑊)) = 0 → (𝐿 ≠ (♯‘𝑊) → 𝐿 = 0))) |
| 35 | 34 | impcom 407 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 ≠ (♯‘𝑊) → 𝐿 = 0)) |
| 36 | 35 | impcom 407 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐿 ≠ (♯‘𝑊) ∧ ((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊))) → 𝐿 = 0) |
| 37 | 36 | orcd 874 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 ≠ (♯‘𝑊) ∧ ((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊))) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊))) |
| 38 | 37 | ex 412 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 ≠ (♯‘𝑊) → (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)))) |
| 39 | 23, 38 | pm2.61ine 3025 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊))) |
| 40 | 39 | orcd 874 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))) |
| 41 | | df-3or 1088 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) ↔ ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))) |
| 42 | 40, 41 | sylibr 234 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))) |
| 43 | 42 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 mod (♯‘𝑊)) = 0 → (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))) |
| 44 | | 3mix3 1333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))) |
| 45 | 44 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) → (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))) |
| 46 | 43, 45 | jaoi 858 |
. . . . . . . . . . . . . 14
⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) → (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))) |
| 47 | 21, 46 | mpcom 38 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))) |
| 48 | 12, 47 | syl3an1 1164 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))) |
| 49 | | 3mix1 1331 |
. . . . . . . . . . . . . 14
⊢ (𝐿 = 0 → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 50 | 49 | a1d 25 |
. . . . . . . . . . . . 13
⊢ (𝐿 = 0 → ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
| 51 | | 3mix2 1332 |
. . . . . . . . . . . . . 14
⊢ (𝐿 = (♯‘𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 52 | 51 | a1d 25 |
. . . . . . . . . . . . 13
⊢ (𝐿 = (♯‘𝑊) → ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
| 53 | | repswsymballbi 14818 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 55 | 12, 54 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 56 | 55 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 57 | 56 | biimpa 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) ∧ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) → ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
| 58 | 57 | 3mix3d 1339 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) ∧ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 59 | 58 | expcom 413 |
. . . . . . . . . . . . 13
⊢ (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) → ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
| 60 | 50, 52, 59 | 3jaoi 1430 |
. . . . . . . . . . . 12
⊢ ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) → ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
| 61 | 48, 60 | mpcom 38 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 62 | 5, 10, 11, 61 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 63 | | elfzo1 13752 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∈
(1..^(♯‘𝑊))
↔ (𝐿 ∈ ℕ
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐿 <
(♯‘𝑊))) |
| 64 | | nnne0 12300 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 ∈ ℕ → 𝐿 ≠ 0) |
| 65 | | df-ne 2941 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐿 ≠ 0 ↔ ¬ 𝐿 = 0) |
| 66 | | pm2.21 123 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝐿 = 0 → (𝐿 = 0 → ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 67 | 65, 66 | sylbi 217 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 ≠ 0 → (𝐿 = 0 → ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 68 | 64, 67 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ ℕ → (𝐿 = 0 → ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 69 | 68 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℕ ∧
(♯‘𝑊) ∈
ℕ ∧ 𝐿 <
(♯‘𝑊)) →
(𝐿 = 0 → ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 70 | 63, 69 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈
(1..^(♯‘𝑊))
→ (𝐿 = 0 →
∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 71 | 70 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 72 | 71 | com12 32 |
. . . . . . . . . . 11
⊢ (𝐿 = 0 → (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 73 | | nnre 12273 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐿 ∈ ℕ → 𝐿 ∈
ℝ) |
| 74 | | ltne 11358 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ ℝ ∧ 𝐿 < (♯‘𝑊)) → (♯‘𝑊) ≠ 𝐿) |
| 75 | 73, 74 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐿 ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → (♯‘𝑊) ≠ 𝐿) |
| 76 | | df-ne 2941 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑊)
≠ 𝐿 ↔ ¬
(♯‘𝑊) = 𝐿) |
| 77 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿 = (♯‘𝑊) ↔ (♯‘𝑊) = 𝐿) |
| 78 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(♯‘𝑊) = 𝐿 → ((♯‘𝑊) = 𝐿 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 79 | 77, 78 | biimtrid 242 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(♯‘𝑊) = 𝐿 → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 80 | 76, 79 | sylbi 217 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝑊)
≠ 𝐿 → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 81 | 75, 80 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 82 | 81 | 3adant2 1132 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℕ ∧
(♯‘𝑊) ∈
ℕ ∧ 𝐿 <
(♯‘𝑊)) →
(𝐿 = (♯‘𝑊) → ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 83 | 63, 82 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈
(1..^(♯‘𝑊))
→ (𝐿 =
(♯‘𝑊) →
∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 84 | 83 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 85 | 84 | com12 32 |
. . . . . . . . . . 11
⊢ (𝐿 = (♯‘𝑊) → (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 86 | | ax-1 6 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 87 | 72, 85, 86 | 3jaoi 1430 |
. . . . . . . . . 10
⊢ ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) → (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
| 88 | 62, 87 | mpcom 38 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
| 89 | 88 | pm2.24d 151 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (𝑊 cyclShift 𝐿) ≠ 𝑊)) |
| 90 | 89 | exp31 419 |
. . . . . . 7
⊢ (𝜑 → (𝐿 ∈ (1..^(♯‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → (¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (𝑊 cyclShift 𝐿) ≠ 𝑊)))) |
| 91 | 90 | com34 91 |
. . . . . 6
⊢ (𝜑 → (𝐿 ∈ (1..^(♯‘𝑊)) → (¬ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊)))) |
| 92 | 91 | com23 86 |
. . . . 5
⊢ (𝜑 → (¬ ∀𝑖 ∈
(0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (𝐿 ∈ (1..^(♯‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊)))) |
| 93 | 4, 92 | biimtrid 242 |
. . . 4
⊢ (𝜑 → (∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) → (𝐿 ∈ (1..^(♯‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊)))) |
| 94 | 93 | 3imp 1111 |
. . 3
⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊)) |
| 95 | 94 | com12 32 |
. 2
⊢ ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊)) |
| 96 | | ax-1 6 |
. 2
⊢ ((𝑊 cyclShift 𝐿) ≠ 𝑊 → ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊)) |
| 97 | 95, 96 | pm2.61ine 3025 |
1
⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊) |