Proof of Theorem cshwshashlem2
Step | Hyp | Ref
| Expression |
1 | | oveq1 6816 |
. . . . . . . 8
⊢ ((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) → ((𝑊 cyclShift 𝐿) cyclShift ((♯‘𝑊) − 𝐿)) = ((𝑊 cyclShift 𝐾) cyclShift ((♯‘𝑊) − 𝐿))) |
2 | 1 | eqcomd 2762 |
. . . . . . 7
⊢ ((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) → ((𝑊 cyclShift 𝐾) cyclShift ((♯‘𝑊) − 𝐿)) = ((𝑊 cyclShift 𝐿) cyclShift ((♯‘𝑊) − 𝐿))) |
3 | 2 | ad2antrr 764 |
. . . . . 6
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → ((𝑊 cyclShift 𝐾) cyclShift ((♯‘𝑊) − 𝐿)) = ((𝑊 cyclShift 𝐿) cyclShift ((♯‘𝑊) − 𝐿))) |
4 | | cshwshash.0 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ)) |
5 | 4 | simpld 477 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ Word 𝑉) |
6 | 5 | adantr 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → 𝑊 ∈ Word 𝑉) |
7 | 6 | adantl 473 |
. . . . . . . 8
⊢ (((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) → 𝑊 ∈ Word 𝑉) |
8 | 7 | adantr 472 |
. . . . . . 7
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → 𝑊 ∈ Word 𝑉) |
9 | | elfzofz 12675 |
. . . . . . . . 9
⊢ (𝐾 ∈
(0..^(♯‘𝑊))
→ 𝐾 ∈
(0...(♯‘𝑊))) |
10 | 9 | 3ad2ant2 1129 |
. . . . . . . 8
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊))
∧ 𝐾 < 𝐿) → 𝐾 ∈ (0...(♯‘𝑊))) |
11 | 10 | adantl 473 |
. . . . . . 7
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → 𝐾 ∈ (0...(♯‘𝑊))) |
12 | | elfzofz 12675 |
. . . . . . . . . 10
⊢ (𝐿 ∈
(0..^(♯‘𝑊))
→ 𝐿 ∈
(0...(♯‘𝑊))) |
13 | | fznn0sub2 12636 |
. . . . . . . . . 10
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ ((♯‘𝑊)
− 𝐿) ∈
(0...(♯‘𝑊))) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝐿 ∈
(0..^(♯‘𝑊))
→ ((♯‘𝑊)
− 𝐿) ∈
(0...(♯‘𝑊))) |
15 | 14 | 3ad2ant1 1128 |
. . . . . . . 8
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊))
∧ 𝐾 < 𝐿) → ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊))) |
16 | 15 | adantl 473 |
. . . . . . 7
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊))) |
17 | | elfzo0 12699 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈
(0..^(♯‘𝑊))
↔ (𝐿 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐿 < (♯‘𝑊))) |
18 | | zre 11569 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
19 | 18 | adantr 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ)) → 𝐾
∈ ℝ) |
20 | | nnre 11215 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ∈ ℝ) |
21 | | nn0re 11489 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) |
22 | | resubcl 10533 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑊)
∈ ℝ ∧ 𝐿
∈ ℝ) → ((♯‘𝑊) − 𝐿) ∈ ℝ) |
23 | 20, 21, 22 | syl2anr 496 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) → ((♯‘𝑊) − 𝐿) ∈ ℝ) |
24 | 23 | adantl 473 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ)) → ((♯‘𝑊) − 𝐿) ∈ ℝ) |
25 | 19, 24 | readdcld 10257 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ)) → (𝐾
+ ((♯‘𝑊)
− 𝐿)) ∈
ℝ) |
26 | 20 | adantl 473 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) → (♯‘𝑊) ∈ ℝ) |
27 | 26 | adantl 473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ)) → (♯‘𝑊) ∈ ℝ) |
28 | 25, 27 | jca 555 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ)) → ((𝐾
+ ((♯‘𝑊)
− 𝐿)) ∈ ℝ
∧ (♯‘𝑊)
∈ ℝ)) |
29 | 28 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℤ → ((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) → ((𝐾
+ ((♯‘𝑊)
− 𝐿)) ∈ ℝ
∧ (♯‘𝑊)
∈ ℝ))) |
30 | | elfzoelz 12660 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈
(0..^(♯‘𝑊))
→ 𝐾 ∈
ℤ) |
31 | 29, 30 | syl11 33 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) → (𝐾
∈ (0..^(♯‘𝑊)) → ((𝐾 + ((♯‘𝑊) − 𝐿)) ∈ ℝ ∧ (♯‘𝑊) ∈
ℝ))) |
32 | 31 | 3adant3 1127 |
. . . . . . . . . . . 12
⊢ ((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐿 <
(♯‘𝑊)) →
(𝐾 ∈
(0..^(♯‘𝑊))
→ ((𝐾 +
((♯‘𝑊) −
𝐿)) ∈ ℝ ∧
(♯‘𝑊) ∈
ℝ))) |
33 | 17, 32 | sylbi 207 |
. . . . . . . . . . 11
⊢ (𝐿 ∈
(0..^(♯‘𝑊))
→ (𝐾 ∈
(0..^(♯‘𝑊))
→ ((𝐾 +
((♯‘𝑊) −
𝐿)) ∈ ℝ ∧
(♯‘𝑊) ∈
ℝ))) |
34 | 33 | imp 444 |
. . . . . . . . . 10
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊)))
→ ((𝐾 +
((♯‘𝑊) −
𝐿)) ∈ ℝ ∧
(♯‘𝑊) ∈
ℝ)) |
35 | 34 | 3adant3 1127 |
. . . . . . . . 9
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊))
∧ 𝐾 < 𝐿) → ((𝐾 + ((♯‘𝑊) − 𝐿)) ∈ ℝ ∧ (♯‘𝑊) ∈
ℝ)) |
36 | | fzonmapblen 12704 |
. . . . . . . . 9
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊))
∧ 𝐾 < 𝐿) → (𝐾 + ((♯‘𝑊) − 𝐿)) < (♯‘𝑊)) |
37 | | ltle 10314 |
. . . . . . . . 9
⊢ (((𝐾 + ((♯‘𝑊) − 𝐿)) ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ) → ((𝐾 + ((♯‘𝑊) − 𝐿)) < (♯‘𝑊) → (𝐾 + ((♯‘𝑊) − 𝐿)) ≤ (♯‘𝑊))) |
38 | 35, 36, 37 | sylc 65 |
. . . . . . . 8
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊))
∧ 𝐾 < 𝐿) → (𝐾 + ((♯‘𝑊) − 𝐿)) ≤ (♯‘𝑊)) |
39 | 38 | adantl 473 |
. . . . . . 7
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → (𝐾 + ((♯‘𝑊) − 𝐿)) ≤ (♯‘𝑊)) |
40 | | simpl 474 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐾 ∈ (0...(♯‘𝑊)) ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ (𝐾 + ((♯‘𝑊) − 𝐿)) ≤ (♯‘𝑊))) → 𝑊 ∈ Word 𝑉) |
41 | | elfzelz 12531 |
. . . . . . . . . 10
⊢ (𝐾 ∈
(0...(♯‘𝑊))
→ 𝐾 ∈
ℤ) |
42 | 41 | 3ad2ant1 1128 |
. . . . . . . . 9
⊢ ((𝐾 ∈
(0...(♯‘𝑊))
∧ ((♯‘𝑊)
− 𝐿) ∈
(0...(♯‘𝑊))
∧ (𝐾 +
((♯‘𝑊) −
𝐿)) ≤
(♯‘𝑊)) →
𝐾 ∈
ℤ) |
43 | 42 | adantl 473 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐾 ∈ (0...(♯‘𝑊)) ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ (𝐾 + ((♯‘𝑊) − 𝐿)) ≤ (♯‘𝑊))) → 𝐾 ∈ ℤ) |
44 | | elfzelz 12531 |
. . . . . . . . . 10
⊢
(((♯‘𝑊)
− 𝐿) ∈
(0...(♯‘𝑊))
→ ((♯‘𝑊)
− 𝐿) ∈
ℤ) |
45 | 44 | 3ad2ant2 1129 |
. . . . . . . . 9
⊢ ((𝐾 ∈
(0...(♯‘𝑊))
∧ ((♯‘𝑊)
− 𝐿) ∈
(0...(♯‘𝑊))
∧ (𝐾 +
((♯‘𝑊) −
𝐿)) ≤
(♯‘𝑊)) →
((♯‘𝑊) −
𝐿) ∈
ℤ) |
46 | 45 | adantl 473 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐾 ∈ (0...(♯‘𝑊)) ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ (𝐾 + ((♯‘𝑊) − 𝐿)) ≤ (♯‘𝑊))) → ((♯‘𝑊) − 𝐿) ∈ ℤ) |
47 | | 2cshw 13755 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐾 ∈ ℤ ∧ ((♯‘𝑊) − 𝐿) ∈ ℤ) → ((𝑊 cyclShift 𝐾) cyclShift ((♯‘𝑊) − 𝐿)) = (𝑊 cyclShift (𝐾 + ((♯‘𝑊) − 𝐿)))) |
48 | 40, 43, 46, 47 | syl3anc 1477 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝐾 ∈ (0...(♯‘𝑊)) ∧ ((♯‘𝑊) − 𝐿) ∈ (0...(♯‘𝑊)) ∧ (𝐾 + ((♯‘𝑊) − 𝐿)) ≤ (♯‘𝑊))) → ((𝑊 cyclShift 𝐾) cyclShift ((♯‘𝑊) − 𝐿)) = (𝑊 cyclShift (𝐾 + ((♯‘𝑊) − 𝐿)))) |
49 | 8, 11, 16, 39, 48 | syl13anc 1479 |
. . . . . 6
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → ((𝑊 cyclShift 𝐾) cyclShift ((♯‘𝑊) − 𝐿)) = (𝑊 cyclShift (𝐾 + ((♯‘𝑊) − 𝐿)))) |
50 | 12 | 3ad2ant1 1128 |
. . . . . . 7
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊))
∧ 𝐾 < 𝐿) → 𝐿 ∈ (0...(♯‘𝑊))) |
51 | | elfzelz 12531 |
. . . . . . . 8
⊢ (𝐿 ∈
(0...(♯‘𝑊))
→ 𝐿 ∈
ℤ) |
52 | | 2cshwid 13756 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → ((𝑊 cyclShift 𝐿) cyclShift ((♯‘𝑊) − 𝐿)) = 𝑊) |
53 | 51, 52 | sylan2 492 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝑊 cyclShift 𝐿) cyclShift ((♯‘𝑊) − 𝐿)) = 𝑊) |
54 | 7, 50, 53 | syl2an 495 |
. . . . . 6
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → ((𝑊 cyclShift 𝐿) cyclShift ((♯‘𝑊) − 𝐿)) = 𝑊) |
55 | 3, 49, 54 | 3eqtr3d 2798 |
. . . . 5
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → (𝑊 cyclShift (𝐾 + ((♯‘𝑊) − 𝐿))) = 𝑊) |
56 | | simplrl 819 |
. . . . . 6
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → 𝜑) |
57 | | simplrr 820 |
. . . . . 6
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) |
58 | | 3simpa 1143 |
. . . . . . . . . . . 12
⊢ ((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐿 <
(♯‘𝑊)) →
(𝐿 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ)) |
59 | 17, 58 | sylbi 207 |
. . . . . . . . . . 11
⊢ (𝐿 ∈
(0..^(♯‘𝑊))
→ (𝐿 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ)) |
60 | | nnz 11587 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑊)
∈ ℕ → (♯‘𝑊) ∈ ℤ) |
61 | | nn0z 11588 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℤ) |
62 | | zsubcl 11607 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝑊)
∈ ℤ ∧ 𝐿
∈ ℤ) → ((♯‘𝑊) − 𝐿) ∈ ℤ) |
63 | 60, 61, 62 | syl2anr 496 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) → ((♯‘𝑊) − 𝐿) ∈ ℤ) |
64 | 63 | anim2i 594 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ)) → (𝐾
∈ ℤ ∧ ((♯‘𝑊) − 𝐿) ∈ ℤ)) |
65 | 64 | ancoms 468 |
. . . . . . . . . . . 12
⊢ (((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐾
∈ ℤ) → (𝐾
∈ ℤ ∧ ((♯‘𝑊) − 𝐿) ∈ ℤ)) |
66 | | zaddcl 11605 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℤ ∧
((♯‘𝑊) −
𝐿) ∈ ℤ) →
(𝐾 + ((♯‘𝑊) − 𝐿)) ∈ ℤ) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) ∧ 𝐾
∈ ℤ) → (𝐾 +
((♯‘𝑊) −
𝐿)) ∈
ℤ) |
68 | 59, 30, 67 | syl2an 495 |
. . . . . . . . . 10
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊)))
→ (𝐾 +
((♯‘𝑊) −
𝐿)) ∈
ℤ) |
69 | 68 | 3adant3 1127 |
. . . . . . . . 9
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊))
∧ 𝐾 < 𝐿) → (𝐾 + ((♯‘𝑊) − 𝐿)) ∈ ℤ) |
70 | | elfzo0 12699 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈
(0..^(♯‘𝑊))
↔ (𝐾 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐾 < (♯‘𝑊))) |
71 | | elnn0z 11578 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℤ
∧ 0 ≤ 𝐾)) |
72 | 18 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) ∧ (𝐿 ∈ ℕ0 ∧
(♯‘𝑊) ∈
ℕ ∧ 𝐿 <
(♯‘𝑊))) →
𝐾 ∈
ℝ) |
73 | 23 | 3adant3 1127 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐿 <
(♯‘𝑊)) →
((♯‘𝑊) −
𝐿) ∈
ℝ) |
74 | 73 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) ∧ (𝐿 ∈ ℕ0 ∧
(♯‘𝑊) ∈
ℕ ∧ 𝐿 <
(♯‘𝑊))) →
((♯‘𝑊) −
𝐿) ∈
ℝ) |
75 | | simplr 809 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) ∧ (𝐿 ∈ ℕ0 ∧
(♯‘𝑊) ∈
ℕ ∧ 𝐿 <
(♯‘𝑊))) →
0 ≤ 𝐾) |
76 | | posdif 10709 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐿 ∈ ℝ ∧
(♯‘𝑊) ∈
ℝ) → (𝐿 <
(♯‘𝑊) ↔ 0
< ((♯‘𝑊)
− 𝐿))) |
77 | 21, 20, 76 | syl2an 495 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ) → (𝐿
< (♯‘𝑊)
↔ 0 < ((♯‘𝑊) − 𝐿))) |
78 | 77 | biimp3a 1577 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐿 <
(♯‘𝑊)) → 0
< ((♯‘𝑊)
− 𝐿)) |
79 | 78 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) ∧ (𝐿 ∈ ℕ0 ∧
(♯‘𝑊) ∈
ℕ ∧ 𝐿 <
(♯‘𝑊))) →
0 < ((♯‘𝑊)
− 𝐿)) |
80 | 72, 74, 75, 79 | addgegt0d 10789 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) ∧ (𝐿 ∈ ℕ0 ∧
(♯‘𝑊) ∈
ℕ ∧ 𝐿 <
(♯‘𝑊))) →
0 < (𝐾 +
((♯‘𝑊) −
𝐿))) |
81 | 80 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) → ((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐿 <
(♯‘𝑊)) → 0
< (𝐾 +
((♯‘𝑊) −
𝐿)))) |
82 | 71, 81 | sylbi 207 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℕ0
→ ((𝐿 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → 0 < (𝐾 + ((♯‘𝑊) − 𝐿)))) |
83 | 82 | 3ad2ant1 1128 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐾 <
(♯‘𝑊)) →
((𝐿 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → 0 < (𝐾 + ((♯‘𝑊) − 𝐿)))) |
84 | 70, 83 | sylbi 207 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈
(0..^(♯‘𝑊))
→ ((𝐿 ∈
ℕ0 ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → 0 < (𝐾 + ((♯‘𝑊) − 𝐿)))) |
85 | 84 | com12 32 |
. . . . . . . . . . . 12
⊢ ((𝐿 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ 𝐿 <
(♯‘𝑊)) →
(𝐾 ∈
(0..^(♯‘𝑊))
→ 0 < (𝐾 +
((♯‘𝑊) −
𝐿)))) |
86 | 17, 85 | sylbi 207 |
. . . . . . . . . . 11
⊢ (𝐿 ∈
(0..^(♯‘𝑊))
→ (𝐾 ∈
(0..^(♯‘𝑊))
→ 0 < (𝐾 +
((♯‘𝑊) −
𝐿)))) |
87 | 86 | imp 444 |
. . . . . . . . . 10
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊)))
→ 0 < (𝐾 +
((♯‘𝑊) −
𝐿))) |
88 | 87 | 3adant3 1127 |
. . . . . . . . 9
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊))
∧ 𝐾 < 𝐿) → 0 < (𝐾 + ((♯‘𝑊) − 𝐿))) |
89 | | elnnz 11575 |
. . . . . . . . 9
⊢ ((𝐾 + ((♯‘𝑊) − 𝐿)) ∈ ℕ ↔ ((𝐾 + ((♯‘𝑊) − 𝐿)) ∈ ℤ ∧ 0 < (𝐾 + ((♯‘𝑊) − 𝐿)))) |
90 | 69, 88, 89 | sylanbrc 701 |
. . . . . . . 8
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊))
∧ 𝐾 < 𝐿) → (𝐾 + ((♯‘𝑊) − 𝐿)) ∈ ℕ) |
91 | 17 | simp2bi 1141 |
. . . . . . . . 9
⊢ (𝐿 ∈
(0..^(♯‘𝑊))
→ (♯‘𝑊)
∈ ℕ) |
92 | 91 | 3ad2ant1 1128 |
. . . . . . . 8
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊))
∧ 𝐾 < 𝐿) → (♯‘𝑊) ∈
ℕ) |
93 | | elfzo1 12708 |
. . . . . . . 8
⊢ ((𝐾 + ((♯‘𝑊) − 𝐿)) ∈ (1..^(♯‘𝑊)) ↔ ((𝐾 + ((♯‘𝑊) − 𝐿)) ∈ ℕ ∧ (♯‘𝑊) ∈ ℕ ∧ (𝐾 + ((♯‘𝑊) − 𝐿)) < (♯‘𝑊))) |
94 | 90, 92, 36, 93 | syl3anbrc 1429 |
. . . . . . 7
⊢ ((𝐿 ∈
(0..^(♯‘𝑊))
∧ 𝐾 ∈
(0..^(♯‘𝑊))
∧ 𝐾 < 𝐿) → (𝐾 + ((♯‘𝑊) − 𝐿)) ∈ (1..^(♯‘𝑊))) |
95 | 94 | adantl 473 |
. . . . . 6
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → (𝐾 + ((♯‘𝑊) − 𝐿)) ∈ (1..^(♯‘𝑊))) |
96 | 4 | cshwshashlem1 16000 |
. . . . . 6
⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ (𝐾 + ((♯‘𝑊) − 𝐿)) ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift (𝐾 + ((♯‘𝑊) − 𝐿))) ≠ 𝑊) |
97 | 56, 57, 95, 96 | syl3anc 1477 |
. . . . 5
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → (𝑊 cyclShift (𝐾 + ((♯‘𝑊) − 𝐿))) ≠ 𝑊) |
98 | 55, 97 | pm2.21ddne 3012 |
. . . 4
⊢ ((((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) ∧ (𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿)) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾)) |
99 | 98 | ex 449 |
. . 3
⊢ (((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) ∧ (𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0))) → ((𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾))) |
100 | 99 | ex 449 |
. 2
⊢ ((𝑊 cyclShift 𝐿) = (𝑊 cyclShift 𝐾) → ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → ((𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾)))) |
101 | | 2a1 28 |
. 2
⊢ ((𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾) → ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → ((𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾)))) |
102 | 100, 101 | pm2.61ine 3011 |
1
⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0)) → ((𝐿 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 ∈ (0..^(♯‘𝑊)) ∧ 𝐾 < 𝐿) → (𝑊 cyclShift 𝐿) ≠ (𝑊 cyclShift 𝐾))) |