Proof of Theorem cshw1
Step | Hyp | Ref
| Expression |
1 | | ral0 4109 |
. . . 4
⊢
∀𝑖 ∈
∅ (𝑊‘𝑖) = (𝑊‘0) |
2 | | oveq2 6698 |
. . . . . 6
⊢
((#‘𝑊) = 0
→ (0..^(#‘𝑊)) =
(0..^0)) |
3 | | fzo0 12531 |
. . . . . 6
⊢ (0..^0) =
∅ |
4 | 2, 3 | syl6eq 2701 |
. . . . 5
⊢
((#‘𝑊) = 0
→ (0..^(#‘𝑊)) =
∅) |
5 | 4 | raleqdv 3174 |
. . . 4
⊢
((#‘𝑊) = 0
→ (∀𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0) ↔ ∀𝑖 ∈ ∅ (𝑊‘𝑖) = (𝑊‘0))) |
6 | 1, 5 | mpbiri 248 |
. . 3
⊢
((#‘𝑊) = 0
→ ∀𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
7 | 6 | a1d 25 |
. 2
⊢
((#‘𝑊) = 0
→ ((𝑊 ∈ Word
𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
8 | | simprl 809 |
. . . . . . . 8
⊢ (((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) ∧
(𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊)) → 𝑊 ∈ Word 𝑉) |
9 | | lencl 13356 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
10 | | 1nn0 11346 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ0 |
11 | 10 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1)) → 1 ∈
ℕ0) |
12 | | df-ne 2824 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) ≠ 0
↔ ¬ (#‘𝑊) =
0) |
13 | | elnnne0 11344 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑊) ∈
ℕ ↔ ((#‘𝑊)
∈ ℕ0 ∧ (#‘𝑊) ≠ 0)) |
14 | 13 | simplbi2com 656 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) ≠ 0
→ ((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℕ)) |
15 | 12, 14 | sylbir 225 |
. . . . . . . . . . . . . . 15
⊢ (¬
(#‘𝑊) = 0 →
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℕ)) |
16 | 15 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) →
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℕ)) |
17 | 16 | impcom 445 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1)) → (#‘𝑊) ∈ ℕ) |
18 | | df-ne 2824 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) ≠ 1
↔ ¬ (#‘𝑊) =
1) |
19 | 18 | biimpri 218 |
. . . . . . . . . . . . . . 15
⊢ (¬
(#‘𝑊) = 1 →
(#‘𝑊) ≠
1) |
20 | 19 | ad2antll 765 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1)) → (#‘𝑊) ≠ 1) |
21 | | nngt1ne1 11085 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) ∈
ℕ → (1 < (#‘𝑊) ↔ (#‘𝑊) ≠ 1)) |
22 | 17, 21 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1)) → (1 < (#‘𝑊) ↔ (#‘𝑊) ≠ 1)) |
23 | 20, 22 | mpbird 247 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (¬ (#‘𝑊) = 0 ∧ ¬ (#‘𝑊) = 1)) → 1 < (#‘𝑊)) |
24 | | elfzo0 12548 |
. . . . . . . . . . . . 13
⊢ (1 ∈
(0..^(#‘𝑊)) ↔ (1
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ ∧ 1 < (#‘𝑊))) |
25 | 11, 17, 23, 24 | syl3anbrc 1265 |
. . . . . . . . . . . 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 811 |
. . . . . . . 8
⊢ (((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) ∧
(𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊)) → (𝑊 cyclShift 1) = 𝑊) |
31 | | lbfzo0 12547 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
(0..^(#‘𝑊)) ↔
(#‘𝑊) ∈
ℕ) |
32 | 31 | biimpri 218 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝑊) ∈
ℕ → 0 ∈ (0..^(#‘𝑊))) |
33 | 13, 32 | sylbir 225 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝑊) ∈
ℕ0 ∧ (#‘𝑊) ≠ 0) → 0 ∈
(0..^(#‘𝑊))) |
34 | 33 | ex 449 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑊) ∈
ℕ0 → ((#‘𝑊) ≠ 0 → 0 ∈ (0..^(#‘𝑊)))) |
35 | 12, 34 | syl5bir 233 |
. . . . . . . . . . . . 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 12509 |
. . . . . . . . . 10
⊢ (1 ∈
(0..^(#‘𝑊)) → 1
∈ ℤ) |
42 | | cshweqrep 13613 |
. . . . . . . . . 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 1367 |
. . . . . . 7
⊢ (((¬
(#‘𝑊) = 0 ∧ ¬
(#‘𝑊) = 1) ∧
(𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊)) → ∀𝑖 ∈ ℕ0 (𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊)))) |
46 | | 0nn0 11345 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
47 | | fzossnn0 12538 |
. . . . . . . . 9
⊢ (0 ∈
ℕ0 → (0..^(#‘𝑊)) ⊆
ℕ0) |
48 | | ssralv 3699 |
. . . . . . . . 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 2658 |
. . . . . . . . . 10
⊢ ((𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) ↔ (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) = (𝑊‘0)) |
51 | | elfzoelz 12509 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → 𝑖 ∈ ℤ) |
52 | | zre 11419 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℝ) |
53 | | ax-1rid 10044 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℝ → (𝑖 · 1) = 𝑖) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℤ → (𝑖 · 1) = 𝑖) |
55 | 54 | oveq2d 6706 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℤ → (0 +
(𝑖 · 1)) = (0 +
𝑖)) |
56 | | zcn 11420 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℤ → 𝑖 ∈
ℂ) |
57 | 56 | addid2d 10275 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℤ → (0 +
𝑖) = 𝑖) |
58 | 55, 57 | eqtrd 2685 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ℤ → (0 +
(𝑖 · 1)) = 𝑖) |
59 | 51, 58 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → (0 + (𝑖 · 1)) = 𝑖) |
60 | 59 | oveq1d 6705 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → ((0 + (𝑖 · 1)) mod (#‘𝑊)) = (𝑖 mod (#‘𝑊))) |
61 | | zmodidfzoimp 12740 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → (𝑖 mod (#‘𝑊)) = 𝑖) |
62 | 60, 61 | eqtrd 2685 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → ((0 + (𝑖 · 1)) mod (#‘𝑊)) = 𝑖) |
63 | 62 | fveq2d 6233 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) = (𝑊‘𝑖)) |
64 | 63 | eqeq1d 2653 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → ((𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) = (𝑊‘0) ↔ (𝑊‘𝑖) = (𝑊‘0))) |
65 | 64 | biimpd 219 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → ((𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) = (𝑊‘0) → (𝑊‘𝑖) = (𝑊‘0))) |
66 | 50, 65 | syl5bi 232 |
. . . . . . . . 9
⊢ (𝑖 ∈ (0..^(#‘𝑊)) → ((𝑊‘0) = (𝑊‘((0 + (𝑖 · 1)) mod (#‘𝑊))) → (𝑊‘𝑖) = (𝑊‘0))) |
67 | 66 | ralimia 2979 |
. . . . . . . 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 2651 |
. . . . . 6
⊢ (𝑊‘0) = (𝑊‘0) |
73 | | c0ex 10072 |
. . . . . . 7
⊢ 0 ∈
V |
74 | | fveq2 6229 |
. . . . . . . 8
⊢ (𝑖 = 0 → (𝑊‘𝑖) = (𝑊‘0)) |
75 | 74 | eqeq1d 2653 |
. . . . . . 7
⊢ (𝑖 = 0 → ((𝑊‘𝑖) = (𝑊‘0) ↔ (𝑊‘0) = (𝑊‘0))) |
76 | 73, 75 | ralsn 4254 |
. . . . . 6
⊢
(∀𝑖 ∈
{0} (𝑊‘𝑖) = (𝑊‘0) ↔ (𝑊‘0) = (𝑊‘0)) |
77 | 72, 76 | mpbir 221 |
. . . . 5
⊢
∀𝑖 ∈ {0}
(𝑊‘𝑖) = (𝑊‘0) |
78 | | oveq2 6698 |
. . . . . . 7
⊢
((#‘𝑊) = 1
→ (0..^(#‘𝑊)) =
(0..^1)) |
79 | | fzo01 12590 |
. . . . . . 7
⊢ (0..^1) =
{0} |
80 | 78, 79 | syl6eq 2701 |
. . . . . 6
⊢
((#‘𝑊) = 1
→ (0..^(#‘𝑊)) =
{0}) |
81 | 80 | raleqdv 3174 |
. . . . 5
⊢
((#‘𝑊) = 1
→ (∀𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0) ↔ ∀𝑖 ∈ {0} (𝑊‘𝑖) = (𝑊‘0))) |
82 | 77, 81 | mpbiri 248 |
. . . 4
⊢
((#‘𝑊) = 1
→ ∀𝑖 ∈
(0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
83 | 71, 82 | pm2.61d2 172 |
. . 3
⊢ ((¬
(#‘𝑊) = 0 ∧
(𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊)) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |
84 | 83 | ex 449 |
. 2
⊢ (¬
(#‘𝑊) = 0 →
((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0))) |
85 | 7, 84 | pm2.61i 176 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) |