Step | Hyp | Ref
| Expression |
1 | | swrdccatin12.l |
. . . . . . . 8
⊢ 𝐿 = (#‘𝐴) |
2 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝐿 = (#‘𝐴) → (𝐿...𝑁) = ((#‘𝐴)...𝑁)) |
3 | 2 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝐿 = (#‘𝐴) → (𝑀 ∈ (𝐿...𝑁) ↔ 𝑀 ∈ ((#‘𝐴)...𝑁))) |
4 | | id 22 |
. . . . . . . . . . 11
⊢ (𝐿 = (#‘𝐴) → 𝐿 = (#‘𝐴)) |
5 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝐿 = (#‘𝐴) → (𝐿 + (#‘𝐵)) = ((#‘𝐴) + (#‘𝐵))) |
6 | 4, 5 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝐿 = (#‘𝐴) → (𝐿...(𝐿 + (#‘𝐵))) = ((#‘𝐴)...((#‘𝐴) + (#‘𝐵)))) |
7 | 6 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝐿 = (#‘𝐴) → (𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))) ↔ 𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵))))) |
8 | 3, 7 | anbi12d 743 |
. . . . . . . 8
⊢ (𝐿 = (#‘𝐴) → ((𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) ↔ (𝑀 ∈ ((#‘𝐴)...𝑁) ∧ 𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵)))))) |
9 | 1, 8 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) ↔ (𝑀 ∈ ((#‘𝐴)...𝑁) ∧ 𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵))))) |
10 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈
ℕ0) |
11 | | elnn0uz 11601 |
. . . . . . . . . . . . 13
⊢
((#‘𝐴) ∈
ℕ0 ↔ (#‘𝐴) ∈
(ℤ≥‘0)) |
12 | 11 | biimpi 205 |
. . . . . . . . . . . 12
⊢
((#‘𝐴) ∈
ℕ0 → (#‘𝐴) ∈
(ℤ≥‘0)) |
13 | | fzss1 12251 |
. . . . . . . . . . . 12
⊢
((#‘𝐴) ∈
(ℤ≥‘0) → ((#‘𝐴)...𝑁) ⊆ (0...𝑁)) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
⊢
((#‘𝐴) ∈
ℕ0 → ((#‘𝐴)...𝑁) ⊆ (0...𝑁)) |
15 | 14 | sseld 3567 |
. . . . . . . . . 10
⊢
((#‘𝐴) ∈
ℕ0 → (𝑀 ∈ ((#‘𝐴)...𝑁) → 𝑀 ∈ (0...𝑁))) |
16 | | fzss1 12251 |
. . . . . . . . . . . 12
⊢
((#‘𝐴) ∈
(ℤ≥‘0) → ((#‘𝐴)...((#‘𝐴) + (#‘𝐵))) ⊆ (0...((#‘𝐴) + (#‘𝐵)))) |
17 | 12, 16 | syl 17 |
. . . . . . . . . . 11
⊢
((#‘𝐴) ∈
ℕ0 → ((#‘𝐴)...((#‘𝐴) + (#‘𝐵))) ⊆ (0...((#‘𝐴) + (#‘𝐵)))) |
18 | 17 | sseld 3567 |
. . . . . . . . . 10
⊢
((#‘𝐴) ∈
ℕ0 → (𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵))) → 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵))))) |
19 | 15, 18 | anim12d 584 |
. . . . . . . . 9
⊢
((#‘𝐴) ∈
ℕ0 → ((𝑀 ∈ ((#‘𝐴)...𝑁) ∧ 𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵)))) → (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵)))))) |
20 | 10, 19 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ Word 𝑉 → ((𝑀 ∈ ((#‘𝐴)...𝑁) ∧ 𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵)))) → (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵)))))) |
21 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ ((#‘𝐴)...𝑁) ∧ 𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵)))) → (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵)))))) |
22 | 9, 21 | syl5bi 231 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵)))))) |
23 | 22 | imp 444 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵))))) |
24 | | swrdccatfn 13333 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵))))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
25 | 23, 24 | syldan 486 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
26 | | elfz2 12204 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (𝐿...𝑁) ↔ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝐿 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁))) |
27 | | zcn 11259 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
28 | | zcn 11259 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
29 | | zcn 11259 |
. . . . . . . . . . . . 13
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℂ) |
30 | 27, 28, 29 | 3anim123i 1240 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐿 ∈
ℂ)) |
31 | 30 | 3comr 1265 |
. . . . . . . . . . 11
⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐿 ∈
ℂ)) |
32 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝐿 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁)) → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) |
33 | 26, 32 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑀 ∈ (𝐿...𝑁) → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) |
34 | 33 | adantr 480 |
. . . . . . . 8
⊢ ((𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → (𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ)) |
35 | | nnncan2 10197 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → ((𝑁 − 𝐿) − (𝑀 − 𝐿)) = (𝑁 − 𝑀)) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ ((𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝑁 − 𝐿) − (𝑀 − 𝐿)) = (𝑁 − 𝑀)) |
37 | 36 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝑁 − 𝐿) − (𝑀 − 𝐿)) = (𝑁 − 𝑀)) |
38 | 37 | oveq2d 6565 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿))) = (0..^(𝑁 − 𝑀))) |
39 | 38 | fneq2d 5896 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿))) ↔ ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀)))) |
40 | 25, 39 | mpbird 246 |
. . 3
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) |
41 | | simpr 476 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐵 ∈ Word 𝑉) |
42 | 41 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → 𝐵 ∈ Word 𝑉) |
43 | | elfzmlbm 12318 |
. . . . 5
⊢ (𝑀 ∈ (𝐿...𝑁) → (𝑀 − 𝐿) ∈ (0...(𝑁 − 𝐿))) |
44 | 43 | ad2antrl 760 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (𝑀 − 𝐿) ∈ (0...(𝑁 − 𝐿))) |
45 | | lencl 13179 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Word 𝑉 → (#‘𝐵) ∈
ℕ0) |
46 | 45 | nn0zd 11356 |
. . . . . . . . 9
⊢ (𝐵 ∈ Word 𝑉 → (#‘𝐵) ∈ ℤ) |
47 | 46 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (#‘𝐵) ∈ ℤ) |
48 | | elfzmlbp 12319 |
. . . . . . . . 9
⊢
(((#‘𝐵) ∈
ℤ ∧ 𝑁 ∈
(𝐿...(𝐿 + (#‘𝐵)))) → (𝑁 − 𝐿) ∈ (0...(#‘𝐵))) |
49 | 48 | ex 449 |
. . . . . . . 8
⊢
((#‘𝐵) ∈
ℤ → (𝑁 ∈
(𝐿...(𝐿 + (#‘𝐵))) → (𝑁 − 𝐿) ∈ (0...(#‘𝐵)))) |
50 | 47, 49 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))) → (𝑁 − 𝐿) ∈ (0...(#‘𝐵)))) |
51 | 50 | com12 32 |
. . . . . 6
⊢ (𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 − 𝐿) ∈ (0...(#‘𝐵)))) |
52 | 51 | adantl 481 |
. . . . 5
⊢ ((𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 − 𝐿) ∈ (0...(#‘𝐵)))) |
53 | 52 | impcom 445 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (𝑁 − 𝐿) ∈ (0...(#‘𝐵))) |
54 | | swrdvalfn 13278 |
. . . 4
⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ (0...(𝑁 − 𝐿)) ∧ (𝑁 − 𝐿) ∈ (0...(#‘𝐵))) → (𝐵 substr 〈(𝑀 − 𝐿), (𝑁 − 𝐿)〉) Fn (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) |
55 | 42, 44, 53, 54 | syl3anc 1318 |
. . 3
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (𝐵 substr 〈(𝑀 − 𝐿), (𝑁 − 𝐿)〉) Fn (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) |
56 | | simpl 472 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
57 | 56 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
58 | | elfzoelz 12339 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿))) → 𝑘 ∈ ℤ) |
59 | | elfzelz 12213 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (𝐿...𝑁) → 𝑀 ∈ ℤ) |
60 | | zaddcl 11294 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 + 𝑀) ∈ ℤ) |
61 | 60 | expcom 450 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → (𝑘 ∈ ℤ → (𝑘 + 𝑀) ∈ ℤ)) |
62 | 59, 61 | syl 17 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (𝐿...𝑁) → (𝑘 ∈ ℤ → (𝑘 + 𝑀) ∈ ℤ)) |
63 | 62 | ad2antrl 760 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (𝑘 ∈ ℤ → (𝑘 + 𝑀) ∈ ℤ)) |
64 | 58, 63 | syl5com 31 |
. . . . . . . 8
⊢ (𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿))) → (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (𝑘 + 𝑀) ∈ ℤ)) |
65 | 64 | impcom 445 |
. . . . . . 7
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → (𝑘 + 𝑀) ∈ ℤ) |
66 | | df-3an 1033 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ (𝑘 + 𝑀) ∈ ℤ) ↔ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑘 + 𝑀) ∈ ℤ)) |
67 | 57, 65, 66 | sylanbrc 695 |
. . . . . 6
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ (𝑘 + 𝑀) ∈ ℤ)) |
68 | | ccatsymb 13219 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ (𝑘 + 𝑀) ∈ ℤ) → ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀)) = if((𝑘 + 𝑀) < (#‘𝐴), (𝐴‘(𝑘 + 𝑀)), (𝐵‘((𝑘 + 𝑀) − (#‘𝐴))))) |
69 | 67, 68 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀)) = if((𝑘 + 𝑀) < (#‘𝐴), (𝐴‘(𝑘 + 𝑀)), (𝐵‘((𝑘 + 𝑀) − (#‘𝐴))))) |
70 | | elfzonn0 12380 |
. . . . . . . 8
⊢ (𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿))) → 𝑘 ∈ ℕ0) |
71 | | zre 11258 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℝ) |
72 | | zre 11258 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
73 | 71, 72 | anim12i 588 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐿 ∈ ℝ ∧ 𝑀 ∈
ℝ)) |
74 | | elnn0z 11267 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℤ
∧ 0 ≤ 𝑘)) |
75 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℝ) |
76 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑀 ∈ ℝ → 0 ∈
ℝ) |
77 | 76 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0
∈ ℝ ∧ 𝐿
∈ ℝ)) |
78 | 77 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (0
∈ ℝ ∧ 𝐿
∈ ℝ)) |
79 | 78 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (0
∈ ℝ ∧ 𝐿
∈ ℝ)) |
80 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ) → 𝑀 ∈
ℝ) |
81 | 80 | anim2i 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (𝑘 ∈ ℝ ∧ 𝑀 ∈
ℝ)) |
82 | | le2add 10389 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((0
∈ ℝ ∧ 𝐿
∈ ℝ) ∧ (𝑘
∈ ℝ ∧ 𝑀
∈ ℝ)) → ((0 ≤ 𝑘 ∧ 𝐿 ≤ 𝑀) → (0 + 𝐿) ≤ (𝑘 + 𝑀))) |
83 | 79, 81, 82 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → ((0
≤ 𝑘 ∧ 𝐿 ≤ 𝑀) → (0 + 𝐿) ≤ (𝑘 + 𝑀))) |
84 | | recn 9905 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐿 ∈ ℝ → 𝐿 ∈
ℂ) |
85 | 84 | addid2d 10116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐿 ∈ ℝ → (0 +
𝐿) = 𝐿) |
86 | 85 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (0 +
𝐿) = 𝐿) |
87 | 86 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → ((0 +
𝐿) ≤ (𝑘 + 𝑀) ↔ 𝐿 ≤ (𝑘 + 𝑀))) |
88 | 83, 87 | sylibd 228 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → ((0
≤ 𝑘 ∧ 𝐿 ≤ 𝑀) → 𝐿 ≤ (𝑘 + 𝑀))) |
89 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ) → 𝐿 ∈
ℝ) |
90 | 89 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → 𝐿 ∈
ℝ) |
91 | | readdcl 9898 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝑘 + 𝑀) ∈ ℝ) |
92 | 81, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (𝑘 + 𝑀) ∈ ℝ) |
93 | 90, 92 | lenltd 10062 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (𝐿 ≤ (𝑘 + 𝑀) ↔ ¬ (𝑘 + 𝑀) < 𝐿)) |
94 | 88, 93 | sylibd 228 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → ((0
≤ 𝑘 ∧ 𝐿 ≤ 𝑀) → ¬ (𝑘 + 𝑀) < 𝐿)) |
95 | 94 | expd 451 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (0 ≤
𝑘 → (𝐿 ≤ 𝑀 → ¬ (𝑘 + 𝑀) < 𝐿))) |
96 | 95 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ≤
𝑘 → ((𝑘 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ)) → (𝐿 ≤ 𝑀 → ¬ (𝑘 + 𝑀) < 𝐿))) |
97 | 96 | expd 451 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ≤
𝑘 → (𝑘 ∈ ℝ → ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝐿 ≤ 𝑀 → ¬ (𝑘 + 𝑀) < 𝐿)))) |
98 | 75, 97 | mpan9 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℤ ∧ 0 ≤
𝑘) → ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝐿 ≤ 𝑀 → ¬ (𝑘 + 𝑀) < 𝐿))) |
99 | 74, 98 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ0
→ ((𝐿 ∈ ℝ
∧ 𝑀 ∈ ℝ)
→ (𝐿 ≤ 𝑀 → ¬ (𝑘 + 𝑀) < 𝐿))) |
100 | 73, 99 | mpan9 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ ℕ0)
→ (𝐿 ≤ 𝑀 → ¬ (𝑘 + 𝑀) < 𝐿)) |
101 | 1 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . . 19
⊢
(#‘𝐴) = 𝐿 |
102 | 101 | breq2i 4591 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 + 𝑀) < (#‘𝐴) ↔ (𝑘 + 𝑀) < 𝐿) |
103 | 102 | notbii 309 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝑘 + 𝑀) < (#‘𝐴) ↔ ¬ (𝑘 + 𝑀) < 𝐿) |
104 | 100, 103 | syl6ibr 241 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ ℕ0)
→ (𝐿 ≤ 𝑀 → ¬ (𝑘 + 𝑀) < (#‘𝐴))) |
105 | 104 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 ∈ ℕ0
→ (𝐿 ≤ 𝑀 → ¬ (𝑘 + 𝑀) < (#‘𝐴)))) |
106 | 105 | com23 84 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐿 ≤ 𝑀 → (𝑘 ∈ ℕ0 → ¬
(𝑘 + 𝑀) < (#‘𝐴)))) |
107 | 106 | 3adant2 1073 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐿 ≤ 𝑀 → (𝑘 ∈ ℕ0 → ¬
(𝑘 + 𝑀) < (#‘𝐴)))) |
108 | 107 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝐿 ≤ 𝑀 → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 ∈ ℕ0 → ¬
(𝑘 + 𝑀) < (#‘𝐴)))) |
109 | 108 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐿 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁) → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 ∈ ℕ0 → ¬
(𝑘 + 𝑀) < (#‘𝐴)))) |
110 | 109 | impcom 445 |
. . . . . . . . . 10
⊢ (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝐿 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁)) → (𝑘 ∈ ℕ0 → ¬
(𝑘 + 𝑀) < (#‘𝐴))) |
111 | 26, 110 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑀 ∈ (𝐿...𝑁) → (𝑘 ∈ ℕ0 → ¬
(𝑘 + 𝑀) < (#‘𝐴))) |
112 | 111 | ad2antrl 760 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (𝑘 ∈ ℕ0 → ¬
(𝑘 + 𝑀) < (#‘𝐴))) |
113 | 70, 112 | syl5com 31 |
. . . . . . 7
⊢ (𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿))) → (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ¬ (𝑘 + 𝑀) < (#‘𝐴))) |
114 | 113 | impcom 445 |
. . . . . 6
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → ¬ (𝑘 + 𝑀) < (#‘𝐴)) |
115 | 114 | iffalsed 4047 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → if((𝑘 + 𝑀) < (#‘𝐴), (𝐴‘(𝑘 + 𝑀)), (𝐵‘((𝑘 + 𝑀) − (#‘𝐴)))) = (𝐵‘((𝑘 + 𝑀) − (#‘𝐴)))) |
116 | | zcn 11259 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℂ) |
117 | 116 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈
ℂ) |
118 | 28 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → 𝑀 ∈
ℂ) |
119 | 118 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝑀 ∈
ℂ) |
120 | 29 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → 𝐿 ∈
ℂ) |
121 | 117, 119,
120 | addsubassd 10291 |
. . . . . . . . . . . . . . 15
⊢ (((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((𝑘 + 𝑀) − 𝐿) = (𝑘 + (𝑀 − 𝐿))) |
122 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 = (#‘𝐴) → ((𝑘 + 𝑀) − 𝐿) = ((𝑘 + 𝑀) − (#‘𝐴))) |
123 | 122 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 = (#‘𝐴) → (((𝑘 + 𝑀) − 𝐿) = (𝑘 + (𝑀 − 𝐿)) ↔ ((𝑘 + 𝑀) − (#‘𝐴)) = (𝑘 + (𝑀 − 𝐿)))) |
124 | 121, 123 | syl5ib 233 |
. . . . . . . . . . . . . 14
⊢ (𝐿 = (#‘𝐴) → (((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((𝑘 + 𝑀) − (#‘𝐴)) = (𝑘 + (𝑀 − 𝐿)))) |
125 | 1, 124 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝑘 ∈ ℤ) → ((𝑘 + 𝑀) − (#‘𝐴)) = (𝑘 + (𝑀 − 𝐿))) |
126 | 125 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 ∈ ℤ → ((𝑘 + 𝑀) − (#‘𝐴)) = (𝑘 + (𝑀 − 𝐿)))) |
127 | 126 | 3adant2 1073 |
. . . . . . . . . . 11
⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑘 ∈ ℤ → ((𝑘 + 𝑀) − (#‘𝐴)) = (𝑘 + (𝑀 − 𝐿)))) |
128 | 127 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝐿 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁)) → (𝑘 ∈ ℤ → ((𝑘 + 𝑀) − (#‘𝐴)) = (𝑘 + (𝑀 − 𝐿)))) |
129 | 26, 128 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑀 ∈ (𝐿...𝑁) → (𝑘 ∈ ℤ → ((𝑘 + 𝑀) − (#‘𝐴)) = (𝑘 + (𝑀 − 𝐿)))) |
130 | 129 | ad2antrl 760 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (𝑘 ∈ ℤ → ((𝑘 + 𝑀) − (#‘𝐴)) = (𝑘 + (𝑀 − 𝐿)))) |
131 | 58, 130 | syl5com 31 |
. . . . . . 7
⊢ (𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿))) → (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝑘 + 𝑀) − (#‘𝐴)) = (𝑘 + (𝑀 − 𝐿)))) |
132 | 131 | impcom 445 |
. . . . . 6
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → ((𝑘 + 𝑀) − (#‘𝐴)) = (𝑘 + (𝑀 − 𝐿))) |
133 | 132 | fveq2d 6107 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → (𝐵‘((𝑘 + 𝑀) − (#‘𝐴))) = (𝐵‘(𝑘 + (𝑀 − 𝐿)))) |
134 | 69, 115, 133 | 3eqtrd 2648 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀)) = (𝐵‘(𝑘 + (𝑀 − 𝐿)))) |
135 | | ccatcl 13212 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
136 | 135 | ad2antrr 758 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
137 | 1, 12 | syl5eqel 2692 |
. . . . . . . . . . . 12
⊢
((#‘𝐴) ∈
ℕ0 → 𝐿 ∈
(ℤ≥‘0)) |
138 | | fzss1 12251 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈
(ℤ≥‘0) → (𝐿...𝑁) ⊆ (0...𝑁)) |
139 | 10, 137, 138 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑉 → (𝐿...𝑁) ⊆ (0...𝑁)) |
140 | 139 | sseld 3567 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → (𝑀 ∈ (𝐿...𝑁) → 𝑀 ∈ (0...𝑁))) |
141 | 140 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑀 ∈ (𝐿...𝑁) → 𝑀 ∈ (0...𝑁))) |
142 | 141 | com12 32 |
. . . . . . . 8
⊢ (𝑀 ∈ (𝐿...𝑁) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝑀 ∈ (0...𝑁))) |
143 | 142 | adantr 480 |
. . . . . . 7
⊢ ((𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝑀 ∈ (0...𝑁))) |
144 | 143 | impcom 445 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → 𝑀 ∈ (0...𝑁)) |
145 | 144 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → 𝑀 ∈ (0...𝑁)) |
146 | 1, 7 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))) ↔ 𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵)))) |
147 | 10, 12 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈
(ℤ≥‘0)) |
148 | 147 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (#‘𝐴) ∈
(ℤ≥‘0)) |
149 | 148, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((#‘𝐴)...((#‘𝐴) + (#‘𝐵))) ⊆ (0...((#‘𝐴) + (#‘𝐵)))) |
150 | 149 | sseld 3567 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵))) → 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵))))) |
151 | 150 | impcom 445 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵))) ∧ (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵)))) |
152 | | ccatlen 13213 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (#‘(𝐴 ++ 𝐵)) = ((#‘𝐴) + (#‘𝐵))) |
153 | 152 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (0...(#‘(𝐴 ++ 𝐵))) = (0...((#‘𝐴) + (#‘𝐵)))) |
154 | 153 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))) ↔ 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵))))) |
155 | 154 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵))) ∧ (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → (𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))) ↔ 𝑁 ∈ (0...((#‘𝐴) + (#‘𝐵))))) |
156 | 151, 155 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵))) ∧ (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) → 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵)))) |
157 | 156 | ex 449 |
. . . . . . . . 9
⊢ (𝑁 ∈ ((#‘𝐴)...((#‘𝐴) + (#‘𝐵))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))))) |
158 | 146, 157 | sylbi 206 |
. . . . . . . 8
⊢ (𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))))) |
159 | 158 | adantl 481 |
. . . . . . 7
⊢ ((𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))))) |
160 | 159 | impcom 445 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵)))) |
161 | 160 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵)))) |
162 | | fzmmmeqm 12245 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (𝐿...𝑁) → ((𝑁 − 𝐿) − (𝑀 − 𝐿)) = (𝑁 − 𝑀)) |
163 | 162 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑀 ∈ (𝐿...𝑁) → (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿))) = (0..^(𝑁 − 𝑀))) |
164 | 163 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑀 ∈ (𝐿...𝑁) → (𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿))) ↔ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) |
165 | 164 | biimpd 218 |
. . . . . . 7
⊢ (𝑀 ∈ (𝐿...𝑁) → (𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿))) → 𝑘 ∈ (0..^(𝑁 − 𝑀)))) |
166 | 165 | ad2antrl 760 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿))) → 𝑘 ∈ (0..^(𝑁 − 𝑀)))) |
167 | 166 | imp 444 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → 𝑘 ∈ (0..^(𝑁 − 𝑀))) |
168 | | swrdfv 13276 |
. . . . 5
⊢ ((((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀))) |
169 | 136, 145,
161, 167, 168 | syl31anc 1321 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀))) |
170 | 46, 49 | syl 17 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Word 𝑉 → (𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))) → (𝑁 − 𝐿) ∈ (0...(#‘𝐵)))) |
171 | 170 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))) → (𝑁 − 𝐿) ∈ (0...(#‘𝐵)))) |
172 | 171 | com12 32 |
. . . . . . . 8
⊢ (𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 − 𝐿) ∈ (0...(#‘𝐵)))) |
173 | 172 | adantl 481 |
. . . . . . 7
⊢ ((𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 − 𝐿) ∈ (0...(#‘𝐵)))) |
174 | 173 | impcom 445 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (𝑁 − 𝐿) ∈ (0...(#‘𝐵))) |
175 | 42, 44, 174 | 3jca 1235 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → (𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ (0...(𝑁 − 𝐿)) ∧ (𝑁 − 𝐿) ∈ (0...(#‘𝐵)))) |
176 | | swrdfv 13276 |
. . . . 5
⊢ (((𝐵 ∈ Word 𝑉 ∧ (𝑀 − 𝐿) ∈ (0...(𝑁 − 𝐿)) ∧ (𝑁 − 𝐿) ∈ (0...(#‘𝐵))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → ((𝐵 substr 〈(𝑀 − 𝐿), (𝑁 − 𝐿)〉)‘𝑘) = (𝐵‘(𝑘 + (𝑀 − 𝐿)))) |
177 | 175, 176 | sylan 487 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → ((𝐵 substr 〈(𝑀 − 𝐿), (𝑁 − 𝐿)〉)‘𝑘) = (𝐵‘(𝑘 + (𝑀 − 𝐿)))) |
178 | 134, 169,
177 | 3eqtr4d 2654 |
. . 3
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ 𝑘 ∈ (0..^((𝑁 − 𝐿) − (𝑀 − 𝐿)))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = ((𝐵 substr 〈(𝑀 − 𝐿), (𝑁 − 𝐿)〉)‘𝑘)) |
179 | 40, 55, 178 | eqfnfvd 6222 |
. 2
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐵 substr 〈(𝑀 − 𝐿), (𝑁 − 𝐿)〉)) |
180 | 179 | ex 449 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (𝐿...𝑁) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐵 substr 〈(𝑀 − 𝐿), (𝑁 − 𝐿)〉))) |