Proof of Theorem crctcshwlkn0lem6
Step | Hyp | Ref
| Expression |
1 | | oveq1 7171 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1)) |
2 | | 0p1e1 11831 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
3 | 1, 2 | eqtrdi 2789 |
. . . . . . . 8
⊢ (𝑖 = 0 → (𝑖 + 1) = 1) |
4 | | wkslem2 27542 |
. . . . . . . 8
⊢ ((𝑖 = 0 ∧ (𝑖 + 1) = 1) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))) |
5 | 3, 4 | mpdan 687 |
. . . . . . 7
⊢ (𝑖 = 0 → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))) |
6 | | crctcshwlkn0lem.p |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) |
7 | | crctcshwlkn0lem.s |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) |
8 | | elfzo1 13171 |
. . . . . . . . . 10
⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) |
9 | | simp2 1138 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ∈ ℕ) |
10 | 8, 9 | sylbi 220 |
. . . . . . . . 9
⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℕ) |
11 | 7, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
12 | | lbfzo0 13161 |
. . . . . . . 8
⊢ (0 ∈
(0..^𝑁) ↔ 𝑁 ∈
ℕ) |
13 | 11, 12 | sylibr 237 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ (0..^𝑁)) |
14 | 5, 6, 13 | rspcdva 3526 |
. . . . . 6
⊢ (𝜑 → if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))) |
15 | | crctcshwlkn0lem.e |
. . . . . . 7
⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0)) |
16 | | eqeq1 2742 |
. . . . . . . 8
⊢ ((𝑃‘𝑁) = (𝑃‘0) → ((𝑃‘𝑁) = (𝑃‘1) ↔ (𝑃‘0) = (𝑃‘1))) |
17 | | sneq 4523 |
. . . . . . . . 9
⊢ ((𝑃‘𝑁) = (𝑃‘0) → {(𝑃‘𝑁)} = {(𝑃‘0)}) |
18 | 17 | eqeq2d 2749 |
. . . . . . . 8
⊢ ((𝑃‘𝑁) = (𝑃‘0) → ((𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘0)})) |
19 | | preq1 4621 |
. . . . . . . . 9
⊢ ((𝑃‘𝑁) = (𝑃‘0) → {(𝑃‘𝑁), (𝑃‘1)} = {(𝑃‘0), (𝑃‘1)}) |
20 | 19 | sseq1d 3906 |
. . . . . . . 8
⊢ ((𝑃‘𝑁) = (𝑃‘0) → ({(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ↔ {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))) |
21 | 16, 18, 20 | ifpbi123d 1079 |
. . . . . . 7
⊢ ((𝑃‘𝑁) = (𝑃‘0) → (if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))) |
22 | 15, 21 | syl 17 |
. . . . . 6
⊢ (𝜑 → (if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))) |
23 | 14, 22 | mpbird 260 |
. . . . 5
⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))) |
24 | | nncn 11717 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
25 | | nncn 11717 |
. . . . . . . . . 10
⊢ (𝑆 ∈ ℕ → 𝑆 ∈
ℂ) |
26 | | npcan 10966 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ) → ((𝑁 − 𝑆) + 𝑆) = 𝑁) |
27 | 24, 25, 26 | syl2anr 600 |
. . . . . . . . 9
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 𝑆) + 𝑆) = 𝑁) |
28 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → ((𝑁 − 𝑆) + 𝑆) = 𝑁) |
29 | | oveq1 7171 |
. . . . . . . . . . 11
⊢ (((𝑁 − 𝑆) + 𝑆) = 𝑁 → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = (𝑁 mod (♯‘𝐹))) |
30 | | crctcshwlkn0lem.n |
. . . . . . . . . . . . . . 15
⊢ 𝑁 = (♯‘𝐹) |
31 | 30 | eqcomi 2747 |
. . . . . . . . . . . . . 14
⊢
(♯‘𝐹) =
𝑁 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(♯‘𝐹) = 𝑁) |
33 | 32 | oveq2d 7180 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod (♯‘𝐹)) = (𝑁 mod 𝑁)) |
34 | | nnrp 12476 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
35 | | modid0 13349 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℝ+
→ (𝑁 mod 𝑁) = 0) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → (𝑁 mod 𝑁) = 0) |
37 | 36 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod 𝑁) = 0) |
38 | 33, 37 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 mod (♯‘𝐹)) = 0) |
39 | 29, 38 | sylan9eqr 2795 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0) |
40 | | simpl 486 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) |
41 | 28, 39, 40 | 3jca 1129 |
. . . . . . . . 9
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((𝑁 − 𝑆) + 𝑆) = 𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ))) |
42 | 27, 41 | mpdan 687 |
. . . . . . . 8
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ))) |
43 | 42 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ))) |
44 | 8, 43 | sylbi 220 |
. . . . . 6
⊢ (𝑆 ∈ (1..^𝑁) → (((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ))) |
45 | | simp1 1137 |
. . . . . . . . 9
⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑁 − 𝑆) + 𝑆) = 𝑁) |
46 | 45 | fveq2d 6672 |
. . . . . . . 8
⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘𝑁)) |
47 | 46 | eqeq1d 2740 |
. . . . . . 7
⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1) ↔ (𝑃‘𝑁) = (𝑃‘1))) |
48 | | simp2 1138 |
. . . . . . . . . 10
⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0) |
49 | 48 | fveq2d 6672 |
. . . . . . . . 9
⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))) = (𝐹‘0)) |
50 | 49 | fveq2d 6672 |
. . . . . . . 8
⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = (𝐼‘(𝐹‘0))) |
51 | 46 | sneqd 4525 |
. . . . . . . 8
⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → {(𝑃‘((𝑁 − 𝑆) + 𝑆))} = {(𝑃‘𝑁)}) |
52 | 50, 51 | eqeq12d 2754 |
. . . . . . 7
⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))} ↔ (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)})) |
53 | 46 | preq1d 4627 |
. . . . . . . 8
⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} = {(𝑃‘𝑁), (𝑃‘1)}) |
54 | 53, 50 | sseq12d 3908 |
. . . . . . 7
⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ({(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) ↔ {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))) |
55 | 47, 52, 54 | ifpbi123d 1079 |
. . . . . 6
⊢ ((((𝑁 − 𝑆) + 𝑆) = 𝑁 ∧ (((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 0 ∧ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))) ↔ if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))) |
56 | 7, 44, 55 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))) ↔ if-((𝑃‘𝑁) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))) |
57 | 23, 56 | mpbird 260 |
. . . 4
⊢ (𝜑 → if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))) |
58 | | nnsub 11753 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 ↔ (𝑁 − 𝑆) ∈ ℕ)) |
59 | 58 | biimp3a 1470 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈ ℕ) |
60 | 59 | nnnn0d 12029 |
. . . . . . . . 9
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈
ℕ0) |
61 | 8, 60 | sylbi 220 |
. . . . . . . 8
⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈
ℕ0) |
62 | 7, 61 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑁 − 𝑆) ∈
ℕ0) |
63 | | nn0fz0 13089 |
. . . . . . 7
⊢ ((𝑁 − 𝑆) ∈ ℕ0 ↔ (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆))) |
64 | 62, 63 | sylib 221 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆))) |
65 | | crctcshwlkn0lem.q |
. . . . . . 7
⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) |
66 | 7, 65 | crctcshwlkn0lem2 27741 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁 − 𝑆) ∈ (0...(𝑁 − 𝑆))) → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆))) |
67 | 64, 66 | mpdan 687 |
. . . . 5
⊢ (𝜑 → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆))) |
68 | | elfzoel2 13121 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℤ) |
69 | | elfzoelz 13122 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ ℤ) |
70 | 68, 69 | zsubcld 12166 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ ℤ) |
71 | 70 | peano2zd 12164 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ∈ ℤ) |
72 | | nnre 11716 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
73 | 72 | anim1i 618 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑆 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈
ℕ)) |
74 | 73 | ancoms 462 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 ∈ ℝ ∧ 𝑆 ∈
ℕ)) |
75 | | crctcshwlkn0lem1 27740 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℕ) → ((𝑁 − 𝑆) + 1) ≤ 𝑁) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 𝑆) + 1) ≤ 𝑁) |
77 | 76 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑁 − 𝑆) + 1) ≤ 𝑁) |
78 | 8, 77 | sylbi 220 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ≤ 𝑁) |
79 | 71, 68, 78 | 3jca 1129 |
. . . . . . . . . 10
⊢ (𝑆 ∈ (1..^𝑁) → (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁)) |
80 | 7, 79 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁)) |
81 | | eluz2 12323 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘((𝑁 − 𝑆) + 1)) ↔ (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑁)) |
82 | 80, 81 | sylibr 237 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘((𝑁 − 𝑆) + 1))) |
83 | | eluzfz1 12998 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘((𝑁 − 𝑆) + 1)) → ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁)) |
84 | 82, 83 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁)) |
85 | 7, 65 | crctcshwlkn0lem3 27742 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑁 − 𝑆) + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁)) → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁))) |
86 | 84, 85 | mpdan 687 |
. . . . . 6
⊢ (𝜑 → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁))) |
87 | | subcl 10956 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑁 − 𝑆) ∈ ℂ) |
88 | 87 | ancoms 462 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑁 − 𝑆) ∈ ℂ) |
89 | | ax-1cn 10666 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
90 | | pncan2 10964 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 − 𝑆) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)) = 1) |
91 | 90 | eqcomd 2744 |
. . . . . . . . . . . . 13
⊢ (((𝑁 − 𝑆) ∈ ℂ ∧ 1 ∈ ℂ)
→ 1 = (((𝑁 −
𝑆) + 1) − (𝑁 − 𝑆))) |
92 | 88, 89, 91 | sylancl 589 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 1 =
(((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆))) |
93 | | peano2cn 10883 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 − 𝑆) ∈ ℂ → ((𝑁 − 𝑆) + 1) ∈ ℂ) |
94 | 88, 93 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑁 − 𝑆) + 1) ∈ ℂ) |
95 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 𝑁 ∈
ℂ) |
96 | | simpl 486 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → 𝑆 ∈
ℂ) |
97 | 94, 95, 96 | subsub3d 11098 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((𝑁 − 𝑆) + 1) − (𝑁 − 𝑆)) = ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)) |
98 | 92, 97 | eqtr2d 2774 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℂ ∧ 𝑁 ∈ ℂ) →
((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1) |
99 | 25, 24, 98 | syl2an 599 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1) |
100 | 99 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1) |
101 | 8, 100 | sylbi 220 |
. . . . . . . 8
⊢ (𝑆 ∈ (1..^𝑁) → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1) |
102 | 7, 101 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁) = 1) |
103 | 102 | fveq2d 6672 |
. . . . . 6
⊢ (𝜑 → (𝑃‘((((𝑁 − 𝑆) + 1) + 𝑆) − 𝑁)) = (𝑃‘1)) |
104 | 86, 103 | eqtrd 2773 |
. . . . 5
⊢ (𝜑 → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1)) |
105 | | crctcshwlkn0lem.h |
. . . . . . 7
⊢ 𝐻 = (𝐹 cyclShift 𝑆) |
106 | 105 | fveq1i 6669 |
. . . . . 6
⊢ (𝐻‘(𝑁 − 𝑆)) = ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) |
107 | | crctcshwlkn0lem.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ Word 𝐴) |
108 | 107 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → 𝐹 ∈ Word 𝐴) |
109 | 69 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → 𝑆 ∈ ℤ) |
110 | | elfzofz 13137 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ (1...𝑁)) |
111 | | ubmelfzo 13186 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (1...𝑁) → (𝑁 − 𝑆) ∈ (0..^𝑁)) |
112 | 110, 111 | syl 17 |
. . . . . . . . . 10
⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈ (0..^𝑁)) |
113 | 112 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → (𝑁 − 𝑆) ∈ (0..^𝑁)) |
114 | 31 | oveq2i 7175 |
. . . . . . . . 9
⊢
(0..^(♯‘𝐹)) = (0..^𝑁) |
115 | 113, 114 | eleqtrrdi 2844 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → (𝑁 − 𝑆) ∈ (0..^(♯‘𝐹))) |
116 | | cshwidxmod 14247 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ (𝑁 − 𝑆) ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) |
117 | 108, 109,
115, 116 | syl3anc 1372 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ∈ (1..^𝑁)) → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) |
118 | 7, 117 | mpdan 687 |
. . . . . 6
⊢ (𝜑 → ((𝐹 cyclShift 𝑆)‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) |
119 | 106, 118 | syl5eq 2785 |
. . . . 5
⊢ (𝜑 → (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) |
120 | | simp1 1137 |
. . . . . . 7
⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆))) |
121 | | simp2 1138 |
. . . . . . 7
⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1)) |
122 | 120, 121 | eqeq12d 2754 |
. . . . . 6
⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)) ↔ (𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1))) |
123 | | simp3 1139 |
. . . . . . . 8
⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) |
124 | 123 | fveq2d 6672 |
. . . . . . 7
⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (𝐼‘(𝐻‘(𝑁 − 𝑆))) = (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))) |
125 | 120 | sneqd 4525 |
. . . . . . 7
⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → {(𝑄‘(𝑁 − 𝑆))} = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}) |
126 | 124, 125 | eqeq12d 2754 |
. . . . . 6
⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ((𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))} ↔ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))})) |
127 | 120, 121 | preq12d 4629 |
. . . . . . 7
⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} = {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)}) |
128 | 127, 124 | sseq12d 3908 |
. . . . . 6
⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → ({(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))) ↔ {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))))) |
129 | 122, 126,
128 | ifpbi123d 1079 |
. . . . 5
⊢ (((𝑄‘(𝑁 − 𝑆)) = (𝑃‘((𝑁 − 𝑆) + 𝑆)) ∧ (𝑄‘((𝑁 − 𝑆) + 1)) = (𝑃‘1) ∧ (𝐻‘(𝑁 − 𝑆)) = (𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) → (if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))) ↔ if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))))) |
130 | 67, 104, 119, 129 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))) ↔ if-((𝑃‘((𝑁 − 𝑆) + 𝑆)) = (𝑃‘1), (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹)))) = {(𝑃‘((𝑁 − 𝑆) + 𝑆))}, {(𝑃‘((𝑁 − 𝑆) + 𝑆)), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘(((𝑁 − 𝑆) + 𝑆) mod (♯‘𝐹))))))) |
131 | 57, 130 | mpbird 260 |
. . 3
⊢ (𝜑 → if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))) |
132 | 131 | adantr 484 |
. 2
⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆))))) |
133 | | wkslem1 27541 |
. . 3
⊢ (𝐽 = (𝑁 − 𝑆) → (if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))) ↔ if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))))) |
134 | 133 | adantl 485 |
. 2
⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → (if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽))) ↔ if-((𝑄‘(𝑁 − 𝑆)) = (𝑄‘((𝑁 − 𝑆) + 1)), (𝐼‘(𝐻‘(𝑁 − 𝑆))) = {(𝑄‘(𝑁 − 𝑆))}, {(𝑄‘(𝑁 − 𝑆)), (𝑄‘((𝑁 − 𝑆) + 1))} ⊆ (𝐼‘(𝐻‘(𝑁 − 𝑆)))))) |
135 | 132, 134 | mpbird 260 |
1
⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽)))) |