Proof of Theorem cshw1
Step | Hyp | Ref
| Expression |
1 | | ral0 4028 |
. . . 4
⊢
∀𝑖 ∈
∅ (𝑊‘𝑖) = (𝑊‘0) |
2 | | oveq2 6557 |
. . . . . 6
⊢
((#‘𝑊) = 0
→ (0..^(#‘𝑊)) =
(0..^0)) |
3 | | fzo0 12361 |
. . . . . 6
⊢ (0..^0) =
∅ |
4 | 2, 3 | syl6eq 2660 |
. . . . 5
⊢
((#‘𝑊) = 0
→ (0..^(#‘𝑊)) =
∅) |
5 | 4 | raleqdv 3121 |
. . . 4
⊢
((#‘𝑊) = 0
→ (∀𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0) ↔ ∀𝑖 ∈ ∅ (𝑊‘𝑖) = (𝑊‘0))) |
6 | 1, 5 | mpbiri 247 |
. . 3
⊢
((#‘𝑊) = 0
→ ∀𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
7 | 6 | a1d 25 |
. 2
⊢
((#‘𝑊) = 0
→ ((𝑊 ∈ Word
𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
8 | | simprl 790 |
. . . . . . . 8
⊢ (((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) ∧
(𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊)) → 𝑊 ∈ Word 𝑉) |
9 | | lencl 13179 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
10 | | 1nn0 11185 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ0 |
11 | 10 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1)) → 1 ∈
ℕ0) |
12 | | df-ne 2782 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) ≠ 0
↔ ¬ (#‘𝑊) =
0) |
13 | | elnnne0 11183 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑊) ∈
ℕ ↔ ((#‘𝑊)
∈ ℕ0 ∧ (#‘𝑊) ≠ 0)) |
14 | 13 | simplbi2com 655 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) ≠ 0
→ ((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℕ)) |
15 | 12, 14 | sylbir 224 |
. . . . . . . . . . . . . . 15
⊢ (¬
(#‘𝑊) = 0 →
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℕ)) |
16 | 15 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) →
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℕ)) |
17 | 16 | impcom 445 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1)) → (#‘𝑊) ∈ ℕ) |
18 | | df-ne 2782 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) ≠ 1
↔ ¬ (#‘𝑊) =
1) |
19 | 18 | biimpri 217 |
. . . . . . . . . . . . . . 15
⊢ (¬
(#‘𝑊) = 1 →
(#‘𝑊) ≠
1) |
20 | 19 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1)) → (#‘𝑊) ≠ 1) |
21 | | nngt1ne1 10924 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) ∈
ℕ → (1 < (#‘𝑊) ↔ (#‘𝑊) ≠ 1)) |
22 | 17, 21 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1)) → (1 < (#‘𝑊) ↔ (#‘𝑊) ≠ 1)) |
23 | 20, 22 | mpbird 246 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1)) → 1 < (#‘𝑊)) |
24 | | elfzo0 12376 |
. . . . . . . . . . . . 13
⊢ (1 ∈
(0..^(#‘𝑊)) ↔ (1
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ ∧ 1 < (#‘𝑊))) |
25 | 11, 17, 23, 24 | syl3anbrc 1239 |
. . . . . . . . . . . 12
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1)) → 1 ∈ (0..^(#‘𝑊))) |
26 | 25 | ex 449 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
ℕ0 → ((¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1) → 1 ∈ (0..^(#‘𝑊)))) |
27 | 9, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → ((¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1) → 1 ∈ (0..^(#‘𝑊)))) |
28 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → ((¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1) → 1 ∈ (0..^(#‘𝑊)))) |
29 | 28 | impcom 445 |
. . . . . . . 8
⊢ (((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) ∧
(𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊)) → 1 ∈ (0..^(#‘𝑊))) |
30 | | simprr 792 |
. . . . . . . 8
⊢ (((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) ∧
(𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊)) → (𝑊 cyclShift 1) = 𝑊) |
31 | | lbfzo0 12375 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
(0..^(#‘𝑊)) ↔
(#‘𝑊) ∈
ℕ) |
32 | 31 | biimpri 217 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) ∈
ℕ → 0 ∈ (0..^(#‘𝑊))) |
33 | 13, 32 | sylbir 224 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (#‘𝑊) ≠ 0) → 0 ∈
(0..^(#‘𝑊))) |
34 | 33 | ex 449 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) ∈
ℕ0 → ((#‘𝑊) ≠ 0 → 0 ∈ (0..^(#‘𝑊)))) |
35 | 12, 34 | syl5bir 232 |
. . . . . . . . . . . . 13
⊢
((#‘𝑊) ∈
ℕ0 → (¬ (#‘𝑊) = 0 → 0 ∈ (0..^(#‘𝑊)))) |
36 | 9, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝑉 → (¬ (#‘𝑊) = 0 → 0 ∈ (0..^(#‘𝑊)))) |
37 | 36 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → (¬ (#‘𝑊) = 0 → 0 ∈ (0..^(#‘𝑊)))) |
38 | 37 | com12 32 |
. . . . . . . . . 10
⊢ (¬
(#‘𝑊) = 0 →
((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → 0 ∈ (0..^(#‘𝑊)))) |
39 | 38 | adantr 480 |
. . . . . . . . 9
⊢ ((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) →
((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → 0 ∈ (0..^(#‘𝑊)))) |
40 | 39 | imp 444 |
. . . . . . . 8
⊢ (((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) ∧
(𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊)) → 0 ∈ (0..^(#‘𝑊))) |
41 | | elfzoelz 12339 |
. . . . . . . . . 10
⊢ (1 ∈
(0..^(#‘𝑊)) → 1
∈ ℤ) |
42 | | cshweqrep 13418 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ∈ ℤ) → (((𝑊 cyclShift 1) = 𝑊 ∧ 0 ∈
(0..^(#‘𝑊))) →
∀𝑖 ∈
ℕ0 (𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))))) |
43 | 41, 42 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ∈ (0..^(#‘𝑊))) → (((𝑊 cyclShift 1) = 𝑊 ∧ 0 ∈ (0..^(#‘𝑊))) → ∀𝑖 ∈ ℕ0
(𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))))) |
44 | 43 | imp 444 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 1 ∈ (0..^(#‘𝑊))) ∧ ((𝑊 cyclShift 1) = 𝑊 ∧ 0 ∈ (0..^(#‘𝑊)))) → ∀𝑖 ∈ ℕ0
(𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊)))) |
45 | 8, 29, 30, 40, 44 | syl22anc 1319 |
. . . . . . 7
⊢ (((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) ∧
(𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊)) → ∀𝑖 ∈ ℕ0 (𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊)))) |
46 | | 0nn0 11184 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
47 | | fzossnn0 12368 |
. . . . . . . . 9
⊢ (0 ∈
ℕ0 → (0..^(#‘𝑊)) ⊆
ℕ0) |
48 | | ssralv 3629 |
. . . . . . . . 9
⊢
((0..^(#‘𝑊))
⊆ ℕ0 → (∀𝑖 ∈ ℕ0 (𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))))) |
49 | 46, 47, 48 | mp2b 10 |
. . . . . . . 8
⊢
(∀𝑖 ∈
ℕ0 (𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊)))) |
50 | | eqcom 2617 |
. . . . . . . . . 10
⊢ ((𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) ↔ (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) = (𝑊‘0)) |
51 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → 𝑖 ∈ ℤ) |
52 | | zre 11258 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℝ) |
53 | | ax-1rid 9885 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℝ → (𝑖 · 1) = 𝑖) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℤ → (𝑖 · 1) = 𝑖) |
55 | 54 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℤ → (0 +
(𝑖 · 1)) = (0 +
𝑖)) |
56 | | zcn 11259 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℂ) |
57 | 56 | addid2d 10116 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℤ → (0 +
𝑖) = 𝑖) |
58 | 55, 57 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℤ → (0 +
(𝑖 · 1)) = 𝑖) |
59 | 51, 58 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → (0 + (𝑖 · 1)) = 𝑖) |
60 | 59 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → ((0 + (𝑖 · 1)) mod (#‘𝑊)) = (𝑖 mod (#‘𝑊))) |
61 | | zmodidfzoimp 12562 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → (𝑖 mod (#‘𝑊)) = 𝑖) |
62 | 60, 61 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → ((0 + (𝑖 · 1)) mod (#‘𝑊)) = 𝑖) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) = (𝑊‘𝑖)) |
64 | 63 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → ((𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) = (𝑊‘0) ↔ (𝑊‘𝑖) = (𝑊‘0))) |
65 | 64 | biimpd 218 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → ((𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) = (𝑊‘0) → (𝑊‘𝑖) = (𝑊‘0))) |
66 | 50, 65 | syl5bi 231 |
. . . . . . . . 9
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → ((𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) → (𝑊‘𝑖) = (𝑊‘0))) |
67 | 66 | ralimia 2934 |
. . . . . . . 8
⊢
(∀𝑖 ∈
(0..^(#‘𝑊))(𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
68 | 49, 67 | syl 17 |
. . . . . . 7
⊢
(∀𝑖 ∈
ℕ0 (𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
69 | 45, 68 | syl 17 |
. . . . . 6
⊢ (((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) ∧
(𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊)) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
70 | 69 | ex 449 |
. . . . 5
⊢ ((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) →
((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
71 | 70 | impancom 455 |
. . . 4
⊢ ((¬
(#‘𝑊) = 0 ∧
(𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊)) → (¬ (#‘𝑊) = 1 → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
72 | | eqid 2610 |
. . . . . 6
⊢ (𝑊‘0) = (𝑊‘0) |
73 | | c0ex 9913 |
. . . . . . 7
⊢ 0 ∈
V |
74 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑖 = 0 → (𝑊‘𝑖) = (𝑊‘0)) |
75 | 74 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑖 = 0 → ((𝑊‘𝑖) = (𝑊‘0) ↔ (𝑊‘0) = (𝑊‘0))) |
76 | 73, 75 | ralsn 4169 |
. . . . . 6
⊢
(∀𝑖 ∈
{0} (𝑊‘𝑖) = (𝑊‘0) ↔ (𝑊‘0) = (𝑊‘0)) |
77 | 72, 76 | mpbir 220 |
. . . . 5
⊢
∀𝑖 ∈ {0}
(𝑊‘𝑖) = (𝑊‘0) |
78 | | oveq2 6557 |
. . . . . . 7
⊢
((#‘𝑊) = 1
→ (0..^(#‘𝑊)) =
(0..^1)) |
79 | | fzo01 12417 |
. . . . . . 7
⊢ (0..^1) =
{0} |
80 | 78, 79 | syl6eq 2660 |
. . . . . 6
⊢
((#‘𝑊) = 1
→ (0..^(#‘𝑊)) =
{0}) |
81 | 80 | raleqdv 3121 |
. . . . 5
⊢
((#‘𝑊) = 1
→ (∀𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0) ↔ ∀𝑖 ∈ {0} (𝑊‘𝑖) = (𝑊‘0))) |
82 | 77, 81 | mpbiri 247 |
. . . 4
⊢
((#‘𝑊) = 1
→ ∀𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
83 | 71, 82 | pm2.61d2 171 |
. . 3
⊢ ((¬
(#‘𝑊) = 0 ∧
(𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊)) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
84 | 83 | ex 449 |
. 2
⊢ (¬
(#‘𝑊) = 0 →
((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
85 | 7, 84 | pm2.61i 175 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |