Proof of Theorem cshwshashlem2
Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . . . . . 8
⊢ ((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) → ((𝑊 cyclShift 𝐿) cyclShift ((#‘𝑊) − 𝐿)) = ((𝑊 cyclShift 𝐾) cyclShift ((#‘𝑊) − 𝐿))) |
2 | 1 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) → ((𝑊 cyclShift 𝐾) cyclShift ((#‘𝑊) − 𝐿)) = ((𝑊 cyclShift 𝐿) cyclShift ((#‘𝑊) − 𝐿))) |
3 | 2 | ad2antrr 758 |
. . . . . 6
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → ((𝑊 cyclShift 𝐾) cyclShift ((#‘𝑊) − 𝐿)) = ((𝑊 cyclShift 𝐿) cyclShift ((#‘𝑊) − 𝐿))) |
4 | | cshwshash.0 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) ∈ ℙ)) |
5 | 4 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ Word 𝑉) |
6 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → 𝑊 ∈ Word 𝑉) |
7 | 6 | adantl 481 |
. . . . . . . 8
⊢ (((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) → 𝑊 ∈ Word 𝑉) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → 𝑊 ∈ Word 𝑉) |
9 | | elfzofz 12354 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0..^(#‘𝑊)) → 𝐾 ∈ (0...(#‘𝑊))) |
10 | 9 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → 𝐾 ∈ (0...(#‘𝑊))) |
11 | 10 | adantl 481 |
. . . . . . 7
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → 𝐾 ∈ (0...(#‘𝑊))) |
12 | | elfzofz 12354 |
. . . . . . . . . 10
⊢ (𝐿 ∈ (0..^(#‘𝑊)) → 𝐿 ∈ (0...(#‘𝑊))) |
13 | | fznn0sub2 12315 |
. . . . . . . . . 10
⊢ (𝐿 ∈ (0...(#‘𝑊)) → ((#‘𝑊) − 𝐿) ∈ (0...(#‘𝑊))) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝐿 ∈ (0..^(#‘𝑊)) → ((#‘𝑊) − 𝐿) ∈ (0...(#‘𝑊))) |
15 | 14 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → ((#‘𝑊) − 𝐿) ∈ (0...(#‘𝑊))) |
16 | 15 | adantl 481 |
. . . . . . 7
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → ((#‘𝑊) − 𝐿) ∈ (0...(#‘𝑊))) |
17 | | elfzo0 12376 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ (0..^(#‘𝑊)) ↔ (𝐿 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝐿 < (#‘𝑊))) |
18 | | elfzoelz 12339 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ (0..^(#‘𝑊)) → 𝐾 ∈ ℤ) |
19 | | zre 11258 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ)) → 𝐾 ∈
ℝ) |
21 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℝ) |
22 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) |
23 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝑊) ∈
ℝ ∧ 𝐿 ∈
ℝ) → ((#‘𝑊) − 𝐿) ∈ ℝ) |
24 | 21, 22, 23 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) → ((#‘𝑊) − 𝐿) ∈ ℝ) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ)) → ((#‘𝑊) − 𝐿) ∈ ℝ) |
26 | 20, 25 | readdcld 9948 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ)) → (𝐾 +
((#‘𝑊) − 𝐿)) ∈
ℝ) |
27 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) → (#‘𝑊)
∈ ℝ) |
28 | 27 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ)) → (#‘𝑊) ∈ ℝ) |
29 | 26, 28 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ)) → ((𝐾 +
((#‘𝑊) − 𝐿)) ∈ ℝ ∧
(#‘𝑊) ∈
ℝ)) |
30 | 29 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℤ → ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) → ((𝐾 +
((#‘𝑊) − 𝐿)) ∈ ℝ ∧
(#‘𝑊) ∈
ℝ))) |
31 | 18, 30 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (0..^(#‘𝑊)) → ((𝐿 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ)
→ ((𝐾 +
((#‘𝑊) − 𝐿)) ∈ ℝ ∧
(#‘𝑊) ∈
ℝ))) |
32 | 31 | com12 32 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) → (𝐾 ∈
(0..^(#‘𝑊)) →
((𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℝ ∧ (#‘𝑊) ∈
ℝ))) |
33 | 32 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ 𝐿 <
(#‘𝑊)) → (𝐾 ∈ (0..^(#‘𝑊)) → ((𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℝ ∧ (#‘𝑊) ∈
ℝ))) |
34 | 17, 33 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (0..^(#‘𝑊)) → (𝐾 ∈ (0..^(#‘𝑊)) → ((𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℝ ∧ (#‘𝑊) ∈
ℝ))) |
35 | 34 | imp 444 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊))) → ((𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℝ ∧ (#‘𝑊) ∈
ℝ)) |
36 | 35 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → ((𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℝ ∧ (#‘𝑊) ∈
ℝ)) |
37 | | fzonmapblen 12381 |
. . . . . . . . 9
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → (𝐾 + ((#‘𝑊) − 𝐿)) < (#‘𝑊)) |
38 | | ltle 10005 |
. . . . . . . . 9
⊢ (((𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → ((𝐾 + ((#‘𝑊) − 𝐿)) < (#‘𝑊) → (𝐾 + ((#‘𝑊) − 𝐿)) ≤ (#‘𝑊))) |
39 | 36, 37, 38 | sylc 63 |
. . . . . . . 8
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → (𝐾 + ((#‘𝑊) − 𝐿)) ≤ (#‘𝑊)) |
40 | 39 | adantl 481 |
. . . . . . 7
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → (𝐾 + ((#‘𝑊) − 𝐿)) ≤ (#‘𝑊)) |
41 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐾 ∈ (0...(#‘𝑊)) ∧ ((#‘𝑊) − 𝐿) ∈ (0...(#‘𝑊)) ∧ (𝐾 + ((#‘𝑊) − 𝐿)) ≤ (#‘𝑊))) → 𝑊 ∈ Word 𝑉) |
42 | | elfzelz 12213 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (0...(#‘𝑊)) → 𝐾 ∈ ℤ) |
43 | 42 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝐾 ∈ (0...(#‘𝑊)) ∧ ((#‘𝑊) − 𝐿) ∈ (0...(#‘𝑊)) ∧ (𝐾 + ((#‘𝑊) − 𝐿)) ≤ (#‘𝑊)) → 𝐾 ∈ ℤ) |
44 | 43 | adantl 481 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐾 ∈ (0...(#‘𝑊)) ∧ ((#‘𝑊) − 𝐿) ∈ (0...(#‘𝑊)) ∧ (𝐾 + ((#‘𝑊) − 𝐿)) ≤ (#‘𝑊))) → 𝐾 ∈ ℤ) |
45 | | elfzelz 12213 |
. . . . . . . . . 10
⊢
(((#‘𝑊)
− 𝐿) ∈
(0...(#‘𝑊)) →
((#‘𝑊) − 𝐿) ∈
ℤ) |
46 | 45 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝐾 ∈ (0...(#‘𝑊)) ∧ ((#‘𝑊) − 𝐿) ∈ (0...(#‘𝑊)) ∧ (𝐾 + ((#‘𝑊) − 𝐿)) ≤ (#‘𝑊)) → ((#‘𝑊) − 𝐿) ∈ ℤ) |
47 | 46 | adantl 481 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐾 ∈ (0...(#‘𝑊)) ∧ ((#‘𝑊) − 𝐿) ∈ (0...(#‘𝑊)) ∧ (𝐾 + ((#‘𝑊) − 𝐿)) ≤ (#‘𝑊))) → ((#‘𝑊) − 𝐿) ∈ ℤ) |
48 | | 2cshw 13410 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐾 ∈ ℤ ∧ ((#‘𝑊) − 𝐿) ∈ ℤ) → ((𝑊 cyclShift 𝐾) cyclShift ((#‘𝑊) − 𝐿)) = (𝑊 cyclShift (𝐾 + ((#‘𝑊) − 𝐿)))) |
49 | 41, 44, 47, 48 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐾 ∈ (0...(#‘𝑊)) ∧ ((#‘𝑊) − 𝐿) ∈ (0...(#‘𝑊)) ∧ (𝐾 + ((#‘𝑊) − 𝐿)) ≤ (#‘𝑊))) → ((𝑊 cyclShift 𝐾) cyclShift ((#‘𝑊) − 𝐿)) = (𝑊 cyclShift (𝐾 + ((#‘𝑊) − 𝐿)))) |
50 | 8, 11, 16, 40, 49 | syl13anc 1320 |
. . . . . 6
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → ((𝑊 cyclShift 𝐾) cyclShift ((#‘𝑊) − 𝐿)) = (𝑊 cyclShift (𝐾 + ((#‘𝑊) − 𝐿)))) |
51 | 12 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → 𝐿 ∈ (0...(#‘𝑊))) |
52 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝐿 ∈ (0...(#‘𝑊)) → 𝐿 ∈ ℤ) |
53 | | 2cshwid 13411 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → ((𝑊 cyclShift 𝐿) cyclShift ((#‘𝑊) − 𝐿)) = 𝑊) |
54 | 52, 53 | sylan2 490 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑊))) → ((𝑊 cyclShift 𝐿) cyclShift ((#‘𝑊) − 𝐿)) = 𝑊) |
55 | 7, 51, 54 | syl2an 493 |
. . . . . 6
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → ((𝑊 cyclShift 𝐿) cyclShift ((#‘𝑊) − 𝐿)) = 𝑊) |
56 | 3, 50, 55 | 3eqtr3d 2652 |
. . . . 5
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → (𝑊 cyclShift (𝐾 + ((#‘𝑊) − 𝐿))) = 𝑊) |
57 | | simplrl 796 |
. . . . . 6
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → 𝜑) |
58 | | simplrr 797 |
. . . . . 6
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) |
59 | | 3simpa 1051 |
. . . . . . . . . . . 12
⊢ ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ 𝐿 <
(#‘𝑊)) → (𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ)) |
60 | 17, 59 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (0..^(#‘𝑊)) → (𝐿 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ)) |
61 | | nnz 11276 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℤ) |
62 | | nn0z 11277 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℤ) |
63 | | zsubcl 11296 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝑊) ∈
ℤ ∧ 𝐿 ∈
ℤ) → ((#‘𝑊) − 𝐿) ∈ ℤ) |
64 | 61, 62, 63 | syl2anr 494 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) → ((#‘𝑊) − 𝐿) ∈ ℤ) |
65 | 64 | anim2i 591 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ)) → (𝐾 ∈
ℤ ∧ ((#‘𝑊)
− 𝐿) ∈
ℤ)) |
66 | 65 | ancoms 468 |
. . . . . . . . . . . 12
⊢ (((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ 𝐾 ∈
ℤ) → (𝐾 ∈
ℤ ∧ ((#‘𝑊)
− 𝐿) ∈
ℤ)) |
67 | | zaddcl 11294 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℤ ∧
((#‘𝑊) − 𝐿) ∈ ℤ) → (𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℤ) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) ∧ 𝐾 ∈
ℤ) → (𝐾 +
((#‘𝑊) − 𝐿)) ∈
ℤ) |
69 | 60, 18, 68 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊))) → (𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℤ) |
70 | 69 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → (𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℤ) |
71 | | elfzo0 12376 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (0..^(#‘𝑊)) ↔ (𝐾 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝐾 < (#‘𝑊))) |
72 | | elnn0z 11267 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℤ
∧ 0 ≤ 𝐾)) |
73 | 19 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) ∧ (𝐿 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝐿 < (#‘𝑊))) → 𝐾 ∈ ℝ) |
74 | 24 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ 𝐿 <
(#‘𝑊)) →
((#‘𝑊) − 𝐿) ∈
ℝ) |
75 | 74 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) ∧ (𝐿 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝐿 < (#‘𝑊))) → ((#‘𝑊) − 𝐿) ∈ ℝ) |
76 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) ∧ (𝐿 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝐿 < (#‘𝑊))) → 0 ≤ 𝐾) |
77 | | posdif 10400 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐿 ∈ ℝ ∧
(#‘𝑊) ∈ ℝ)
→ (𝐿 <
(#‘𝑊) ↔ 0 <
((#‘𝑊) − 𝐿))) |
78 | 22, 21, 77 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ) → (𝐿 <
(#‘𝑊) ↔ 0 <
((#‘𝑊) − 𝐿))) |
79 | 78 | biimp3a 1424 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ 𝐿 <
(#‘𝑊)) → 0 <
((#‘𝑊) − 𝐿)) |
80 | 79 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) ∧ (𝐿 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝐿 < (#‘𝑊))) → 0 <
((#‘𝑊) − 𝐿)) |
81 | 73, 75, 76, 80 | addgegt0d 10480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) ∧ (𝐿 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝐿 < (#‘𝑊))) → 0 < (𝐾 + ((#‘𝑊) − 𝐿))) |
82 | 81 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) → ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ 𝐿 <
(#‘𝑊)) → 0 <
(𝐾 + ((#‘𝑊) − 𝐿)))) |
83 | 72, 82 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℕ0
→ ((𝐿 ∈
ℕ0 ∧ (#‘𝑊) ∈ ℕ ∧ 𝐿 < (#‘𝑊)) → 0 < (𝐾 + ((#‘𝑊) − 𝐿)))) |
84 | 83 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ 𝐾 <
(#‘𝑊)) → ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ 𝐿 <
(#‘𝑊)) → 0 <
(𝐾 + ((#‘𝑊) − 𝐿)))) |
85 | 71, 84 | sylbi 206 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ (0..^(#‘𝑊)) → ((𝐿 ∈ ℕ0 ∧
(#‘𝑊) ∈ ℕ
∧ 𝐿 < (#‘𝑊)) → 0 < (𝐾 + ((#‘𝑊) − 𝐿)))) |
86 | 85 | com12 32 |
. . . . . . . . . . . 12
⊢ ((𝐿 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ 𝐿 <
(#‘𝑊)) → (𝐾 ∈ (0..^(#‘𝑊)) → 0 < (𝐾 + ((#‘𝑊) − 𝐿)))) |
87 | 17, 86 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (0..^(#‘𝑊)) → (𝐾 ∈ (0..^(#‘𝑊)) → 0 < (𝐾 + ((#‘𝑊) − 𝐿)))) |
88 | 87 | imp 444 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊))) → 0 < (𝐾 + ((#‘𝑊) − 𝐿))) |
89 | 88 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → 0 < (𝐾 + ((#‘𝑊) − 𝐿))) |
90 | | elnnz 11264 |
. . . . . . . . 9
⊢ ((𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℕ ↔ ((𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℤ ∧ 0 < (𝐾 + ((#‘𝑊) − 𝐿)))) |
91 | 70, 89, 90 | sylanbrc 695 |
. . . . . . . 8
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → (𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℕ) |
92 | 17 | simp2bi 1070 |
. . . . . . . . 9
⊢ (𝐿 ∈ (0..^(#‘𝑊)) → (#‘𝑊) ∈
ℕ) |
93 | 92 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → (#‘𝑊) ∈ ℕ) |
94 | | elfzo1 12385 |
. . . . . . . 8
⊢ ((𝐾 + ((#‘𝑊) − 𝐿)) ∈ (1..^(#‘𝑊)) ↔ ((𝐾 + ((#‘𝑊) − 𝐿)) ∈ ℕ ∧ (#‘𝑊) ∈ ℕ ∧ (𝐾 + ((#‘𝑊) − 𝐿)) < (#‘𝑊))) |
95 | 91, 93, 37, 94 | syl3anbrc 1239 |
. . . . . . 7
⊢ ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → (𝐾 + ((#‘𝑊) − 𝐿)) ∈ (1..^(#‘𝑊))) |
96 | 95 | adantl 481 |
. . . . . 6
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → (𝐾 + ((#‘𝑊) − 𝐿)) ∈ (1..^(#‘𝑊))) |
97 | 4 | cshwshashlem1 15640 |
. . . . . 6
⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ (𝐾 + ((#‘𝑊) − 𝐿)) ∈ (1..^(#‘𝑊))) → (𝑊 cyclShift (𝐾 + ((#‘𝑊) − 𝐿))) ≠ 𝑊) |
98 | 57, 58, 96, 97 | syl3anc 1318 |
. . . . 5
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → (𝑊 cyclShift (𝐾 + ((#‘𝑊) − 𝐿))) ≠ 𝑊) |
99 | 56, 98 | pm2.21ddne 2866 |
. . . 4
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿)) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾)) |
100 | 99 | ex 449 |
. . 3
⊢ (((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) → ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾))) |
101 | 100 | ex 449 |
. 2
⊢ ((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) → ((𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾)))) |
102 | | 2a1 28 |
. 2
⊢ ((𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾) → ((𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾)))) |
103 | 101, 102 | pm2.61ine 2865 |
1
⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → ((𝐿 ∈ (0..^(#‘𝑊)) ∧ 𝐾 ∈ (0..^(#‘𝑊)) ∧ 𝐾 < 𝐿) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾))) |