Proof of Theorem crctcshwlkn0lem7
| Step | Hyp | Ref
| Expression |
| 1 | | crctcshwlkn0lem.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) |
| 2 | | crctcshwlkn0lem.q |
. . . . . 6
⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) |
| 3 | | crctcshwlkn0lem.h |
. . . . . 6
⊢ 𝐻 = (𝐹 cyclShift 𝑆) |
| 4 | | crctcshwlkn0lem.n |
. . . . . 6
⊢ 𝑁 = (♯‘𝐹) |
| 5 | | crctcshwlkn0lem.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ Word 𝐴) |
| 6 | | crctcshwlkn0lem.p |
. . . . . 6
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) |
| 7 | 1, 2, 3, 4, 5, 6 | crctcshwlkn0lem4 29833 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ (0..^(𝑁 − 𝑆))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
| 8 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → (𝑁 − 𝑆) = (𝑁 − 𝑆)) |
| 9 | | crctcshwlkn0lem.e |
. . . . . . . 8
⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0)) |
| 10 | 1, 2, 3, 4, 5, 6, 9 | crctcshwlkn0lem6 29835 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 − 𝑆) = (𝑁 − 𝑆)) → if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))) |
| 11 | 8, 10 | mpdan 687 |
. . . . . 6
⊢ (𝜑 → if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))) |
| 12 | | ovex 7464 |
. . . . . . 7
⊢ (𝑁 − 𝑆) ∈ V |
| 13 | | wkslem1 29625 |
. . . . . . 7
⊢ (𝑗 = (𝑁 − 𝑆) → (if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))))) |
| 14 | 12, 13 | ralsn 4681 |
. . . . . 6
⊢
(∀𝑗 ∈
{(𝑁 − 𝑆)}if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))) |
| 15 | 11, 14 | sylibr 234 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ {(𝑁 − 𝑆)}if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
| 16 | | ralunb 4197 |
. . . . 5
⊢
(∀𝑗 ∈
((0..^(𝑁 − 𝑆)) ∪ {(𝑁 − 𝑆)})if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ (∀𝑗 ∈ (0..^(𝑁 − 𝑆))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ∧ ∀𝑗 ∈ {(𝑁 − 𝑆)}if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
| 17 | 7, 15, 16 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ ((0..^(𝑁 − 𝑆)) ∪ {(𝑁 − 𝑆)})if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
| 18 | | elfzo1 13752 |
. . . . . 6
⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) |
| 19 | | nnz 12634 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 20 | | nnz 12634 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ ℕ → 𝑆 ∈
ℤ) |
| 21 | | zsubcl 12659 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ) |
| 22 | 19, 20, 21 | syl2anr 597 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 − 𝑆) ∈ ℤ) |
| 23 | 22 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈ ℤ) |
| 24 | | nnre 12273 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ ℕ → 𝑆 ∈
ℝ) |
| 25 | | nnre 12273 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 26 | | posdif 11756 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑆 < 𝑁 ↔ 0 < (𝑁 − 𝑆))) |
| 27 | | 0re 11263 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
| 28 | | resubcl 11573 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑁 − 𝑆) ∈ ℝ) |
| 29 | 28 | ancoms 458 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑁 − 𝑆) ∈ ℝ) |
| 30 | | ltle 11349 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ (𝑁
− 𝑆) ∈ ℝ)
→ (0 < (𝑁 −
𝑆) → 0 ≤ (𝑁 − 𝑆))) |
| 31 | 27, 29, 30 | sylancr 587 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 <
(𝑁 − 𝑆) → 0 ≤ (𝑁 − 𝑆))) |
| 32 | 26, 31 | sylbid 240 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑆 < 𝑁 → 0 ≤ (𝑁 − 𝑆))) |
| 33 | 24, 25, 32 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 → 0 ≤ (𝑁 − 𝑆))) |
| 34 | 33 | 3impia 1118 |
. . . . . . . . 9
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 0 ≤ (𝑁 − 𝑆)) |
| 35 | | elnn0z 12626 |
. . . . . . . . 9
⊢ ((𝑁 − 𝑆) ∈ ℕ0 ↔ ((𝑁 − 𝑆) ∈ ℤ ∧ 0 ≤ (𝑁 − 𝑆))) |
| 36 | 23, 34, 35 | sylanbrc 583 |
. . . . . . . 8
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈
ℕ0) |
| 37 | | elnn0uz 12923 |
. . . . . . . 8
⊢ ((𝑁 − 𝑆) ∈ ℕ0 ↔ (𝑁 − 𝑆) ∈
(ℤ≥‘0)) |
| 38 | 36, 37 | sylib 218 |
. . . . . . 7
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈
(ℤ≥‘0)) |
| 39 | | fzosplitsn 13814 |
. . . . . . 7
⊢ ((𝑁 − 𝑆) ∈ (ℤ≥‘0)
→ (0..^((𝑁 −
𝑆) + 1)) = ((0..^(𝑁 − 𝑆)) ∪ {(𝑁 − 𝑆)})) |
| 40 | 38, 39 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (0..^((𝑁 − 𝑆) + 1)) = ((0..^(𝑁 − 𝑆)) ∪ {(𝑁 − 𝑆)})) |
| 41 | 18, 40 | sylbi 217 |
. . . . 5
⊢ (𝑆 ∈ (1..^𝑁) → (0..^((𝑁 − 𝑆) + 1)) = ((0..^(𝑁 − 𝑆)) ∪ {(𝑁 − 𝑆)})) |
| 42 | 1, 41 | syl 17 |
. . . 4
⊢ (𝜑 → (0..^((𝑁 − 𝑆) + 1)) = ((0..^(𝑁 − 𝑆)) ∪ {(𝑁 − 𝑆)})) |
| 43 | 17, 42 | raleqtrrdv 3330 |
. . 3
⊢ (𝜑 → ∀𝑗 ∈ (0..^((𝑁 − 𝑆) + 1))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
| 44 | 1, 2, 3, 4, 5, 6 | crctcshwlkn0lem5 29834 |
. . 3
⊢ (𝜑 → ∀𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
| 45 | | ralunb 4197 |
. . 3
⊢
(∀𝑗 ∈
((0..^((𝑁 − 𝑆) + 1)) ∪ (((𝑁 − 𝑆) + 1)..^𝑁))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ (∀𝑗 ∈ (0..^((𝑁 − 𝑆) + 1))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ∧ ∀𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
| 46 | 43, 44, 45 | sylanbrc 583 |
. 2
⊢ (𝜑 → ∀𝑗 ∈ ((0..^((𝑁 − 𝑆) + 1)) ∪ (((𝑁 − 𝑆) + 1)..^𝑁))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
| 47 | | nnsub 12310 |
. . . . . . 7
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 ↔ (𝑁 − 𝑆) ∈ ℕ)) |
| 48 | 47 | biimp3a 1471 |
. . . . . 6
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈ ℕ) |
| 49 | | nnnn0 12533 |
. . . . . 6
⊢ ((𝑁 − 𝑆) ∈ ℕ → (𝑁 − 𝑆) ∈
ℕ0) |
| 50 | | peano2nn0 12566 |
. . . . . 6
⊢ ((𝑁 − 𝑆) ∈ ℕ0 → ((𝑁 − 𝑆) + 1) ∈
ℕ0) |
| 51 | 48, 49, 50 | 3syl 18 |
. . . . 5
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑁 − 𝑆) + 1) ∈
ℕ0) |
| 52 | | nnnn0 12533 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 53 | 52 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ∈
ℕ0) |
| 54 | 25 | anim1i 615 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈
ℕ)) |
| 55 | 54 | ancoms 458 |
. . . . . . 7
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈
ℕ)) |
| 56 | | crctcshwlkn0lem1 29830 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ) → ((𝑁 − 𝑆) + 1) ≤ 𝑁) |
| 57 | 55, 56 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 𝑆) + 1) ≤ 𝑁) |
| 58 | 57 | 3adant3 1133 |
. . . . 5
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑁 − 𝑆) + 1) ≤ 𝑁) |
| 59 | | elfz2nn0 13658 |
. . . . 5
⊢ (((𝑁 − 𝑆) + 1) ∈ (0...𝑁) ↔ (((𝑁 − 𝑆) + 1) ∈ ℕ0 ∧
𝑁 ∈
ℕ0 ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁)) |
| 60 | 51, 53, 58, 59 | syl3anbrc 1344 |
. . . 4
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑁 − 𝑆) + 1) ∈ (0...𝑁)) |
| 61 | 18, 60 | sylbi 217 |
. . 3
⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ∈ (0...𝑁)) |
| 62 | | fzosplit 13732 |
. . 3
⊢ (((𝑁 − 𝑆) + 1) ∈ (0...𝑁) → (0..^𝑁) = ((0..^((𝑁 − 𝑆) + 1)) ∪ (((𝑁 − 𝑆) + 1)..^𝑁))) |
| 63 | 1, 61, 62 | 3syl 18 |
. 2
⊢ (𝜑 → (0..^𝑁) = ((0..^((𝑁 − 𝑆) + 1)) ∪ (((𝑁 − 𝑆) + 1)..^𝑁))) |
| 64 | 46, 63 | raleqtrrdv 3330 |
1
⊢ (𝜑 → ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |