Proof of Theorem cshwcsh2id
Step | Hyp | Ref
| Expression |
1 | | oveq1 7278 |
. . . . . . . . 9
⊢ (𝑦 = (𝑧 cyclShift 𝑘) → (𝑦 cyclShift 𝑚) = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) |
2 | 1 | eqeq2d 2751 |
. . . . . . . 8
⊢ (𝑦 = (𝑧 cyclShift 𝑘) → (𝑥 = (𝑦 cyclShift 𝑚) ↔ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚))) |
3 | 2 | anbi2d 629 |
. . . . . . 7
⊢ (𝑦 = (𝑧 cyclShift 𝑘) → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ↔ (𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)))) |
4 | 3 | adantr 481 |
. . . . . 6
⊢ ((𝑦 = (𝑧 cyclShift 𝑘) ∧ 𝑘 ∈ (0...(♯‘𝑧))) → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ↔ (𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)))) |
5 | | elfznn0 13348 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(0...(♯‘𝑧))
→ 𝑘 ∈
ℕ0) |
6 | | elfznn0 13348 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈
(0...(♯‘𝑦))
→ 𝑚 ∈
ℕ0) |
7 | | nn0addcl 12268 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (𝑘 + 𝑚) ∈
ℕ0) |
8 | 5, 6, 7 | syl2anr 597 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
→ (𝑘 + 𝑚) ∈
ℕ0) |
9 | 8 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ ((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → (𝑘 + 𝑚) ∈
ℕ0) |
10 | | elfz3nn0 13349 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈
(0...(♯‘𝑧))
→ (♯‘𝑧)
∈ ℕ0) |
11 | 10 | ad2antlr 724 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ ((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → (♯‘𝑧) ∈
ℕ0) |
12 | | simprl 768 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ ((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → (𝑘 + 𝑚) ≤ (♯‘𝑧)) |
13 | | elfz2nn0 13346 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 + 𝑚) ∈ (0...(♯‘𝑧)) ↔ ((𝑘 + 𝑚) ∈ ℕ0 ∧
(♯‘𝑧) ∈
ℕ0 ∧ (𝑘 + 𝑚) ≤ (♯‘𝑧))) |
14 | 9, 11, 12, 13 | syl3anbrc 1342 |
. . . . . . . . . . . . . 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 13255 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(0...(♯‘𝑧))
→ 𝑘 ∈
ℤ) |
20 | 19 | ad2antlr 724 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ ((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → 𝑘 ∈ ℤ) |
21 | | elfzelz 13255 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈
(0...(♯‘𝑦))
→ 𝑚 ∈
ℤ) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
→ 𝑚 ∈
ℤ) |
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ ((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → 𝑚 ∈ ℤ) |
24 | | 2cshw 14524 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ Word 𝑉 ∧ 𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑧 cyclShift 𝑘) cyclShift 𝑚) = (𝑧 cyclShift (𝑘 + 𝑚))) |
25 | 18, 20, 23, 24 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ ((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → ((𝑧 cyclShift 𝑘) cyclShift 𝑚) = (𝑧 cyclShift (𝑘 + 𝑚))) |
26 | 25 | eqeq2d 2751 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ ((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) ↔ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚)))) |
27 | 26 | biimpa 477 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ ((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚))) |
28 | 15, 27 | jca 512 |
. . . . . . . . . . . 12
⊢ ((((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ ((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → ((𝑘 + 𝑚) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚)))) |
29 | 28 | exp41 435 |
. . . . . . . . . . 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 407 |
. . . . . . . 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 239 |
. . . . 5
⊢ ((𝑦 = (𝑧 cyclShift 𝑘) ∧ 𝑘 ∈ (0...(♯‘𝑧))) → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → ((𝑘 + 𝑚) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚)))))) |
36 | 35 | ancoms 459 |
. . . 4
⊢ ((𝑘 ∈
(0...(♯‘𝑧))
∧ 𝑦 = (𝑧 cyclShift 𝑘)) → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → ((𝑘 + 𝑚) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚)))))) |
37 | 36 | impcom 408 |
. . 3
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(♯‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → (((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → ((𝑘 + 𝑚) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚))))) |
38 | | oveq2 7279 |
. . . 4
⊢ (𝑛 = (𝑘 + 𝑚) → (𝑧 cyclShift 𝑛) = (𝑧 cyclShift (𝑘 + 𝑚))) |
39 | 38 | rspceeqv 3576 |
. . 3
⊢ (((𝑘 + 𝑚) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift (𝑘 + 𝑚))) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)) |
40 | 37, 39 | syl6com 37 |
. 2
⊢ (((𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → (((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(♯‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
41 | | elfz2 13245 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈
(0...(♯‘𝑧))
↔ ((0 ∈ ℤ ∧ (♯‘𝑧) ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (0 ≤ 𝑘 ∧ 𝑘 ≤ (♯‘𝑧)))) |
42 | | nn0z 12343 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℤ) |
43 | | zaddcl 12360 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 + 𝑚) ∈ ℤ) |
44 | 43 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ ℤ → (𝑚 ∈ ℤ → (𝑘 + 𝑚) ∈ ℤ)) |
45 | 44 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((♯‘𝑧)
∈ ℤ ∧ 𝑘
∈ ℤ) → (𝑚
∈ ℤ → (𝑘 +
𝑚) ∈
ℤ)) |
46 | 45 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑚 ∈ ℤ ∧
((♯‘𝑧) ∈
ℤ ∧ 𝑘 ∈
ℤ)) → (𝑘 + 𝑚) ∈
ℤ) |
47 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑚 ∈ ℤ ∧
((♯‘𝑧) ∈
ℤ ∧ 𝑘 ∈
ℤ)) → (♯‘𝑧) ∈ ℤ) |
48 | 46, 47 | zsubcld 12430 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑚 ∈ ℤ ∧
((♯‘𝑧) ∈
ℤ ∧ 𝑘 ∈
ℤ)) → ((𝑘 +
𝑚) −
(♯‘𝑧)) ∈
ℤ) |
49 | 48 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℤ →
(((♯‘𝑧) ∈
ℤ ∧ 𝑘 ∈
ℤ) → ((𝑘 + 𝑚) − (♯‘𝑧)) ∈
ℤ)) |
50 | 42, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℕ0
→ (((♯‘𝑧)
∈ ℤ ∧ 𝑘
∈ ℤ) → ((𝑘
+ 𝑚) −
(♯‘𝑧)) ∈
ℤ)) |
51 | 50 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((♯‘𝑧)
∈ ℤ ∧ 𝑘
∈ ℤ) → (𝑚
∈ ℕ0 → ((𝑘 + 𝑚) − (♯‘𝑧)) ∈ ℤ)) |
52 | 51 | 3adant1 1129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℤ ∧ (♯‘𝑧) ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑚 ∈ ℕ0 → ((𝑘 + 𝑚) − (♯‘𝑧)) ∈ ℤ)) |
53 | 52 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((0
∈ ℤ ∧ (♯‘𝑧) ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (0 ≤ 𝑘 ∧ 𝑘 ≤ (♯‘𝑧))) → (𝑚 ∈ ℕ0 → ((𝑘 + 𝑚) − (♯‘𝑧)) ∈ ℤ)) |
54 | 41, 53 | sylbi 216 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈
(0...(♯‘𝑧))
→ (𝑚 ∈
ℕ0 → ((𝑘 + 𝑚) − (♯‘𝑧)) ∈ ℤ)) |
55 | 6, 54 | mpan9 507 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
→ ((𝑘 + 𝑚) − (♯‘𝑧)) ∈
ℤ) |
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → ((𝑘 + 𝑚) − (♯‘𝑧)) ∈ ℤ) |
57 | | elfz2nn0 13346 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(0...(♯‘𝑧))
↔ (𝑘 ∈
ℕ0 ∧ (♯‘𝑧) ∈ ℕ0 ∧ 𝑘 ≤ (♯‘𝑧))) |
58 | | nn0re 12242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
59 | | nn0re 12242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝑧)
∈ ℕ0 → (♯‘𝑧) ∈ ℝ) |
60 | 58, 59 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) → (𝑘 ∈ ℝ ∧ (♯‘𝑧) ∈
ℝ)) |
61 | | nn0re 12242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) |
62 | 60, 61 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℝ ∧
(♯‘𝑧) ∈
ℝ) ∧ 𝑚 ∈
ℝ)) |
63 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑘 ∈ ℝ ∧
(♯‘𝑧) ∈
ℝ) ∧ 𝑚 ∈
ℝ) → (♯‘𝑧) ∈ ℝ) |
64 | | readdcl 10955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ) → (𝑘 + 𝑚) ∈ ℝ) |
65 | 64 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑘 ∈ ℝ ∧
(♯‘𝑧) ∈
ℝ) ∧ 𝑚 ∈
ℝ) → (𝑘 + 𝑚) ∈
ℝ) |
66 | 63, 65 | ltnled 11122 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑘 ∈ ℝ ∧
(♯‘𝑧) ∈
ℝ) ∧ 𝑚 ∈
ℝ) → ((♯‘𝑧) < (𝑘 + 𝑚) ↔ ¬ (𝑘 + 𝑚) ≤ (♯‘𝑧))) |
67 | 63, 65 | posdifd 11562 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑘 ∈ ℝ ∧
(♯‘𝑧) ∈
ℝ) ∧ 𝑚 ∈
ℝ) → ((♯‘𝑧) < (𝑘 + 𝑚) ↔ 0 < ((𝑘 + 𝑚) − (♯‘𝑧)))) |
68 | 67 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑘 ∈ ℝ ∧
(♯‘𝑧) ∈
ℝ) ∧ 𝑚 ∈
ℝ) → ((♯‘𝑧) < (𝑘 + 𝑚) → 0 < ((𝑘 + 𝑚) − (♯‘𝑧)))) |
69 | 66, 68 | sylbird 259 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑘 ∈ ℝ ∧
(♯‘𝑧) ∈
ℝ) ∧ 𝑚 ∈
ℝ) → (¬ (𝑘 +
𝑚) ≤
(♯‘𝑧) → 0
< ((𝑘 + 𝑚) − (♯‘𝑧)))) |
70 | 62, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) ∧ 𝑚 ∈ ℕ0) → (¬
(𝑘 + 𝑚) ≤ (♯‘𝑧) → 0 < ((𝑘 + 𝑚) − (♯‘𝑧)))) |
71 | 70 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) → (𝑚 ∈ ℕ0 → (¬
(𝑘 + 𝑚) ≤ (♯‘𝑧) → 0 < ((𝑘 + 𝑚) − (♯‘𝑧))))) |
72 | 71 | 3adant3 1131 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0 ∧ 𝑘 ≤ (♯‘𝑧)) → (𝑚 ∈ ℕ0 → (¬
(𝑘 + 𝑚) ≤ (♯‘𝑧) → 0 < ((𝑘 + 𝑚) − (♯‘𝑧))))) |
73 | 57, 72 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈
(0...(♯‘𝑧))
→ (𝑚 ∈
ℕ0 → (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) → 0 < ((𝑘 + 𝑚) − (♯‘𝑧))))) |
74 | 6, 73 | mpan9 507 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
→ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) → 0 < ((𝑘 + 𝑚) − (♯‘𝑧)))) |
75 | 74 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝑘 + 𝑚) ≤ (♯‘𝑧) → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑘 ∈ (0...(♯‘𝑧))) → 0 < ((𝑘 + 𝑚) − (♯‘𝑧)))) |
76 | 75 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
(𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑘 ∈ (0...(♯‘𝑧))) → 0 < ((𝑘 + 𝑚) − (♯‘𝑧)))) |
77 | 76 | impcom 408 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → 0 < ((𝑘 + 𝑚) − (♯‘𝑧))) |
78 | | elnnz 12329 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ ℕ ↔ (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ ℤ ∧ 0 < ((𝑘 + 𝑚) − (♯‘𝑧)))) |
79 | 56, 77, 78 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → ((𝑘 + 𝑚) − (♯‘𝑧)) ∈ ℕ) |
80 | 79 | nnnn0d 12293 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → ((𝑘 + 𝑚) − (♯‘𝑧)) ∈
ℕ0) |
81 | 10 | ad2antlr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → (♯‘𝑧) ∈
ℕ0) |
82 | | cshwcsh2id.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦))) |
83 | | oveq2 7279 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑦) =
(♯‘𝑧) →
(0...(♯‘𝑦)) =
(0...(♯‘𝑧))) |
84 | 83 | eleq2d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑦) =
(♯‘𝑧) →
(𝑚 ∈
(0...(♯‘𝑦))
↔ 𝑚 ∈
(0...(♯‘𝑧)))) |
85 | 84 | anbi1d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑦) =
(♯‘𝑧) →
((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
↔ (𝑚 ∈
(0...(♯‘𝑧))
∧ 𝑘 ∈
(0...(♯‘𝑧))))) |
86 | | elfz2nn0 13346 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈
(0...(♯‘𝑧))
↔ (𝑚 ∈
ℕ0 ∧ (♯‘𝑧) ∈ ℕ0 ∧ 𝑚 ≤ (♯‘𝑧))) |
87 | 58 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) → 𝑘 ∈ ℝ) |
88 | 87, 61 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) ∧ 𝑚 ∈ ℕ0) → (𝑘 ∈ ℝ ∧ 𝑚 ∈
ℝ)) |
89 | 59, 59 | jca 512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((♯‘𝑧)
∈ ℕ0 → ((♯‘𝑧) ∈ ℝ ∧ (♯‘𝑧) ∈
ℝ)) |
90 | 89 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) ∧ 𝑚 ∈ ℕ0) →
((♯‘𝑧) ∈
ℝ ∧ (♯‘𝑧) ∈ ℝ)) |
91 | | le2add 11457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ) ∧
((♯‘𝑧) ∈
ℝ ∧ (♯‘𝑧) ∈ ℝ)) → ((𝑘 ≤ (♯‘𝑧) ∧ 𝑚 ≤ (♯‘𝑧)) → (𝑘 + 𝑚) ≤ ((♯‘𝑧) + (♯‘𝑧)))) |
92 | 88, 90, 91 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ≤ (♯‘𝑧) ∧ 𝑚 ≤ (♯‘𝑧)) → (𝑘 + 𝑚) ≤ ((♯‘𝑧) + (♯‘𝑧)))) |
93 | | nn0readdcl 12299 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑘 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (𝑘 + 𝑚) ∈ ℝ) |
94 | 93 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) ∧ 𝑚 ∈ ℕ0) → (𝑘 + 𝑚) ∈ ℝ) |
95 | 59 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) ∧ 𝑚 ∈ ℕ0) →
(♯‘𝑧) ∈
ℝ) |
96 | 94, 95, 95 | lesubadd2d 11574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) ∧ 𝑚 ∈ ℕ0) → (((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧) ↔ (𝑘 + 𝑚) ≤ ((♯‘𝑧) + (♯‘𝑧)))) |
97 | 92, 96 | sylibrd 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ≤ (♯‘𝑧) ∧ 𝑚 ≤ (♯‘𝑧)) → ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧))) |
98 | 97 | expcomd 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) ∧ 𝑚 ∈ ℕ0) → (𝑚 ≤ (♯‘𝑧) → (𝑘 ≤ (♯‘𝑧) → ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧)))) |
99 | 98 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) → (𝑚 ∈ ℕ0 → (𝑚 ≤ (♯‘𝑧) → (𝑘 ≤ (♯‘𝑧) → ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧))))) |
100 | 99 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0) → (𝑘 ≤ (♯‘𝑧) → (𝑚 ≤ (♯‘𝑧) → (𝑚 ∈ ℕ0 → ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧))))) |
101 | 100 | 3impia 1116 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0 ∧ 𝑘 ≤ (♯‘𝑧)) → (𝑚 ≤ (♯‘𝑧) → (𝑚 ∈ ℕ0 → ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧)))) |
102 | 101 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 ∈ ℕ0
→ (𝑚 ≤
(♯‘𝑧) →
((𝑘 ∈
ℕ0 ∧ (♯‘𝑧) ∈ ℕ0 ∧ 𝑘 ≤ (♯‘𝑧)) → ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧)))) |
103 | 102 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 ∈ ℕ0
∧ 𝑚 ≤
(♯‘𝑧)) →
((𝑘 ∈
ℕ0 ∧ (♯‘𝑧) ∈ ℕ0 ∧ 𝑘 ≤ (♯‘𝑧)) → ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧))) |
104 | 57, 103 | syl5bi 241 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 ∈ ℕ0
∧ 𝑚 ≤
(♯‘𝑧)) →
(𝑘 ∈
(0...(♯‘𝑧))
→ ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧))) |
105 | 104 | 3adant2 1130 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑚 ∈ ℕ0
∧ (♯‘𝑧)
∈ ℕ0 ∧ 𝑚 ≤ (♯‘𝑧)) → (𝑘 ∈ (0...(♯‘𝑧)) → ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧))) |
106 | 86, 105 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈
(0...(♯‘𝑧))
→ (𝑘 ∈
(0...(♯‘𝑧))
→ ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧))) |
107 | 106 | imp 407 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈
(0...(♯‘𝑧))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
→ ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧)) |
108 | 85, 107 | syl6bi 252 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑦) =
(♯‘𝑧) →
((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
→ ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧))) |
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((♯‘𝑦)
= (♯‘𝑧) ∧
(♯‘𝑥) =
(♯‘𝑦)) →
((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
→ ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧))) |
110 | 82, 109 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑘 ∈ (0...(♯‘𝑧))) → ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧))) |
111 | 110 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((¬
(𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑘 ∈ (0...(♯‘𝑧))) → ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧))) |
112 | 111 | impcom 408 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧)) |
113 | | elfz2nn0 13346 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧)) ↔ (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ ℕ0 ∧
(♯‘𝑧) ∈
ℕ0 ∧ ((𝑘 + 𝑚) − (♯‘𝑧)) ≤ (♯‘𝑧))) |
114 | 80, 81, 112, 113 | syl3anbrc 1342 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → ((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧))) |
115 | 114 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → ((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧))) |
116 | 16 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
(𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → 𝑧 ∈ Word 𝑉) |
117 | 116 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → 𝑧 ∈ Word 𝑉) |
118 | 19 | ad2antlr 724 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → 𝑘 ∈ ℤ) |
119 | 22 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → 𝑚 ∈ ℤ) |
120 | 117, 118,
119, 24 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → ((𝑧 cyclShift 𝑘) cyclShift 𝑚) = (𝑧 cyclShift (𝑘 + 𝑚))) |
121 | 19, 21, 43 | syl2anr 597 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
→ (𝑘 + 𝑚) ∈
ℤ) |
122 | | cshwsublen 14507 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ Word 𝑉 ∧ (𝑘 + 𝑚) ∈ ℤ) → (𝑧 cyclShift (𝑘 + 𝑚)) = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧)))) |
123 | 116, 121,
122 | syl2anr 597 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → (𝑧 cyclShift (𝑘 + 𝑚)) = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧)))) |
124 | 120, 123 | eqtrd 2780 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → ((𝑧 cyclShift 𝑘) cyclShift 𝑚) = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧)))) |
125 | 124 | eqeq2d 2751 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) → (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) ↔ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧))))) |
126 | 125 | biimpa 477 |
. . . . . . . . . . . 12
⊢ ((((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧)))) |
127 | 115, 126 | jca 512 |
. . . . . . . . . . 11
⊢ ((((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑘 ∈
(0...(♯‘𝑧)))
∧ (¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑)) ∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧))))) |
128 | 127 | exp41 435 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(0...(♯‘𝑦))
→ (𝑘 ∈
(0...(♯‘𝑧))
→ ((¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) → (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧)))))))) |
129 | 128 | com23 86 |
. . . . . . . . 9
⊢ (𝑚 ∈
(0...(♯‘𝑦))
→ ((¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → (𝑘 ∈ (0...(♯‘𝑧)) → (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) → (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧)))))))) |
130 | 129 | com24 95 |
. . . . . . . 8
⊢ (𝑚 ∈
(0...(♯‘𝑦))
→ (𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚) → (𝑘 ∈ (0...(♯‘𝑧)) → ((¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧)))))))) |
131 | 130 | imp 407 |
. . . . . . 7
⊢ ((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑥 = ((𝑧 cyclShift 𝑘) cyclShift 𝑚)) → (𝑘 ∈ (0...(♯‘𝑧)) → ((¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧))))))) |
132 | 3, 131 | syl6bi 252 |
. . . . . 6
⊢ (𝑦 = (𝑧 cyclShift 𝑘) → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (𝑘 ∈ (0...(♯‘𝑧)) → ((¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧)))))))) |
133 | 132 | com23 86 |
. . . . 5
⊢ (𝑦 = (𝑧 cyclShift 𝑘) → (𝑘 ∈ (0...(♯‘𝑧)) → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ((¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧)))))))) |
134 | 133 | impcom 408 |
. . . 4
⊢ ((𝑘 ∈
(0...(♯‘𝑧))
∧ 𝑦 = (𝑧 cyclShift 𝑘)) → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ((¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧))))))) |
135 | 134 | impcom 408 |
. . 3
⊢ (((𝑚 ∈
(0...(♯‘𝑦))
∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(♯‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ((¬ (𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → (((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧)))))) |
136 | | oveq2 7279 |
. . . 4
⊢ (𝑛 = ((𝑘 + 𝑚) − (♯‘𝑧)) → (𝑧 cyclShift 𝑛) = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧)))) |
137 | 136 | rspceeqv 3576 |
. . 3
⊢ ((((𝑘 + 𝑚) − (♯‘𝑧)) ∈ (0...(♯‘𝑧)) ∧ 𝑥 = (𝑧 cyclShift ((𝑘 + 𝑚) − (♯‘𝑧)))) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)) |
138 | 135, 137 | syl6com 37 |
. 2
⊢ ((¬
(𝑘 + 𝑚) ≤ (♯‘𝑧) ∧ 𝜑) → (((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(♯‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |
139 | 40, 138 | pm2.61ian 809 |
1
⊢ (𝜑 → (((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(♯‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) |