| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | swrdcl 14684 | . . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr 〈𝑀, 𝑁〉) ∈ Word 𝑉) | 
| 2 | 1 | 3ad2ant1 1133 | . . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → (𝑊 substr 〈𝑀, 𝑁〉) ∈ Word 𝑉) | 
| 3 | 2 | adantr 480 | . . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 substr 〈𝑀, 𝑁〉) ∈ Word 𝑉) | 
| 4 |  | elfz0ubfz0 13673 | . . . . 5
⊢ ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → 𝐾 ∈ (0...𝐿)) | 
| 5 | 4 | adantl 481 | . . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → 𝐾 ∈ (0...𝐿)) | 
| 6 |  | elfzuz 13561 | . . . . . . . . 9
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) → 𝐾 ∈
(ℤ≥‘0)) | 
| 7 | 6 | adantl 481 | . . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ 𝐾 ∈ (0...(𝑁 − 𝑀))) → 𝐾 ∈
(ℤ≥‘0)) | 
| 8 |  | fzss1 13604 | . . . . . . . 8
⊢ (𝐾 ∈
(ℤ≥‘0) → (𝐾...(𝑁 − 𝑀)) ⊆ (0...(𝑁 − 𝑀))) | 
| 9 | 7, 8 | syl 17 | . . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ 𝐾 ∈ (0...(𝑁 − 𝑀))) → (𝐾...(𝑁 − 𝑀)) ⊆ (0...(𝑁 − 𝑀))) | 
| 10 | 9 | sseld 3981 | . . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ 𝐾 ∈ (0...(𝑁 − 𝑀))) → (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → 𝐿 ∈ (0...(𝑁 − 𝑀)))) | 
| 11 | 10 | impr 454 | . . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → 𝐿 ∈ (0...(𝑁 − 𝑀))) | 
| 12 |  | 3ancomb 1098 | . . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ↔ (𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) | 
| 13 | 12 | biimpi 216 | . . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → (𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) | 
| 14 | 13 | adantr 480 | . . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) | 
| 15 |  | swrdlen 14686 | . . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr 〈𝑀, 𝑁〉)) = (𝑁 − 𝑀)) | 
| 16 | 14, 15 | syl 17 | . . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (♯‘(𝑊 substr 〈𝑀, 𝑁〉)) = (𝑁 − 𝑀)) | 
| 17 | 16 | oveq2d 7448 | . . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (0...(♯‘(𝑊 substr 〈𝑀, 𝑁〉))) = (0...(𝑁 − 𝑀))) | 
| 18 | 11, 17 | eleqtrrd 2843 | . . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → 𝐿 ∈ (0...(♯‘(𝑊 substr 〈𝑀, 𝑁〉)))) | 
| 19 |  | swrdval2 14685 | . . . 4
⊢ (((𝑊 substr 〈𝑀, 𝑁〉) ∈ Word 𝑉 ∧ 𝐾 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘(𝑊 substr 〈𝑀, 𝑁〉)))) → ((𝑊 substr 〈𝑀, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)))) | 
| 20 | 3, 5, 18, 19 | syl3anc 1372 | . . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → ((𝑊 substr 〈𝑀, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)))) | 
| 21 |  | fvex 6918 | . . . . . 6
⊢ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)) ∈ V | 
| 22 |  | eqid 2736 | . . . . . 6
⊢ (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾))) = (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾))) | 
| 23 | 21, 22 | fnmpti 6710 | . . . . 5
⊢ (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾))) Fn (0..^(𝐿 − 𝐾)) | 
| 24 | 23 | a1i 11 | . . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾))) Fn (0..^(𝐿 − 𝐾))) | 
| 25 |  | swrdswrdlem 14743 | . . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(♯‘𝑊)))) | 
| 26 |  | swrdvalfn 14690 | . . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(♯‘𝑊))) → (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉) Fn (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) | 
| 27 | 25, 26 | syl 17 | . . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉) Fn (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) | 
| 28 |  | elfzelz 13565 | . . . . . . . . . 10
⊢ (𝑀 ∈ (0...𝑁) → 𝑀 ∈ ℤ) | 
| 29 |  | elfzelz 13565 | . . . . . . . . . . 11
⊢ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → 𝐿 ∈ ℤ) | 
| 30 |  | elfzelz 13565 | . . . . . . . . . . 11
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) → 𝐾 ∈ ℤ) | 
| 31 |  | zcn 12620 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) | 
| 32 | 31 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝑀 ∈
ℂ) | 
| 33 |  | zcn 12620 | . . . . . . . . . . . . . 14
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℂ) | 
| 34 | 33 | ad2antrl 728 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝐿 ∈
ℂ) | 
| 35 |  | zcn 12620 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) | 
| 36 | 35 | ad2antll 729 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝐾 ∈
ℂ) | 
| 37 |  | pnpcan 11549 | . . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝑀 + 𝐿) − (𝑀 + 𝐾)) = (𝐿 − 𝐾)) | 
| 38 | 37 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝐾 ∈ ℂ) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))) | 
| 39 | 32, 34, 36, 38 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))) | 
| 40 | 39 | expcom 413 | . . . . . . . . . . 11
⊢ ((𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∈ ℤ → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) | 
| 41 | 29, 30, 40 | syl2anr 597 | . . . . . . . . . 10
⊢ ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝑀 ∈ ℤ → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) | 
| 42 | 28, 41 | syl5com 31 | . . . . . . . . 9
⊢ (𝑀 ∈ (0...𝑁) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) | 
| 43 | 42 | 3ad2ant3 1135 | . . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) | 
| 44 | 43 | imp 406 | . . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))) | 
| 45 | 44 | oveq2d 7448 | . . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (0..^(𝐿 − 𝐾)) = (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) | 
| 46 | 45 | fneq2d 6661 | . . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → ((𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉) Fn (0..^(𝐿 − 𝐾)) ↔ (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉) Fn (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾))))) | 
| 47 | 27, 46 | mpbird 257 | . . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉) Fn (0..^(𝐿 − 𝐾))) | 
| 48 |  | simpr 484 | . . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → 𝑦 ∈ (0..^(𝐿 − 𝐾))) | 
| 49 |  | fvex 6918 | . . . . . . 7
⊢ (𝑊‘((𝑦 + 𝐾) + 𝑀)) ∈ V | 
| 50 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 + 𝐾) = (𝑦 + 𝐾)) | 
| 51 | 50 | fvoveq1d 7454 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑊‘((𝑥 + 𝐾) + 𝑀)) = (𝑊‘((𝑦 + 𝐾) + 𝑀))) | 
| 52 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀))) = (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀))) | 
| 53 | 51, 52 | fvmptg 7013 | . . . . . . 7
⊢ ((𝑦 ∈ (0..^(𝐿 − 𝐾)) ∧ (𝑊‘((𝑦 + 𝐾) + 𝑀)) ∈ V) → ((𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))‘𝑦) = (𝑊‘((𝑦 + 𝐾) + 𝑀))) | 
| 54 | 48, 49, 53 | sylancl 586 | . . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → ((𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))‘𝑦) = (𝑊‘((𝑦 + 𝐾) + 𝑀))) | 
| 55 |  | zcn 12620 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) | 
| 56 | 55, 31, 35 | 3anim123i 1151 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑦 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈
ℂ)) | 
| 57 | 56 | 3expa 1118 | . . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝑦 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈
ℂ)) | 
| 58 |  | add32r 11482 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ) → (𝑦 + (𝑀 + 𝐾)) = ((𝑦 + 𝐾) + 𝑀)) | 
| 59 | 58 | eqcomd 2742 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))) | 
| 60 | 57, 59 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))) | 
| 61 | 60 | exp31 419 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℤ → (𝑀 ∈ ℤ → (𝐾 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))) | 
| 62 | 61 | com13 88 | . . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℤ → (𝑀 ∈ ℤ → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))) | 
| 63 | 30, 62 | syl 17 | . . . . . . . . . . . 12
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) → (𝑀 ∈ ℤ → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))) | 
| 64 | 63 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝑀 ∈ ℤ → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))) | 
| 65 | 28, 64 | syl5com 31 | . . . . . . . . . 10
⊢ (𝑀 ∈ (0...𝑁) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))) | 
| 66 | 65 | 3ad2ant3 1135 | . . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))))) | 
| 67 | 66 | imp 406 | . . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑦 ∈ ℤ → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾)))) | 
| 68 |  | elfzoelz 13700 | . . . . . . . 8
⊢ (𝑦 ∈ (0..^(𝐿 − 𝐾)) → 𝑦 ∈ ℤ) | 
| 69 | 67, 68 | impel 505 | . . . . . . 7
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → ((𝑦 + 𝐾) + 𝑀) = (𝑦 + (𝑀 + 𝐾))) | 
| 70 | 69 | fveq2d 6909 | . . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → (𝑊‘((𝑦 + 𝐾) + 𝑀)) = (𝑊‘(𝑦 + (𝑀 + 𝐾)))) | 
| 71 | 54, 70 | eqtrd 2776 | . . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → ((𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))‘𝑦) = (𝑊‘(𝑦 + (𝑀 + 𝐾)))) | 
| 72 | 13 | ad3antrrr 730 | . . . . . . . 8
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐾))) → (𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊)))) | 
| 73 |  | elfz2nn0 13659 | . . . . . . . . . . . . 13
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) ↔ (𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0 ∧ 𝐾 ≤ (𝑁 − 𝑀))) | 
| 74 |  | elfz2 13555 | . . . . . . . . . . . . . . . 16
⊢ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) ↔ ((𝐾 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)))) | 
| 75 |  | elfzo0 13741 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↔ (𝑥 ∈ ℕ0 ∧ (𝐿 − 𝐾) ∈ ℕ ∧ 𝑥 < (𝐿 − 𝐾))) | 
| 76 |  | nn0re 12537 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℝ) | 
| 77 | 76 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → 𝑥
∈ ℝ) | 
| 78 |  | nn0re 12537 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) | 
| 79 | 78 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → 𝐾
∈ ℝ) | 
| 80 |  | zre 12619 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℝ) | 
| 81 | 80 | ad2antll 729 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → 𝐿
∈ ℝ) | 
| 82 |  | ltaddsub 11738 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑥 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑥 + 𝐾) < 𝐿 ↔ 𝑥 < (𝐿 − 𝐾))) | 
| 83 | 82 | bicomd 223 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑥 < (𝐿 − 𝐾) ↔ (𝑥 + 𝐾) < 𝐿)) | 
| 84 | 77, 79, 81, 83 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → (𝑥
< (𝐿 − 𝐾) ↔ (𝑥 + 𝐾) < 𝐿)) | 
| 85 |  | nn0addcl 12563 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑥 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑥 + 𝐾) ∈
ℕ0) | 
| 86 | 85 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → (𝑥 + 𝐾) ∈
ℕ0)) | 
| 87 | 86 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑥 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝐾 ∈
ℕ0 → (𝑥 + 𝐾) ∈
ℕ0)) | 
| 88 | 87 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → (𝑥
+ 𝐾) ∈
ℕ0) | 
| 89 | 88 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑥 ∈ ℕ0 ∧ 𝐿 ∈ ℤ)) ∧ (𝑥 + 𝐾) < 𝐿) ∧ (𝑁 − 𝑀) ∈ ℕ0) ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑥 + 𝐾) ∈
ℕ0) | 
| 90 |  | elnn0z 12628 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑥 + 𝐾) ∈ ℕ0 ↔ ((𝑥 + 𝐾) ∈ ℤ ∧ 0 ≤ (𝑥 + 𝐾))) | 
| 91 |  | 0red 11265 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → 0 ∈
ℝ) | 
| 92 |  | zre 12619 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑥 + 𝐾) ∈ ℤ → (𝑥 + 𝐾) ∈ ℝ) | 
| 93 | 92 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑥 + 𝐾) ∈ ℝ) | 
| 94 | 80 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐿 ∈ ℝ) | 
| 95 |  | lelttr 11352 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((0
∈ ℝ ∧ (𝑥 +
𝐾) ∈ ℝ ∧
𝐿 ∈ ℝ) →
((0 ≤ (𝑥 + 𝐾) ∧ (𝑥 + 𝐾) < 𝐿) → 0 < 𝐿)) | 
| 96 | 91, 93, 94, 95 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((0 ≤ (𝑥 + 𝐾) ∧ (𝑥 + 𝐾) < 𝐿) → 0 < 𝐿)) | 
| 97 |  | 0red 11265 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝐿 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℕ0) → 0
∈ ℝ) | 
| 98 | 80 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝐿 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℕ0) → 𝐿 ∈
ℝ) | 
| 99 |  | nn0re 12537 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑁 − 𝑀) ∈ ℕ0 → (𝑁 − 𝑀) ∈ ℝ) | 
| 100 | 99 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝐿 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑁 − 𝑀) ∈ ℝ) | 
| 101 |  | ltletr 11354 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((0
∈ ℝ ∧ 𝐿
∈ ℝ ∧ (𝑁
− 𝑀) ∈ ℝ)
→ ((0 < 𝐿 ∧
𝐿 ≤ (𝑁 − 𝑀)) → 0 < (𝑁 − 𝑀))) | 
| 102 | 97, 98, 100, 101 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝐿 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℕ0) → ((0
< 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → 0 < (𝑁 − 𝑀))) | 
| 103 |  | elnnnn0b 12572 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑁 − 𝑀) ∈ ℕ ↔ ((𝑁 − 𝑀) ∈ ℕ0 ∧ 0 <
(𝑁 − 𝑀))) | 
| 104 | 103 | simplbi2 500 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑁 − 𝑀) ∈ ℕ0 → (0 <
(𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)) | 
| 105 | 104 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝐿 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℕ0) → (0 <
(𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)) | 
| 106 | 102, 105 | syld 47 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝐿 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℕ0) → ((0
< 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑁 − 𝑀) ∈ ℕ)) | 
| 107 | 106 | exp4b 430 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝐿 ∈ ℤ → ((𝑁 − 𝑀) ∈ ℕ0 → (0 <
𝐿 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))) | 
| 108 | 107 | com23 86 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝐿 ∈ ℤ → (0 <
𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))) | 
| 109 | 108 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))) | 
| 110 | 96, 109 | syld 47 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((0 ≤ (𝑥 + 𝐾) ∧ (𝑥 + 𝐾) < 𝐿) → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))) | 
| 111 | 110 | expd 415 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤ (𝑥 + 𝐾) → ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ))))) | 
| 112 | 111 | a1d 25 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝑥 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)
→ (0 ≤ (𝑥 + 𝐾) → ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))))) | 
| 113 | 112 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑥 + 𝐾) ∈ ℤ → (𝐿 ∈ ℤ → ((𝑥 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)
→ (0 ≤ (𝑥 + 𝐾) → ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ))))))) | 
| 114 | 113 | com24 95 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑥 + 𝐾) ∈ ℤ → (0 ≤ (𝑥 + 𝐾) → ((𝑥 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)
→ (𝐿 ∈ ℤ
→ ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ))))))) | 
| 115 | 114 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑥 + 𝐾) ∈ ℤ ∧ 0 ≤ (𝑥 + 𝐾)) → ((𝑥 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0)
→ (𝐿 ∈ ℤ
→ ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))))) | 
| 116 | 90, 115 | sylbi 217 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑥 + 𝐾) ∈ ℕ0 → ((𝑥 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝐿 ∈ ℤ → ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))))) | 
| 117 | 85, 116 | mpcom 38 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑥 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝐿 ∈ ℤ → ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ))))) | 
| 118 | 117 | impancom 451 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑥 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝐾 ∈
ℕ0 → ((𝑥 + 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ))))) | 
| 119 | 118 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → ((𝑥
+ 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 − 𝑀) ∈ ℕ)))) | 
| 120 | 119 | imp41 425 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑥 ∈ ℕ0 ∧ 𝐿 ∈ ℤ)) ∧ (𝑥 + 𝐾) < 𝐿) ∧ (𝑁 − 𝑀) ∈ ℕ0) ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑁 − 𝑀) ∈ ℕ) | 
| 121 |  | nn0readdcl 12595 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑥 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑥 + 𝐾) ∈ ℝ) | 
| 122 | 121 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑥 ∈ ℕ0
→ (𝐾 ∈
ℕ0 → (𝑥 + 𝐾) ∈ ℝ)) | 
| 123 | 122 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑥 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝐾 ∈
ℕ0 → (𝑥 + 𝐾) ∈ ℝ)) | 
| 124 | 123 | impcom 407 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → (𝑥
+ 𝐾) ∈
ℝ) | 
| 125 |  | ltletr 11354 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑥 + 𝐾) ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (𝑁 − 𝑀) ∈ ℝ) → (((𝑥 + 𝐾) < 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑥 + 𝐾) < (𝑁 − 𝑀))) | 
| 126 | 124, 81, 99, 125 | syl2an3an 1423 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ (𝑁
− 𝑀) ∈
ℕ0) → (((𝑥 + 𝐾) < 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑥 + 𝐾) < (𝑁 − 𝑀))) | 
| 127 | 126 | exp4b 430 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → ((𝑁
− 𝑀) ∈
ℕ0 → ((𝑥 + 𝐾) < 𝐿 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) < (𝑁 − 𝑀))))) | 
| 128 | 127 | com23 86 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → ((𝑥
+ 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) < (𝑁 − 𝑀))))) | 
| 129 | 128 | imp41 425 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑥 ∈ ℕ0 ∧ 𝐿 ∈ ℤ)) ∧ (𝑥 + 𝐾) < 𝐿) ∧ (𝑁 − 𝑀) ∈ ℕ0) ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑥 + 𝐾) < (𝑁 − 𝑀)) | 
| 130 |  | elfzo0 13741 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)) ↔ ((𝑥 + 𝐾) ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ (𝑥 + 𝐾) < (𝑁 − 𝑀))) | 
| 131 | 89, 120, 129, 130 | syl3anbrc 1343 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝐾 ∈
ℕ0 ∧ (𝑥 ∈ ℕ0 ∧ 𝐿 ∈ ℤ)) ∧ (𝑥 + 𝐾) < 𝐿) ∧ (𝑁 − 𝑀) ∈ ℕ0) ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))) | 
| 132 | 131 | exp41 434 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → ((𝑥
+ 𝐾) < 𝐿 → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) | 
| 133 | 84, 132 | sylbid 240 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐾 ∈ ℕ0
∧ (𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → (𝑥
< (𝐿 − 𝐾) → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) | 
| 134 | 133 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐾 ∈ ℕ0
→ ((𝑥 ∈
ℕ0 ∧ 𝐿
∈ ℤ) → (𝑥
< (𝐿 − 𝐾) → ((𝑁 − 𝑀) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))))) | 
| 135 | 134 | com24 95 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐾 ∈ ℕ0
→ ((𝑁 − 𝑀) ∈ ℕ0
→ (𝑥 < (𝐿 − 𝐾) → ((𝑥 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))))) | 
| 136 | 135 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐾 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ0)
→ (𝑥 < (𝐿 − 𝐾) → ((𝑥 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) | 
| 137 | 136 | com13 88 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝑥 < (𝐿 − 𝐾) → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) | 
| 138 | 137 | impancom 451 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℕ0
∧ 𝑥 < (𝐿 − 𝐾)) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) | 
| 139 | 138 | 3adant2 1131 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℕ0
∧ (𝐿 − 𝐾) ∈ ℕ ∧ 𝑥 < (𝐿 − 𝐾)) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) | 
| 140 | 75, 139 | sylbi 217 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝐿 ≤ (𝑁 − 𝑀) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) | 
| 141 | 140 | com14 96 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 ≤ (𝑁 − 𝑀) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) | 
| 142 | 141 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝐿 ∈ ℤ → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) | 
| 143 | 142 | com12 32 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐿 ∈ ℤ → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) | 
| 144 | 143 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))))) | 
| 145 | 144 | imp 406 | . . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀))) → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))) | 
| 146 | 74, 145 | sylbi 217 | . . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))) | 
| 147 | 146 | com12 32 | . . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ0)
→ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))) | 
| 148 | 147 | 3adant3 1132 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ0
∧ 𝐾 ≤ (𝑁 − 𝑀)) → (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))) | 
| 149 | 73, 148 | sylbi 217 | . . . . . . . . . . . 12
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) → (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))))) | 
| 150 | 149 | imp 406 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))) | 
| 151 | 150 | adantl 481 | . . . . . . . . . 10
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))) | 
| 152 | 151 | adantr 480 | . . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀)))) | 
| 153 | 152 | imp 406 | . . . . . . . 8
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐾))) → (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))) | 
| 154 |  | swrdfv 14687 | . . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ (𝑥 + 𝐾) ∈ (0..^(𝑁 − 𝑀))) → ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)) = (𝑊‘((𝑥 + 𝐾) + 𝑀))) | 
| 155 | 72, 153, 154 | syl2anc 584 | . . . . . . 7
⊢
(((((𝑊 ∈ Word
𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) ∧ 𝑥 ∈ (0..^(𝐿 − 𝐾))) → ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)) = (𝑊‘((𝑥 + 𝐾) + 𝑀))) | 
| 156 | 155 | mpteq2dva 5241 | . . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾))) = (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))) | 
| 157 | 156 | fveq1d 6907 | . . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → ((𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)))‘𝑦) = ((𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ (𝑊‘((𝑥 + 𝐾) + 𝑀)))‘𝑦)) | 
| 158 | 25 | adantr 480 | . . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(♯‘𝑊)))) | 
| 159 | 31, 33, 35 | 3anim123i 1151 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝐾 ∈
ℂ)) | 
| 160 | 159 | 3expa 1118 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ∧ 𝐾 ∈
ℂ)) | 
| 161 | 160, 38 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))) | 
| 162 | 161 | exp31 419 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℤ → (𝐿 ∈ ℤ → (𝐾 ∈ ℤ → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))) | 
| 163 | 162 | com3l 89 | . . . . . . . . . . . . . 14
⊢ (𝐿 ∈ ℤ → (𝐾 ∈ ℤ → (𝑀 ∈ ℤ → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))) | 
| 164 | 29, 163 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → (𝐾 ∈ ℤ → (𝑀 ∈ ℤ → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))))) | 
| 165 | 30, 164 | mpan9 506 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝑀 ∈ ℤ → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) | 
| 166 | 28, 165 | syl5com 31 | . . . . . . . . . . 11
⊢ (𝑀 ∈ (0...𝑁) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) | 
| 167 | 166 | 3ad2ant3 1135 | . . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾)))) | 
| 168 | 167 | imp 406 | . . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝐿 − 𝐾) = ((𝑀 + 𝐿) − (𝑀 + 𝐾))) | 
| 169 | 168 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (0..^(𝐿 − 𝐾)) = (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) | 
| 170 | 169 | eleq2d 2826 | . . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑦 ∈ (0..^(𝐿 − 𝐾)) ↔ 𝑦 ∈ (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾))))) | 
| 171 | 170 | biimpa 476 | . . . . . 6
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → 𝑦 ∈ (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) | 
| 172 |  | swrdfv 14687 | . . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(♯‘𝑊))) ∧ 𝑦 ∈ (0..^((𝑀 + 𝐿) − (𝑀 + 𝐾)))) → ((𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉)‘𝑦) = (𝑊‘(𝑦 + (𝑀 + 𝐾)))) | 
| 173 | 158, 171,
172 | syl2anc 584 | . . . . 5
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → ((𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉)‘𝑦) = (𝑊‘(𝑦 + (𝑀 + 𝐾)))) | 
| 174 | 71, 157, 173 | 3eqtr4d 2786 | . . . 4
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) ∧ 𝑦 ∈ (0..^(𝐿 − 𝐾))) → ((𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾)))‘𝑦) = ((𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉)‘𝑦)) | 
| 175 | 24, 47, 174 | eqfnfvd 7053 | . . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑥 ∈ (0..^(𝐿 − 𝐾)) ↦ ((𝑊 substr 〈𝑀, 𝑁〉)‘(𝑥 + 𝐾))) = (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉)) | 
| 176 | 20, 175 | eqtrd 2776 | . 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → ((𝑊 substr 〈𝑀, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉)) | 
| 177 | 176 | ex 412 | 1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → ((𝑊 substr 〈𝑀, 𝑁〉) substr 〈𝐾, 𝐿〉) = (𝑊 substr 〈(𝑀 + 𝐾), (𝑀 + 𝐿)〉))) |