Step | Hyp | Ref
| Expression |
1 | | swrdcl 13271 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr 〈𝑀, 𝑁〉) ∈ Word 𝑉) |
2 | 1 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → (𝑊 substr 〈𝑀, 𝑁〉) ∈ Word 𝑉) |
3 | 2 | adantr 480 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 substr 〈𝑀, 𝑁〉) ∈ Word 𝑉) |
4 | | elfz0ubfz0 12312 |
. . . . 5
⊢ ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → 𝐾 ∈ (0...𝐿)) |
5 | 4 | adantl 481 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → 𝐾 ∈ (0...𝐿)) |
6 | | elfzuz 12209 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) → 𝐾 ∈
(ℤ≥‘0)) |
7 | 6 | adantl 481 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ 𝐾 ∈ (0...(𝑁 − 𝑀))) → 𝐾 ∈
(ℤ≥‘0)) |
8 | | fzss1 12251 |
. . . . . . . 8
⊢ (𝐾 ∈
(ℤ≥‘0) → (𝐾...(𝑁 − 𝑀)) ⊆ (0...(𝑁 − 𝑀))) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ 𝐾 ∈ (0...(𝑁 − 𝑀))) → (𝐾...(𝑁 − 𝑀)) ⊆ (0...(𝑁 − 𝑀))) |
10 | 9 | sseld 3567 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ 𝐾 ∈ (0...(𝑁 − 𝑀))) → (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → 𝐿 ∈ (0...(𝑁 − 𝑀)))) |
11 | 10 | impr 647 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → 𝐿 ∈ (0...(𝑁 − 𝑀))) |
12 | | 3ancomb 1040 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ↔ (𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊)))) |
13 | 12 | biimpi 205 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → (𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊)))) |
14 | 13 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊)))) |
15 | | swrdlen 13275 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) → (#‘(𝑊 substr 〈𝑀, 𝑁〉)) = (𝑁 − 𝑀)) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (#‘(𝑊 substr 〈𝑀, 𝑁〉)) = (𝑁 − 𝑀)) |
17 | 16 | oveq2d 6565 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (0...(#‘(𝑊 substr 〈𝑀, 𝑁〉))) = (0...(𝑁 − 𝑀))) |
18 | 11, 17 | eleqtrrd 2691 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → 𝐿 ∈ (0...(#‘(𝑊 substr 〈𝑀, 𝑁〉)))) |
19 | | swrdval2 13272 |
. . . 4
⊢ (((𝑊 substr 〈𝑀, 𝑁〉) ∈ Word 𝑉 ∧ 𝐾 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(#‘(𝑊 substr 〈𝑀, 𝑁〉)))) → ((𝑊 substr 〈𝑀, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)))) |
20 | 3, 5, 18, 19 | syl3anc 1318 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → ((𝑊 substr 〈𝑀, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)))) |
21 | | fvex 6113 |
. . . . . 6
⊢ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)) ∈ V |
22 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾))) = (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾))) |
23 | 21, 22 | fnmpti 5935 |
. . . . 5
⊢ (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾))) Fn (0..^(𝐿 − 𝐾)) |
24 | 23 | a1i 11 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾))) Fn (0..^(𝐿 − 𝐾))) |
25 | | swrdswrdlem 13311 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(#‘𝑊)))) |
26 | | swrdvalfn 13278 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(#‘𝑊))) → (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉) Fn (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) |
27 | 25, 26 | syl 17 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉) Fn (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) |
28 | | elfzelz 12213 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (0...𝑁) → 𝑀 ∈ ℤ) |
29 | | elfzelz 12213 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → 𝐿 ∈ ℤ) |
30 | | elfzelz 12213 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) → 𝐾 ∈ ℤ) |
31 | | zcn 11259 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝑀 ∈
ℂ) |
33 | | zcn 11259 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℂ) |
34 | 33 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝐿 ∈
ℂ) |
35 | | zcn 11259 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) |
36 | 35 | ad2antll 761 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝐾 ∈
ℂ) |
37 | | pnpcan 10199 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝑀 + 𝐿) − (𝑀 + 𝐾)) = (𝐿 − 𝐾)) |
38 | 37 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝐾 ∈ ℂ) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))) |
39 | 32, 34, 36, 38 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))) |
40 | 39 | expcom 450 |
. . . . . . . . . . 11
⊢ ((𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∈ ℤ → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) |
41 | 29, 30, 40 | syl2anr 494 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝑀 ∈ ℤ → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) |
42 | 28, 41 | syl5com 31 |
. . . . . . . . 9
⊢ (𝑀 ∈ (0...𝑁) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) |
43 | 42 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) |
44 | 43 | imp 444 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))) |
45 | 44 | oveq2d 6565 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (0..^(𝐿 − 𝐾)) = (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) |
46 | 45 | fneq2d 5896 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → ((𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉) Fn (0..^(𝐿 − 𝐾)) ↔ (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉) Fn (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾))))) |
47 | 27, 46 | mpbird 246 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉) Fn (0..^(𝐿 − 𝐾))) |
48 | | simpr 476 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → 𝑦 ∈ (0..^(𝐿 − 𝐾))) |
49 | | fvex 6113 |
. . . . . . 7
⊢ (𝑊‘((𝑦 + 𝐾) + 𝑀)) ∈ V |
50 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 + 𝐾) = (𝑦 + 𝐾)) |
51 | 50 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥 + 𝐾) + 𝑀) = ((𝑦 + 𝐾) + 𝑀)) |
52 | 51 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑊‘((𝑥 + 𝐾) + 𝑀)) = (𝑊‘((𝑦 + 𝐾) + 𝑀))) |
53 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀))) = (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀))) |
54 | 52, 53 | fvmptg 6189 |
. . . . . . 7
⊢ ((𝑦 ∈ (0..^(𝐿 − 𝐾)) ∧ (𝑊‘((𝑦 + 𝐾) + 𝑀)) ∈ V) → ((𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))‘𝑦) = (𝑊‘((𝑦 + 𝐾) + 𝑀))) |
55 | 48, 49, 54 | sylancl 693 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → ((𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))‘𝑦) = (𝑊‘((𝑦 + 𝐾) + 𝑀))) |
56 | | elfzoelz 12339 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0..^(𝐿 − 𝐾)) → 𝑦 ∈ ℤ) |
57 | | zcn 11259 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
58 | 57, 31, 35 | 3anim123i 1240 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑦 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈
ℂ)) |
59 | 58 | 3expa 1257 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝑦 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈
ℂ)) |
60 | | add32r 10134 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ) → (𝑦 + (𝑀 + 𝐾)) = ((𝑦 + 𝐾) + 𝑀)) |
61 | 60 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))) |
62 | 59, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))) |
63 | 62 | exp31 628 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℤ → (𝑀 ∈ ℤ → (𝐾 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))) |
64 | 63 | com13 86 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℤ → (𝑀 ∈ ℤ → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))) |
65 | 30, 64 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) → (𝑀 ∈ ℤ → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))) |
66 | 65 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝑀 ∈ ℤ → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))) |
67 | 28, 66 | syl5com 31 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (0...𝑁) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))) |
68 | 67 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))) |
69 | 68 | imp 444 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾)))) |
70 | 56, 69 | syl5com 31 |
. . . . . . . 8
⊢ (𝑦 ∈ (0..^(𝐿 − 𝐾)) → (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾)))) |
71 | 70 | impcom 445 |
. . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))) |
72 | 71 | fveq2d 6107 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → (𝑊‘((𝑦 + 𝐾) + 𝑀)) = (𝑊‘(𝑦 + (𝑀 + 𝐾)))) |
73 | 55, 72 | eqtrd 2644 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → ((𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))‘𝑦) = (𝑊‘(𝑦 + (𝑀 + 𝐾)))) |
74 | 13 | ad3antrrr 762 |
. . . . . . . 8
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐾))) → (𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊)))) |
75 | | elfz2nn0 12300 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) ↔ (𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0 ∧ 𝐾 ≤ (𝑁 − 𝑀))) |
76 | | elfz2 12204 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) ↔ ((𝐾 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)))) |
77 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↔ (𝑥 ∈ ℕ0 ∧ (𝐿 − 𝐾) ∈ ℕ ∧ 𝑥 < (𝐿 − 𝐾))) |
78 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℝ) |
79 | 78 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → 𝑥
∈ ℝ) |
80 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
81 | 80 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → 𝐾
∈ ℝ) |
82 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℝ) |
83 | 82 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → 𝐿
∈ ℝ) |
84 | | ltaddsub 10381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑥 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑥 + 𝐾) < 𝐿 ↔ 𝑥 < (𝐿 − 𝐾))) |
85 | 84 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑥 < (𝐿 − 𝐾) ↔ (𝑥 + 𝐾) < 𝐿)) |
86 | 79, 81, 83, 85 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → (𝑥
< (𝐿 − 𝐾) ↔ (𝑥 + 𝐾) < 𝐿)) |
87 | | nn0addcl 11205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑥 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑥 + 𝐾) ∈
ℕ0) |
88 | 87 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → (𝑥 + 𝐾) ∈
ℕ0)) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑥 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝐾 ∈
ℕ0 → (𝑥 + 𝐾) ∈
ℕ0)) |
90 | 89 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → (𝑥
+ 𝐾) ∈
ℕ0) |
91 | 90 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑥 ∈ ℕ0 ∧ 𝐿 ∈ ℤ)) ∧ (𝑥 + 𝐾) < 𝐿) ∧ (𝑁 − 𝑀) ∈ ℕ0) ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑥 + 𝐾) ∈
ℕ0) |
92 | | elnn0z 11267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑥 + 𝐾) ∈ ℕ0 ↔ ((𝑥 + 𝐾) ∈ ℤ ∧ 0 ≤ (𝑥 + 𝐾))) |
93 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → 0 ∈
ℝ) |
94 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑥 + 𝐾) ∈ ℤ → (𝑥 + 𝐾) ∈ ℝ) |
95 | 94 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑥 + 𝐾) ∈ ℝ) |
96 | 82 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐿 ∈ ℝ) |
97 | | lelttr 10007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((0
∈ ℝ ∧ (𝑥 +
𝐾) ∈ ℝ ∧
𝐿 ∈ ℝ) →
((0 ≤ (𝑥 + 𝐾) ∧ (𝑥 + 𝐾) < 𝐿) → 0 < 𝐿)) |
98 | 93, 95, 96, 97 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((0 ≤ (𝑥 + 𝐾) ∧ (𝑥 + 𝐾) < 𝐿) → 0 < 𝐿)) |
99 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝐿 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℕ0) → 0
∈ ℝ) |
100 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝐿 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℕ0) → 𝐿 ∈
ℝ) |
101 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑁 − 𝑀) ∈ ℕ0 → (𝑁 − 𝑀) ∈ ℝ) |
102 | 101 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝐿 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑁 − 𝑀) ∈ ℝ) |
103 | | ltletr 10008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((0
∈ ℝ ∧ 𝐿
∈ ℝ ∧ (𝑁
− 𝑀) ∈ ℝ)
→ ((0 < 𝐿 ∧
𝐿 ≤ (𝑁 − 𝑀)) → 0 < (𝑁 − 𝑀))) |
104 | 99, 100, 102, 103 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝐿 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℕ0) → ((0
< 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → 0 < (𝑁 − 𝑀))) |
105 | | elnnnn0b 11214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑁 − 𝑀) ∈ ℕ ↔ ((𝑁 − 𝑀) ∈ ℕ0 ∧ 0 <
(𝑁 − 𝑀))) |
106 | 105 | simplbi2 653 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑁 − 𝑀) ∈ ℕ0 → (0 <
(𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)) |
107 | 106 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝐿 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℕ0) → (0 <
(𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)) |
108 | 104, 107 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝐿 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℕ0) → ((0
< 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑁 − 𝑀) ∈ ℕ)) |
109 | 108 | exp4b 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝐿 ∈ ℤ → ((𝑁 − 𝑀) ∈ ℕ0 → (0 <
𝐿 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))) |
110 | 109 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝐿 ∈ ℤ → (0 <
𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))) |
111 | 110 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))) |
112 | 98, 111 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((0 ≤ (𝑥 + 𝐾) ∧ (𝑥 + 𝐾) < 𝐿) → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))) |
113 | 112 | expd 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤ (𝑥 + 𝐾) → ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ))))) |
114 | 113 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝑥 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)
→ (0 ≤ (𝑥 + 𝐾) → ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))))) |
115 | 114 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑥 + 𝐾) ∈ ℤ → (𝐿 ∈ ℤ → ((𝑥 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)
→ (0 ≤ (𝑥 + 𝐾) → ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ))))))) |
116 | 115 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑥 + 𝐾) ∈ ℤ → (0 ≤ (𝑥 + 𝐾) → ((𝑥 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)
→ (𝐿 ∈ ℤ
→ ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ))))))) |
117 | 116 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 0 ≤ (𝑥 + 𝐾)) → ((𝑥 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)
→ (𝐿 ∈ ℤ
→ ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))))) |
118 | 92, 117 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑥 + 𝐾) ∈ ℕ0 → ((𝑥 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝐿 ∈ ℤ → ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))))) |
119 | 87, 118 | mpcom 37 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑥 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝐿 ∈ ℤ → ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ))))) |
120 | 119 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑥 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝐾 ∈
ℕ0 → ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ))))) |
121 | 120 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → ((𝑥
+ 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))) |
122 | 121 | imp41 617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑥 ∈ ℕ0 ∧ 𝐿 ∈ ℤ)) ∧ (𝑥 + 𝐾) < 𝐿) ∧ (𝑁 − 𝑀) ∈ ℕ0) ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑁 − 𝑀) ∈ ℕ) |
123 | | nn0readdcl 11234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑥 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑥 + 𝐾) ∈ ℝ) |
124 | 123 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑥 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → (𝑥 + 𝐾) ∈ ℝ)) |
125 | 124 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑥 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝐾 ∈
ℕ0 → (𝑥 + 𝐾) ∈ ℝ)) |
126 | 125 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → (𝑥
+ 𝐾) ∈
ℝ) |
127 | 126 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ (𝑁
− 𝑀) ∈
ℕ0) → (𝑥 + 𝐾) ∈ ℝ) |
128 | 83 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ (𝑁
− 𝑀) ∈
ℕ0) → 𝐿 ∈ ℝ) |
129 | 101 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ (𝑁
− 𝑀) ∈
ℕ0) → (𝑁 − 𝑀) ∈ ℝ) |
130 | | ltletr 10008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑥 + 𝐾) ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (𝑁 − 𝑀) ∈ ℝ) → (((𝑥 + 𝐾) < 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑥 + 𝐾) < (𝑁 − 𝑀))) |
131 | 127, 128,
129, 130 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ (𝑁
− 𝑀) ∈
ℕ0) → (((𝑥 + 𝐾) < 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑥 + 𝐾) < (𝑁 − 𝑀))) |
132 | 131 | exp4b 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → ((𝑁
− 𝑀) ∈
ℕ0 → ((𝑥 + 𝐾) < 𝐿 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) < (𝑁 − 𝑀))))) |
133 | 132 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → ((𝑥
+ 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) < (𝑁 − 𝑀))))) |
134 | 133 | imp41 617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑥 ∈ ℕ0 ∧ 𝐿 ∈ ℤ)) ∧ (𝑥 + 𝐾) < 𝐿) ∧ (𝑁 − 𝑀) ∈ ℕ0) ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑥 + 𝐾) < (𝑁 − 𝑀)) |
135 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)) ↔ ((𝑥 + 𝐾) ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ (𝑥 + 𝐾) < (𝑁 − 𝑀))) |
136 | 91, 122, 134, 135 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑥 ∈ ℕ0 ∧ 𝐿 ∈ ℤ)) ∧ (𝑥 + 𝐾) < 𝐿) ∧ (𝑁 − 𝑀) ∈ ℕ0) ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))) |
137 | 136 | exp41 636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → ((𝑥
+ 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) |
138 | 86, 137 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → (𝑥
< (𝐿 − 𝐾) → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) |
139 | 138 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐾 ∈ ℕ0
→ ((𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ) → (𝑥
< (𝐿 − 𝐾) → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))))) |
140 | 139 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐾 ∈ ℕ0
→ ((𝑁 − 𝑀) ∈ ℕ0
→ (𝑥 < (𝐿 − 𝐾) → ((𝑥 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))))) |
141 | 140 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐾 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ0)
→ (𝑥 < (𝐿 − 𝐾) → ((𝑥 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) |
142 | 141 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝑥 < (𝐿 − 𝐾) → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) |
143 | 142 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℕ0
∧ 𝑥 < (𝐿 − 𝐾)) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) |
144 | 143 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℕ0
∧ (𝐿 − 𝐾) ∈ ℕ ∧ 𝑥 < (𝐿 − 𝐾)) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) |
145 | 77, 144 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) |
146 | 145 | com14 94 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 ≤ (𝑁 − 𝑀) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) |
147 | 146 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) |
148 | 147 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿 ∈ ℤ → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) |
149 | 148 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) |
150 | 149 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀))) → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))) |
151 | 76, 150 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))) |
152 | 151 | com12 32 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ0)
→ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))) |
153 | 152 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ0
∧ 𝐾 ≤ (𝑁 − 𝑀)) → (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))) |
154 | 75, 153 | sylbi 206 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) → (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))) |
155 | 154 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))) |
156 | 155 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))) |
157 | 156 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))) |
158 | 157 | imp 444 |
. . . . . . . 8
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐾))) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))) |
159 | | swrdfv 13276 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))) → ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)) = (𝑊‘((𝑥 + 𝐾) + 𝑀))) |
160 | 74, 158, 159 | syl2anc 691 |
. . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐾))) → ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)) = (𝑊‘((𝑥 + 𝐾) + 𝑀))) |
161 | 160 | mpteq2dva 4672 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾))) = (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))) |
162 | 161 | fveq1d 6105 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → ((𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)))‘𝑦) = ((𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))‘𝑦)) |
163 | 25 | adantr 480 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(#‘𝑊)))) |
164 | 31, 33, 35 | 3anim123i 1240 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝐾 ∈
ℂ)) |
165 | 164 | 3expa 1257 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝐾 ∈
ℂ)) |
166 | 165, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))) |
167 | 166 | exp31 628 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℤ → (𝐿 ∈ ℤ → (𝐾 ∈ ℤ → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))) |
168 | 167 | com3l 87 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∈ ℤ → (𝐾 ∈ ℤ → (𝑀 ∈ ℤ → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))) |
169 | 29, 168 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → (𝐾 ∈ ℤ → (𝑀 ∈ ℤ → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))) |
170 | 30, 169 | mpan9 485 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝑀 ∈ ℤ → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) |
171 | 28, 170 | syl5com 31 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (0...𝑁) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) |
172 | 171 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) |
173 | 172 | imp 444 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))) |
174 | 173 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (0..^(𝐿 − 𝐾)) = (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) |
175 | 174 | eleq2d 2673 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑦 ∈ (0..^(𝐿 − 𝐾)) ↔ 𝑦 ∈ (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾))))) |
176 | 175 | biimpa 500 |
. . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → 𝑦 ∈ (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) |
177 | | swrdfv 13276 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(#‘𝑊))) ∧ 𝑦 ∈ (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) → ((𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉)‘𝑦) = (𝑊‘(𝑦 + (𝑀 + 𝐾)))) |
178 | 163, 176,
177 | syl2anc 691 |
. . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → ((𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉)‘𝑦) = (𝑊‘(𝑦 + (𝑀 + 𝐾)))) |
179 | 73, 162, 178 | 3eqtr4d 2654 |
. . . 4
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → ((𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)))‘𝑦) = ((𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉)‘𝑦)) |
180 | 24, 47, 179 | eqfnfvd 6222 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾))) = (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉)) |
181 | 20, 180 | eqtrd 2644 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → ((𝑊 substr 〈𝑀, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉)) |
182 | 181 | ex 449 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → ((𝑊 substr 〈𝑀, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉))) |