Proof of Theorem cshwcsh2id
Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑦 = (𝑧 cyclShift 𝑘) → (𝑦 cyclShift 𝑚) = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) |
2 | 1 | eqeq2d 2632 |
. . . . . . . 8
⊢ (𝑦 = (𝑧 cyclShift 𝑘) → (𝑥 = (𝑦 cyclShift 𝑚) ↔ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚))) |
3 | 2 | anbi2d 740 |
. . . . . . 7
⊢ (𝑦 = (𝑧 cyclShift 𝑘) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ↔ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)))) |
4 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝑦 = (𝑧 cyclShift 𝑘) ∧ 𝑘 ∈ (0...(#‘𝑧))) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ↔ (𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)))) |
5 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (0...(#‘𝑧)) → 𝑘 ∈ ℕ0) |
6 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (0...(#‘𝑦)) → 𝑚 ∈ ℕ0) |
7 | | nn0addcl 11328 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (𝑘 + 𝑚) ∈
ℕ0) |
8 | 5, 6, 7 | syl2anr 495 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → (𝑘 + 𝑚) ∈
ℕ0) |
9 | 8 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ ((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → (𝑘 + 𝑚) ∈
ℕ0) |
10 | | elfz3nn0 12434 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (0...(#‘𝑧)) → (#‘𝑧) ∈
ℕ0) |
11 | 10 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ ((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → (#‘𝑧) ∈
ℕ0) |
12 | | simprl 794 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ ((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → (𝑘 + 𝑚) ≤ (#‘𝑧)) |
13 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 + 𝑚) ∈ (0...(#‘𝑧)) ↔ ((𝑘 + 𝑚) ∈ ℕ0 ∧
(#‘𝑧) ∈
ℕ0 ∧ (𝑘 + 𝑚) ≤ (#‘𝑧))) |
14 | 9, 11, 12, 13 | syl3anbrc 1246 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ ((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → (𝑘 + 𝑚) ∈ (0...(#‘𝑧))) |
15 | 14 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ ((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → (𝑘 + 𝑚) ∈ (0...(#‘𝑧))) |
16 | | cshwcsh2id.1 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑧 ∈ Word 𝑉) |
17 | 16 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → 𝑧 ∈ Word 𝑉) |
18 | 17 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ ((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → 𝑧 ∈ Word 𝑉) |
19 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (0...(#‘𝑧)) → 𝑘 ∈ ℤ) |
20 | 19 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ ((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → 𝑘 ∈ ℤ) |
21 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ (0...(#‘𝑦)) → 𝑚 ∈ ℤ) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → 𝑚 ∈ ℤ) |
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ ((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → 𝑚 ∈ ℤ) |
24 | | 2cshw 13559 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ Word 𝑉 ∧ 𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑧 cyclShift 𝑘) cyclShift 𝑚) = (𝑧 cyclShift (𝑘 + 𝑚))) |
25 | 18, 20, 23, 24 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ ((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → ((𝑧 cyclShift 𝑘) cyclShift 𝑚) = (𝑧 cyclShift (𝑘 + 𝑚))) |
26 | 25 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ ((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) ↔ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚)))) |
27 | 26 | biimpa 501 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ ((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚))) |
28 | 15, 27 | jca 554 |
. . . . . . . . . . . 12
⊢ ((((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ ((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → ((𝑘 + 𝑚) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚)))) |
29 | 28 | exp41 638 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (0...(#‘𝑦)) → (𝑘 ∈ (0...(#‘𝑧)) → (((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) → ((𝑘 + 𝑚) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚))))))) |
30 | 29 | com23 86 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (0...(#‘𝑦)) → (((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → (𝑘 ∈ (0...(#‘𝑧)) → (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) → ((𝑘 + 𝑚) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚))))))) |
31 | 30 | com24 95 |
. . . . . . . . 9
⊢ (𝑚 ∈ (0...(#‘𝑦)) → (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) → (𝑘 ∈ (0...(#‘𝑧)) → (((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → ((𝑘 + 𝑚) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚))))))) |
32 | 31 | imp 445 |
. . . . . . . 8
⊢ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → (𝑘 ∈ (0...(#‘𝑧)) → (((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → ((𝑘 + 𝑚) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚)))))) |
33 | 32 | com12 32 |
. . . . . . 7
⊢ (𝑘 ∈ (0...(#‘𝑧)) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → (((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → ((𝑘 + 𝑚) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚)))))) |
34 | 33 | adantl 482 |
. . . . . 6
⊢ ((𝑦 = (𝑧 cyclShift 𝑘) ∧ 𝑘 ∈ (0...(#‘𝑧))) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → (((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → ((𝑘 + 𝑚) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚)))))) |
35 | 4, 34 | sylbid 230 |
. . . . 5
⊢ ((𝑦 = (𝑧 cyclShift 𝑘) ∧ 𝑘 ∈ (0...(#‘𝑧))) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → ((𝑘 + 𝑚) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚)))))) |
36 | 35 | ancoms 469 |
. . . 4
⊢ ((𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘)) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → ((𝑘 + 𝑚) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚)))))) |
37 | 36 | impcom 446 |
. . 3
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → (((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → ((𝑘 + 𝑚) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚))))) |
38 | | oveq2 6658 |
. . . . 5
⊢ (𝑛 = (𝑘 + 𝑚) → (𝑧 cyclShift 𝑛) = (𝑧 cyclShift (𝑘 + 𝑚))) |
39 | 38 | eqeq2d 2632 |
. . . 4
⊢ (𝑛 = (𝑘 + 𝑚) → (𝑥 = (𝑧 cyclShift 𝑛) ↔ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚)))) |
40 | 39 | rspcev 3309 |
. . 3
⊢ (((𝑘 + 𝑚) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)) |
41 | 37, 40 | syl6com 37 |
. 2
⊢ (((𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
42 | | elfz2 12333 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (0...(#‘𝑧)) ↔ ((0 ∈ ℤ
∧ (#‘𝑧) ∈
ℤ ∧ 𝑘 ∈
ℤ) ∧ (0 ≤ 𝑘
∧ 𝑘 ≤ (#‘𝑧)))) |
43 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℤ) |
44 | | zaddcl 11417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 + 𝑚) ∈ ℤ) |
45 | 44 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ℤ → (𝑚 ∈ ℤ → (𝑘 + 𝑚) ∈ ℤ)) |
46 | 45 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝑧) ∈
ℤ ∧ 𝑘 ∈
ℤ) → (𝑚 ∈
ℤ → (𝑘 + 𝑚) ∈
ℤ)) |
47 | 46 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑚 ∈ ℤ ∧
((#‘𝑧) ∈ ℤ
∧ 𝑘 ∈ ℤ))
→ (𝑘 + 𝑚) ∈
ℤ) |
48 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑚 ∈ ℤ ∧
((#‘𝑧) ∈ ℤ
∧ 𝑘 ∈ ℤ))
→ (#‘𝑧) ∈
ℤ) |
49 | 47, 48 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑚 ∈ ℤ ∧
((#‘𝑧) ∈ ℤ
∧ 𝑘 ∈ ℤ))
→ ((𝑘 + 𝑚) − (#‘𝑧)) ∈
ℤ) |
50 | 49 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℤ →
(((#‘𝑧) ∈
ℤ ∧ 𝑘 ∈
ℤ) → ((𝑘 + 𝑚) − (#‘𝑧)) ∈
ℤ)) |
51 | 43, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℕ0
→ (((#‘𝑧) ∈
ℤ ∧ 𝑘 ∈
ℤ) → ((𝑘 + 𝑚) − (#‘𝑧)) ∈
ℤ)) |
52 | 51 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑧) ∈
ℤ ∧ 𝑘 ∈
ℤ) → (𝑚 ∈
ℕ0 → ((𝑘 + 𝑚) − (#‘𝑧)) ∈ ℤ)) |
53 | 52 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℤ ∧ (#‘𝑧) ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑚 ∈ ℕ0 → ((𝑘 + 𝑚) − (#‘𝑧)) ∈ ℤ)) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((0
∈ ℤ ∧ (#‘𝑧) ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (0 ≤ 𝑘 ∧ 𝑘 ≤ (#‘𝑧))) → (𝑚 ∈ ℕ0 → ((𝑘 + 𝑚) − (#‘𝑧)) ∈ ℤ)) |
55 | 42, 54 | sylbi 207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (0...(#‘𝑧)) → (𝑚 ∈ ℕ0 → ((𝑘 + 𝑚) − (#‘𝑧)) ∈ ℤ)) |
56 | 6, 55 | mpan9 486 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → ((𝑘 + 𝑚) − (#‘𝑧)) ∈ ℤ) |
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → ((𝑘 + 𝑚) − (#‘𝑧)) ∈ ℤ) |
58 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (0...(#‘𝑧)) ↔ (𝑘 ∈ ℕ0 ∧
(#‘𝑧) ∈
ℕ0 ∧ 𝑘
≤ (#‘𝑧))) |
59 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
60 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝑧) ∈
ℕ0 → (#‘𝑧) ∈ ℝ) |
61 | 59, 60 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) → (𝑘 ∈ ℝ ∧ (#‘𝑧) ∈
ℝ)) |
62 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) |
63 | 61, 62 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℝ ∧
(#‘𝑧) ∈ ℝ)
∧ 𝑚 ∈
ℝ)) |
64 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑘 ∈ ℝ ∧
(#‘𝑧) ∈ ℝ)
∧ 𝑚 ∈ ℝ)
→ (#‘𝑧) ∈
ℝ) |
65 | | readdcl 10019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ) → (𝑘 + 𝑚) ∈ ℝ) |
66 | 65 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑘 ∈ ℝ ∧
(#‘𝑧) ∈ ℝ)
∧ 𝑚 ∈ ℝ)
→ (𝑘 + 𝑚) ∈
ℝ) |
67 | 64, 66 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑘 ∈ ℝ ∧
(#‘𝑧) ∈ ℝ)
∧ 𝑚 ∈ ℝ)
→ ((#‘𝑧) <
(𝑘 + 𝑚) ↔ ¬ (𝑘 + 𝑚) ≤ (#‘𝑧))) |
68 | 64, 66 | posdifd 10614 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑘 ∈ ℝ ∧
(#‘𝑧) ∈ ℝ)
∧ 𝑚 ∈ ℝ)
→ ((#‘𝑧) <
(𝑘 + 𝑚) ↔ 0 < ((𝑘 + 𝑚) − (#‘𝑧)))) |
69 | 68 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑘 ∈ ℝ ∧
(#‘𝑧) ∈ ℝ)
∧ 𝑚 ∈ ℝ)
→ ((#‘𝑧) <
(𝑘 + 𝑚) → 0 < ((𝑘 + 𝑚) − (#‘𝑧)))) |
70 | 67, 69 | sylbird 250 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑘 ∈ ℝ ∧
(#‘𝑧) ∈ ℝ)
∧ 𝑚 ∈ ℝ)
→ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) → 0 < ((𝑘 + 𝑚) − (#‘𝑧)))) |
71 | 63, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) ∧ 𝑚 ∈ ℕ0) → (¬
(𝑘 + 𝑚) ≤ (#‘𝑧) → 0 < ((𝑘 + 𝑚) − (#‘𝑧)))) |
72 | 71 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) → (𝑚 ∈ ℕ0 → (¬
(𝑘 + 𝑚) ≤ (#‘𝑧) → 0 < ((𝑘 + 𝑚) − (#‘𝑧))))) |
73 | 72 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0 ∧ 𝑘
≤ (#‘𝑧)) →
(𝑚 ∈
ℕ0 → (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) → 0 < ((𝑘 + 𝑚) − (#‘𝑧))))) |
74 | 58, 73 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (0...(#‘𝑧)) → (𝑚 ∈ ℕ0 → (¬
(𝑘 + 𝑚) ≤ (#‘𝑧) → 0 < ((𝑘 + 𝑚) − (#‘𝑧))))) |
75 | 6, 74 | mpan9 486 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) → 0 < ((𝑘 + 𝑚) − (#‘𝑧)))) |
76 | 75 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝑘 + 𝑚) ≤ (#‘𝑧) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → 0 < ((𝑘 + 𝑚) − (#‘𝑧)))) |
77 | 76 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
(𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → 0 < ((𝑘 + 𝑚) − (#‘𝑧)))) |
78 | 77 | impcom 446 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → 0 < ((𝑘 + 𝑚) − (#‘𝑧))) |
79 | | elnnz 11387 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 + 𝑚) − (#‘𝑧)) ∈ ℕ ↔ (((𝑘 + 𝑚) − (#‘𝑧)) ∈ ℤ ∧ 0 < ((𝑘 + 𝑚) − (#‘𝑧)))) |
80 | 57, 78, 79 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → ((𝑘 + 𝑚) − (#‘𝑧)) ∈ ℕ) |
81 | 80 | nnnn0d 11351 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → ((𝑘 + 𝑚) − (#‘𝑧)) ∈
ℕ0) |
82 | 10 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → (#‘𝑧) ∈
ℕ0) |
83 | | cshwcsh2id.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) |
84 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑦) =
(#‘𝑧) →
(0...(#‘𝑦)) =
(0...(#‘𝑧))) |
85 | 84 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑦) =
(#‘𝑧) → (𝑚 ∈ (0...(#‘𝑦)) ↔ 𝑚 ∈ (0...(#‘𝑧)))) |
86 | 85 | anbi1d 741 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑦) =
(#‘𝑧) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ↔ (𝑚 ∈ (0...(#‘𝑧)) ∧ 𝑘 ∈ (0...(#‘𝑧))))) |
87 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ (0...(#‘𝑧)) ↔ (𝑚 ∈ ℕ0 ∧
(#‘𝑧) ∈
ℕ0 ∧ 𝑚
≤ (#‘𝑧))) |
88 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) → 𝑘 ∈ ℝ) |
89 | 88, 62 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) ∧ 𝑚 ∈ ℕ0) → (𝑘 ∈ ℝ ∧ 𝑚 ∈
ℝ)) |
90 | 60, 60 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝑧) ∈
ℕ0 → ((#‘𝑧) ∈ ℝ ∧ (#‘𝑧) ∈
ℝ)) |
91 | 90 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) ∧ 𝑚 ∈ ℕ0) →
((#‘𝑧) ∈ ℝ
∧ (#‘𝑧) ∈
ℝ)) |
92 | | le2add 10510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ) ∧
((#‘𝑧) ∈ ℝ
∧ (#‘𝑧) ∈
ℝ)) → ((𝑘 ≤
(#‘𝑧) ∧ 𝑚 ≤ (#‘𝑧)) → (𝑘 + 𝑚) ≤ ((#‘𝑧) + (#‘𝑧)))) |
93 | 89, 91, 92 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ≤ (#‘𝑧) ∧ 𝑚 ≤ (#‘𝑧)) → (𝑘 + 𝑚) ≤ ((#‘𝑧) + (#‘𝑧)))) |
94 | | nn0readdcl 11357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑘 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (𝑘 + 𝑚) ∈ ℝ) |
95 | 94 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) ∧ 𝑚 ∈ ℕ0) → (𝑘 + 𝑚) ∈ ℝ) |
96 | 60 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) ∧ 𝑚 ∈ ℕ0) →
(#‘𝑧) ∈
ℝ) |
97 | 95, 96, 96 | lesubadd2d 10626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) ∧ 𝑚 ∈ ℕ0) → (((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧) ↔ (𝑘 + 𝑚) ≤ ((#‘𝑧) + (#‘𝑧)))) |
98 | 93, 97 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ≤ (#‘𝑧) ∧ 𝑚 ≤ (#‘𝑧)) → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧))) |
99 | 98 | expcomd 454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) ∧ 𝑚 ∈ ℕ0) → (𝑚 ≤ (#‘𝑧) → (𝑘 ≤ (#‘𝑧) → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧)))) |
100 | 99 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) → (𝑚 ∈ ℕ0 → (𝑚 ≤ (#‘𝑧) → (𝑘 ≤ (#‘𝑧) → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧))))) |
101 | 100 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0) → (𝑘 ≤ (#‘𝑧) → (𝑚 ≤ (#‘𝑧) → (𝑚 ∈ ℕ0 → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧))))) |
102 | 101 | 3impia 1261 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0 ∧ 𝑘
≤ (#‘𝑧)) →
(𝑚 ≤ (#‘𝑧) → (𝑚 ∈ ℕ0 → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧)))) |
103 | 102 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 ∈ ℕ0
→ (𝑚 ≤
(#‘𝑧) → ((𝑘 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0 ∧ 𝑘
≤ (#‘𝑧)) →
((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧)))) |
104 | 103 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 ∈ ℕ0
∧ 𝑚 ≤ (#‘𝑧)) → ((𝑘 ∈ ℕ0 ∧
(#‘𝑧) ∈
ℕ0 ∧ 𝑘
≤ (#‘𝑧)) →
((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧))) |
105 | 58, 104 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 ∈ ℕ0
∧ 𝑚 ≤ (#‘𝑧)) → (𝑘 ∈ (0...(#‘𝑧)) → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧))) |
106 | 105 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑚 ∈ ℕ0
∧ (#‘𝑧) ∈
ℕ0 ∧ 𝑚
≤ (#‘𝑧)) →
(𝑘 ∈
(0...(#‘𝑧)) →
((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧))) |
107 | 87, 106 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ (0...(#‘𝑧)) → (𝑘 ∈ (0...(#‘𝑧)) → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧))) |
108 | 107 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ (0...(#‘𝑧)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧)) |
109 | 86, 108 | syl6bi 243 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑦) =
(#‘𝑧) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧))) |
110 | 109 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝑦) =
(#‘𝑧) ∧
(#‘𝑥) =
(#‘𝑦)) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧))) |
111 | 83, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧))) |
112 | 111 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((¬
(𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧))) |
113 | 112 | impcom 446 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧)) |
114 | | elfz2nn0 12431 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧)) ↔ (((𝑘 + 𝑚) − (#‘𝑧)) ∈ ℕ0 ∧
(#‘𝑧) ∈
ℕ0 ∧ ((𝑘 + 𝑚) − (#‘𝑧)) ≤ (#‘𝑧))) |
115 | 81, 82, 113, 114 | syl3anbrc 1246 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → ((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧))) |
116 | 115 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → ((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧))) |
117 | 16 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
(𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → 𝑧 ∈ Word 𝑉) |
118 | 117 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → 𝑧 ∈ Word 𝑉) |
119 | 19 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → 𝑘 ∈ ℤ) |
120 | 22 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → 𝑚 ∈ ℤ) |
121 | 118, 119,
120, 24 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → ((𝑧 cyclShift 𝑘) cyclShift 𝑚) = (𝑧 cyclShift (𝑘 + 𝑚))) |
122 | 19, 21, 44 | syl2anr 495 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) → (𝑘 + 𝑚) ∈ ℤ) |
123 | | cshwsublen 13542 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ Word 𝑉 ∧ (𝑘 + 𝑚) ∈ ℤ) → (𝑧 cyclShift (𝑘 + 𝑚)) = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧)))) |
124 | 117, 122,
123 | syl2anr 495 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → (𝑧 cyclShift (𝑘 + 𝑚)) = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧)))) |
125 | 121, 124 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → ((𝑧 cyclShift 𝑘) cyclShift 𝑚) = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧)))) |
126 | 125 | eqeq2d 2632 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) → (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) ↔ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧))))) |
127 | 126 | biimpa 501 |
. . . . . . . . . . . 12
⊢ ((((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧)))) |
128 | 116, 127 | jca 554 |
. . . . . . . . . . 11
⊢ ((((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑘 ∈ (0...(#‘𝑧))) ∧ (¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → (((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧))))) |
129 | 128 | exp41 638 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (0...(#‘𝑦)) → (𝑘 ∈ (0...(#‘𝑧)) → ((¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) → (((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧)))))))) |
130 | 129 | com23 86 |
. . . . . . . . 9
⊢ (𝑚 ∈ (0...(#‘𝑦)) → ((¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → (𝑘 ∈ (0...(#‘𝑧)) → (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) → (((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧)))))))) |
131 | 130 | com24 95 |
. . . . . . . 8
⊢ (𝑚 ∈ (0...(#‘𝑦)) → (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) → (𝑘 ∈ (0...(#‘𝑧)) → ((¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → (((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧)))))))) |
132 | 131 | imp 445 |
. . . . . . 7
⊢ ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → (𝑘 ∈ (0...(#‘𝑧)) → ((¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → (((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧))))))) |
133 | 3, 132 | syl6bi 243 |
. . . . . 6
⊢ (𝑦 = (𝑧 cyclShift 𝑘) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (𝑘 ∈ (0...(#‘𝑧)) → ((¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → (((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧)))))))) |
134 | 133 | com23 86 |
. . . . 5
⊢ (𝑦 = (𝑧 cyclShift 𝑘) → (𝑘 ∈ (0...(#‘𝑧)) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ((¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → (((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧)))))))) |
135 | 134 | impcom 446 |
. . . 4
⊢ ((𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘)) → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ((¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → (((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧))))))) |
136 | 135 | impcom 446 |
. . 3
⊢ (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ((¬ (𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → (((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧)))))) |
137 | | oveq2 6658 |
. . . . 5
⊢ (𝑛 = ((𝑘 + 𝑚) − (#‘𝑧)) → (𝑧 cyclShift 𝑛) = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧)))) |
138 | 137 | eqeq2d 2632 |
. . . 4
⊢ (𝑛 = ((𝑘 + 𝑚) − (#‘𝑧)) → (𝑥 = (𝑧 cyclShift 𝑛) ↔ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧))))) |
139 | 138 | rspcev 3309 |
. . 3
⊢ ((((𝑘 + 𝑚) − (#‘𝑧)) ∈ (0...(#‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (#‘𝑧)))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)) |
140 | 136, 139 | syl6com 37 |
. 2
⊢ ((¬
(𝑘 + 𝑚) ≤ (#‘𝑧) ∧ 𝜑) → (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
141 | 41, 140 | pm2.61ian 831 |
1
⊢ (𝜑 → (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |