Proof of Theorem cshwidxm1
Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) → 𝑊 ∈ Word 𝑉) |
2 | | elfzoelz 13387 |
. . . 4
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
→ 𝑁 ∈
ℤ) |
3 | 2 | adantl 482 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) → 𝑁 ∈ ℤ) |
4 | | ubmelm1fzo 13483 |
. . . 4
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
→ (((♯‘𝑊)
− 𝑁) − 1)
∈ (0..^(♯‘𝑊))) |
5 | 4 | adantl 482 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) →
(((♯‘𝑊) −
𝑁) − 1) ∈
(0..^(♯‘𝑊))) |
6 | | cshwidxmod 14516 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (((♯‘𝑊) − 𝑁) − 1) ∈
(0..^(♯‘𝑊)))
→ ((𝑊 cyclShift 𝑁)‘(((♯‘𝑊) − 𝑁) − 1)) = (𝑊‘(((((♯‘𝑊) − 𝑁) − 1) + 𝑁) mod (♯‘𝑊)))) |
7 | 1, 3, 5, 6 | syl3anc 1370 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘(((♯‘𝑊) − 𝑁) − 1)) = (𝑊‘(((((♯‘𝑊) − 𝑁) − 1) + 𝑁) mod (♯‘𝑊)))) |
8 | | elfzoel2 13386 |
. . . . . . . 8
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
→ (♯‘𝑊)
∈ ℤ) |
9 | 8 | zcnd 12427 |
. . . . . . 7
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
→ (♯‘𝑊)
∈ ℂ) |
10 | 2 | zcnd 12427 |
. . . . . . 7
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
→ 𝑁 ∈
ℂ) |
11 | | 1cnd 10970 |
. . . . . . 7
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
→ 1 ∈ ℂ) |
12 | | nnpcan 11244 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℂ ∧ 𝑁
∈ ℂ ∧ 1 ∈ ℂ) → ((((♯‘𝑊) − 𝑁) − 1) + 𝑁) = ((♯‘𝑊) − 1)) |
13 | 9, 10, 11, 12 | syl3anc 1370 |
. . . . . 6
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
→ ((((♯‘𝑊)
− 𝑁) − 1) +
𝑁) = ((♯‘𝑊) − 1)) |
14 | 13 | oveq1d 7290 |
. . . . 5
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
→ (((((♯‘𝑊) − 𝑁) − 1) + 𝑁) mod (♯‘𝑊)) = (((♯‘𝑊) − 1) mod (♯‘𝑊))) |
15 | 14 | adantl 482 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) →
(((((♯‘𝑊)
− 𝑁) − 1) +
𝑁) mod (♯‘𝑊)) = (((♯‘𝑊) − 1) mod
(♯‘𝑊))) |
16 | | elfzo0 13428 |
. . . . . . . 8
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
↔ (𝑁 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝑁 < (♯‘𝑊))) |
17 | | nnre 11980 |
. . . . . . . . . . 11
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ∈ ℝ) |
18 | | peano2rem 11288 |
. . . . . . . . . . 11
⊢
((♯‘𝑊)
∈ ℝ → ((♯‘𝑊) − 1) ∈
ℝ) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ → ((♯‘𝑊) − 1) ∈
ℝ) |
20 | | nnrp 12741 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ∈
ℝ+) |
21 | 19, 20 | jca 512 |
. . . . . . . . 9
⊢
((♯‘𝑊)
∈ ℕ → (((♯‘𝑊) − 1) ∈ ℝ ∧
(♯‘𝑊) ∈
ℝ+)) |
22 | 21 | 3ad2ant2 1133 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝑁 <
(♯‘𝑊)) →
(((♯‘𝑊) −
1) ∈ ℝ ∧ (♯‘𝑊) ∈
ℝ+)) |
23 | 16, 22 | sylbi 216 |
. . . . . . 7
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
→ (((♯‘𝑊)
− 1) ∈ ℝ ∧ (♯‘𝑊) ∈
ℝ+)) |
24 | | nnm1ge0 12388 |
. . . . . . . . 9
⊢
((♯‘𝑊)
∈ ℕ → 0 ≤ ((♯‘𝑊) − 1)) |
25 | 24 | 3ad2ant2 1133 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝑁 <
(♯‘𝑊)) → 0
≤ ((♯‘𝑊)
− 1)) |
26 | 16, 25 | sylbi 216 |
. . . . . . 7
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
→ 0 ≤ ((♯‘𝑊) − 1)) |
27 | | zre 12323 |
. . . . . . . . 9
⊢
((♯‘𝑊)
∈ ℤ → (♯‘𝑊) ∈ ℝ) |
28 | 27 | ltm1d 11907 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℤ → ((♯‘𝑊) − 1) < (♯‘𝑊)) |
29 | 8, 28 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
→ ((♯‘𝑊)
− 1) < (♯‘𝑊)) |
30 | 23, 26, 29 | jca32 516 |
. . . . . 6
⊢ (𝑁 ∈
(0..^(♯‘𝑊))
→ ((((♯‘𝑊)
− 1) ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ+) ∧ (0 ≤
((♯‘𝑊) −
1) ∧ ((♯‘𝑊)
− 1) < (♯‘𝑊)))) |
31 | 30 | adantl 482 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) →
((((♯‘𝑊)
− 1) ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ+) ∧ (0 ≤
((♯‘𝑊) −
1) ∧ ((♯‘𝑊)
− 1) < (♯‘𝑊)))) |
32 | | modid 13616 |
. . . . 5
⊢
(((((♯‘𝑊) − 1) ∈ ℝ ∧
(♯‘𝑊) ∈
ℝ+) ∧ (0 ≤ ((♯‘𝑊) − 1) ∧ ((♯‘𝑊) − 1) <
(♯‘𝑊))) →
(((♯‘𝑊) −
1) mod (♯‘𝑊)) =
((♯‘𝑊) −
1)) |
33 | 31, 32 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) →
(((♯‘𝑊) −
1) mod (♯‘𝑊)) =
((♯‘𝑊) −
1)) |
34 | 15, 33 | eqtrd 2778 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) →
(((((♯‘𝑊)
− 𝑁) − 1) +
𝑁) mod (♯‘𝑊)) = ((♯‘𝑊) − 1)) |
35 | 34 | fveq2d 6778 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) → (𝑊‘(((((♯‘𝑊) − 𝑁) − 1) + 𝑁) mod (♯‘𝑊))) = (𝑊‘((♯‘𝑊) − 1))) |
36 | 7, 35 | eqtrd 2778 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘(((♯‘𝑊) − 𝑁) − 1)) = (𝑊‘((♯‘𝑊) − 1))) |