Proof of Theorem cshwshashlem1
Step | Hyp | Ref
| Expression |
1 | | df-ne 2782 |
. . . . . . 7
⊢ ((𝑊‘𝑖) ≠ (𝑊‘0) ↔ ¬ (𝑊‘𝑖) = (𝑊‘0)) |
2 | 1 | rexbii 3023 |
. . . . . 6
⊢
(∃𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ↔ ∃𝑖 ∈ (0..^(#‘𝑊)) ¬ (𝑊‘𝑖) = (𝑊‘0)) |
3 | | rexnal 2978 |
. . . . . 6
⊢
(∃𝑖 ∈
(0..^(#‘𝑊)) ¬
(𝑊‘𝑖) = (𝑊‘0) ↔ ¬ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
4 | 2, 3 | bitri 263 |
. . . . 5
⊢
(∃𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ↔ ¬ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
5 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(#‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝜑) |
6 | | fzo0ss1 12367 |
. . . . . . . . . . . . . 14
⊢
(1..^(#‘𝑊))
⊆ (0..^(#‘𝑊)) |
7 | | fzossfz 12357 |
. . . . . . . . . . . . . 14
⊢
(0..^(#‘𝑊))
⊆ (0...(#‘𝑊)) |
8 | 6, 7 | sstri 3577 |
. . . . . . . . . . . . 13
⊢
(1..^(#‘𝑊))
⊆ (0...(#‘𝑊)) |
9 | 8 | sseli 3564 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ (1..^(#‘𝑊)) → 𝐿 ∈ (0...(#‘𝑊))) |
10 | 9 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(#‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝐿 ∈ (0...(#‘𝑊))) |
11 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(#‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝑊 cyclShift 𝐿) = 𝑊) |
12 | | cshwshash.0 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ)) |
13 | | simpll 786 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊))) → 𝑊 ∈ Word 𝑉) |
14 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) → (#‘𝑊) ∈
ℙ) |
15 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊))) → (#‘𝑊) ∈ ℙ) |
16 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿 ∈ (0...(#‘𝑊)) → 𝐿 ∈ ℤ) |
17 | 16 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊))) → 𝐿 ∈ ℤ) |
18 | | cshwsidrepswmod0 15639 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ ∧ 𝐿 ∈ ℤ) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (#‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊))))) |
19 | 13, 15, 17, 18 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊))) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (#‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊))))) |
20 | 19 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) → (𝐿 ∈ (0...(#‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (#‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊)))))) |
21 | 20 | 3imp 1249 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ((𝐿 mod (#‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊)))) |
22 | | olc 398 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 = (#‘𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊))) |
23 | 22 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 = (#‘𝑊) → (((𝐿 mod (#‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊)))) |
24 | | fzofzim 12382 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐿 ≠ (#‘𝑊) ∧ 𝐿 ∈ (0...(#‘𝑊))) → 𝐿 ∈ (0..^(#‘𝑊))) |
25 | | zmodidfzoimp 12562 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐿 ∈ (0..^(#‘𝑊)) → (𝐿 mod (#‘𝑊)) = 𝐿) |
26 | | eqtr2 2630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐿 mod (#‘𝑊)) = 𝐿 ∧ (𝐿 mod (#‘𝑊)) = 0) → 𝐿 = 0) |
27 | 26 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐿 mod (#‘𝑊)) = 𝐿 ∧ (𝐿 mod (#‘𝑊)) = 0) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) → 𝐿 = 0)) |
28 | 27 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐿 ∈ (0...(#‘𝑊)) → (𝐿 ≠ (#‘𝑊) → ((𝐿 mod (#‘𝑊)) = 0 → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) → 𝐿 = 0)))) |
32 | 31 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐿 ∈ (0...(#‘𝑊)) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) → ((𝐿 mod (#‘𝑊)) = 0 → (𝐿 ≠ (#‘𝑊) → 𝐿 = 0)))) |
33 | 32 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊))) → ((𝐿 mod (#‘𝑊)) = 0 → (𝐿 ≠ (#‘𝑊) → 𝐿 = 0))) |
34 | 33 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ((𝐿 mod (#‘𝑊)) = 0 → (𝐿 ≠ (#‘𝑊) → 𝐿 = 0))) |
35 | 34 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐿 mod (#‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 ≠ (#‘𝑊) → 𝐿 = 0)) |
36 | 35 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐿 ≠ (#‘𝑊) ∧ ((𝐿 mod (#‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊))) → 𝐿 = 0) |
37 | 36 | orcd 406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 ≠ (#‘𝑊) ∧ ((𝐿 mod (#‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊))) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊))) |
38 | 37 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 ≠ (#‘𝑊) → (((𝐿 mod (#‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊)))) |
39 | 23, 38 | pm2.61ine 2865 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐿 mod (#‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊))) |
40 | 39 | orcd 406 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐿 mod (#‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → ((𝐿 = 0 ∨ 𝐿 = (#‘𝑊)) ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊)))) |
41 | | df-3or 1032 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊))) ↔ ((𝐿 = 0 ∨ 𝐿 = (#‘𝑊)) ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊)))) |
42 | 40, 41 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐿 mod (#‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊)))) |
43 | 42 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 mod (#‘𝑊)) = 0 → (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊))))) |
44 | | 3mix3 1225 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊)))) |
45 | 44 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) → (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊))))) |
46 | 43, 45 | jaoi 393 |
. . . . . . . . . . . . . 14
⊢ (((𝐿 mod (#‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊))) → (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊))))) |
47 | 21, 46 | mpcom 37 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊)))) |
48 | 12, 47 | syl3an1 1351 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊)))) |
49 | | 3mix1 1223 |
. . . . . . . . . . . . . 14
⊢ (𝐿 = 0 → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
50 | 49 | a1d 25 |
. . . . . . . . . . . . 13
⊢ (𝐿 = 0 → ((𝜑 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
51 | | 3mix2 1224 |
. . . . . . . . . . . . . 14
⊢ (𝐿 = (#‘𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
52 | 51 | a1d 25 |
. . . . . . . . . . . . 13
⊢ (𝐿 = (#‘𝑊) → ((𝜑 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
53 | | repswsymballbi 13378 |
. . . . . . . . . . . . . . . . . . 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 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) ↔ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
57 | 56 | biimpa 500 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) ∧ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊))) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
58 | 57 | 3mix3d 1231 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) ∧ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊))) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
59 | 58 | expcom 450 |
. . . . . . . . . . . . 13
⊢ (𝑊 = ((𝑊‘0) repeatS (#‘𝑊)) → ((𝜑 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
60 | 50, 52, 59 | 3jaoi 1383 |
. . . . . . . . . . . 12
⊢ ((𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (#‘𝑊))) → ((𝜑 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))) |
61 | 48, 60 | mpcom 37 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
62 | 5, 10, 11, 61 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(#‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
63 | | elfzo1 12385 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∈ (1..^(#‘𝑊)) ↔ (𝐿 ∈ ℕ ∧ (#‘𝑊) ∈ ℕ ∧ 𝐿 < (#‘𝑊))) |
64 | | nnne0 10930 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 ∈ ℕ → 𝐿 ≠ 0) |
65 | | df-ne 2782 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐿 ≠ 0 ↔ ¬ 𝐿 = 0) |
66 | | pm2.21 119 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝐿 = 0 → (𝐿 = 0 → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
67 | 65, 66 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 ≠ 0 → (𝐿 = 0 → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
68 | 64, 67 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ ℕ → (𝐿 = 0 → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
69 | 68 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝐿 < (#‘𝑊)) → (𝐿 = 0 → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
70 | 63, 69 | sylbi 206 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈ (1..^(#‘𝑊)) → (𝐿 = 0 → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
71 | 70 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(#‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
72 | 71 | com12 32 |
. . . . . . . . . . 11
⊢ (𝐿 = 0 → (((𝜑 ∧ 𝐿 ∈ (1..^(#‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
73 | | nnre 10904 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐿 ∈ ℕ → 𝐿 ∈
ℝ) |
74 | | ltne 10013 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ ℝ ∧ 𝐿 < (#‘𝑊)) → (#‘𝑊) ≠ 𝐿) |
75 | 73, 74 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐿 ∈ ℕ ∧ 𝐿 < (#‘𝑊)) → (#‘𝑊) ≠ 𝐿) |
76 | | df-ne 2782 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑊) ≠
𝐿 ↔ ¬
(#‘𝑊) = 𝐿) |
77 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿 = (#‘𝑊) ↔ (#‘𝑊) = 𝐿) |
78 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(#‘𝑊) = 𝐿 → ((#‘𝑊) = 𝐿 → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
79 | 77, 78 | syl5bi 231 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(#‘𝑊) = 𝐿 → (𝐿 = (#‘𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
80 | 76, 79 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) ≠
𝐿 → (𝐿 = (#‘𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
81 | 75, 80 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ ℕ ∧ 𝐿 < (#‘𝑊)) → (𝐿 = (#‘𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
82 | 81 | 3adant2 1073 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℕ ∧
(#‘𝑊) ∈ ℕ
∧ 𝐿 < (#‘𝑊)) → (𝐿 = (#‘𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
83 | 63, 82 | sylbi 206 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈ (1..^(#‘𝑊)) → (𝐿 = (#‘𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
84 | 83 | ad2antlr 759 |
. . . . . . . . . . . 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 1383 |
. . . . . . . . . 10
⊢ ((𝐿 = 0 ∨ 𝐿 = (#‘𝑊) ∨ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) → (((𝜑 ∧ 𝐿 ∈ (1..^(#‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
88 | 62, 87 | mpcom 37 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(#‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
89 | 88 | pm2.24d 146 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(#‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (¬ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (𝑊 cyclShift 𝐿) ≠ 𝑊)) |
90 | 89 | exp31 628 |
. . . . . . 7
⊢ (𝜑 → (𝐿 ∈ (1..^(#‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → (¬ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (𝑊 cyclShift 𝐿) ≠ 𝑊)))) |
91 | 90 | com34 89 |
. . . . . 6
⊢ (𝜑 → (𝐿 ∈ (1..^(#‘𝑊)) → (¬ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊)))) |
92 | 91 | com23 84 |
. . . . 5
⊢ (𝜑 → (¬ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (𝐿 ∈ (1..^(#‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊)))) |
93 | 4, 92 | syl5bi 231 |
. . . 4
⊢ (𝜑 → (∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) → (𝐿 ∈ (1..^(#‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊)))) |
94 | 93 | 3imp 1249 |
. . 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 2865 |
1
⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(#‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊) |