Proof of Theorem swrdccatin12lem3
Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
2 | | elfzo0 12376 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0..^(𝐿 − 𝑀)) ↔ (𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀))) |
3 | | swrdccatin12.l |
. . . . . . . . . . . . 13
⊢ 𝐿 = (#‘𝐴) |
4 | | lencl 13179 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈
ℕ0) |
5 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ (0...𝐿) ↔ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿)) |
6 | | nn0addcl 11205 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 + 𝑀) ∈
ℕ0) |
7 | 6 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐾 ∈ ℕ0
→ (𝑀 ∈
ℕ0 → (𝐾 + 𝑀) ∈
ℕ0)) |
8 | 7 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → (𝑀 ∈ ℕ0 → (𝐾 + 𝑀) ∈
ℕ0)) |
9 | 8 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℕ0
→ ((𝐾 ∈
ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → (𝐾 + 𝑀) ∈
ℕ0)) |
10 | 9 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → (𝐾 + 𝑀) ∈
ℕ0)) |
11 | 10 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) ∧ (𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀))) → (𝐾 + 𝑀) ∈
ℕ0) |
12 | | elnnz 11264 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐿 − 𝑀) ∈ ℕ ↔ ((𝐿 − 𝑀) ∈ ℤ ∧ 0 < (𝐿 − 𝑀))) |
13 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
14 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) |
15 | | posdif 10400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑀 < 𝐿 ↔ 0 < (𝐿 − 𝑀))) |
16 | 13, 14, 15 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑀 < 𝐿 ↔ 0 < (𝐿 − 𝑀))) |
17 | | elnn0z 11267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℤ
∧ 0 ≤ 𝑀)) |
18 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0)
→ 0 ∈ ℝ) |
19 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0)
→ 𝑀 ∈
ℝ) |
21 | 14 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0)
→ 𝐿 ∈
ℝ) |
22 | | lelttr 10007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((0
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 𝐿
∈ ℝ) → ((0 ≤ 𝑀 ∧ 𝑀 < 𝐿) → 0 < 𝐿)) |
23 | 18, 20, 21, 22 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0)
→ ((0 ≤ 𝑀 ∧
𝑀 < 𝐿) → 0 < 𝐿)) |
24 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℤ) |
25 | 24 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐿 ∈ ℕ0
∧ 0 < 𝐿) →
(𝐿 ∈ ℤ ∧ 0
< 𝐿)) |
26 | | elnnz 11264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 0 <
𝐿)) |
27 | 25, 26 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐿 ∈ ℕ0
∧ 0 < 𝐿) →
𝐿 ∈
ℕ) |
28 | 27 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝐿 ∈ ℕ0
→ (0 < 𝐿 →
𝐿 ∈
ℕ)) |
29 | 28 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0)
→ (0 < 𝐿 →
𝐿 ∈
ℕ)) |
30 | 23, 29 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0)
→ ((0 ≤ 𝑀 ∧
𝑀 < 𝐿) → 𝐿 ∈ ℕ)) |
31 | 30 | expd 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0)
→ (0 ≤ 𝑀 →
(𝑀 < 𝐿 → 𝐿 ∈ ℕ))) |
32 | 31 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑀 ∈ ℤ ∧ 0 ≤
𝑀) → (𝐿 ∈ ℕ0
→ (𝑀 < 𝐿 → 𝐿 ∈ ℕ))) |
33 | 17, 32 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑀 ∈ ℕ0
→ (𝐿 ∈
ℕ0 → (𝑀 < 𝐿 → 𝐿 ∈ ℕ))) |
34 | 33 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑀 < 𝐿 → 𝐿 ∈ ℕ)) |
35 | 16, 34 | sylbird 249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (0 < (𝐿 − 𝑀) → 𝐿 ∈ ℕ)) |
36 | 35 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (0 <
(𝐿 − 𝑀) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ 𝐿 ∈
ℕ)) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐿 − 𝑀) ∈ ℤ ∧ 0 < (𝐿 − 𝑀)) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ 𝐿 ∈
ℕ)) |
38 | 12, 37 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐿 − 𝑀) ∈ ℕ → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ 𝐿 ∈
ℕ)) |
39 | 38 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ 𝐿 ∈
ℕ)) |
40 | 39 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → 𝐿 ∈ ℕ)) |
41 | 40 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → 𝐿 ∈ ℕ)) |
42 | 41 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) ∧ (𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀))) → 𝐿 ∈ ℕ) |
43 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐾 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝐿
∈ ℕ0 ∧ 𝑀 ≤ 𝐿)) → 𝐾 ∈ ℝ) |
45 | 13 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → 𝑀 ∈
ℝ) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐾 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝐿
∈ ℕ0 ∧ 𝑀 ≤ 𝐿)) → 𝑀 ∈ ℝ) |
47 | 14 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → 𝐿 ∈
ℝ) |
48 | 47 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐾 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝐿
∈ ℕ0 ∧ 𝑀 ≤ 𝐿)) → 𝐿 ∈ ℝ) |
49 | 44, 46, 48 | ltaddsubd 10506 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐾 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝐿
∈ ℕ0 ∧ 𝑀 ≤ 𝐿)) → ((𝐾 + 𝑀) < 𝐿 ↔ 𝐾 < (𝐿 − 𝑀))) |
50 | 49 | exbiri 650 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐾 ∈ ℕ0
→ ((𝑀 ∈
ℕ0 ∧ 𝐿
∈ ℕ0 ∧ 𝑀 ≤ 𝐿) → (𝐾 < (𝐿 − 𝑀) → (𝐾 + 𝑀) < 𝐿))) |
51 | 50 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐾 ∈ ℕ0
→ (𝐾 < (𝐿 − 𝑀) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿) → (𝐾 + 𝑀) < 𝐿))) |
52 | 51 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐾 ∈ ℕ0
∧ 𝐾 < (𝐿 − 𝑀)) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿) → (𝐾 + 𝑀) < 𝐿)) |
53 | 52 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿) → (𝐾 + 𝑀) < 𝐿)) |
54 | 53 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) ∧ (𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀))) → (𝐾 + 𝑀) < 𝐿) |
55 | 11, 42, 54 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) ∧ (𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)) |
56 | 55 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))) |
57 | 56 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → (𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)))) |
58 | 5, 57 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ (0...𝐿) → (𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)))) |
59 | 58 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))) |
60 | 59 | 2a1i 12 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐴) = 𝐿 → (𝐿 ∈ ℕ0 → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))))) |
61 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐴) = 𝐿 → ((#‘𝐴) ∈ ℕ0
↔ 𝐿 ∈
ℕ0)) |
62 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐴) = 𝐿 → ((#‘𝐴) ∈ ℕ ↔ 𝐿 ∈
ℕ)) |
63 | | breq2 4587 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐴) = 𝐿 → ((𝐾 + 𝑀) < (#‘𝐴) ↔ (𝐾 + 𝑀) < 𝐿)) |
64 | 62, 63 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐴) = 𝐿 → (((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴)) ↔ ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))) |
65 | 64 | imbi2d 329 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐴) = 𝐿 → (((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴))) ↔ ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)))) |
66 | 65 | imbi2d 329 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐴) = 𝐿 → (((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴)))) ↔ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))))) |
67 | 60, 61, 66 | 3imtr4d 282 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐴) = 𝐿 → ((#‘𝐴) ∈ ℕ0
→ ((𝑀 ∈
(0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴)))))) |
68 | 67 | eqcoms 2618 |
. . . . . . . . . . . . 13
⊢ (𝐿 = (#‘𝐴) → ((#‘𝐴) ∈ ℕ0 → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴)))))) |
69 | 3, 4, 68 | mpsyl 66 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Word 𝑉 → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴))))) |
70 | 69 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴))))) |
71 | 70 | imp 444 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴)))) |
72 | 71 | com12 32 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴)))) |
73 | 2, 72 | sylbi 206 |
. . . . . . . 8
⊢ (𝐾 ∈ (0..^(𝐿 − 𝑀)) → (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴)))) |
74 | 73 | adantl 481 |
. . . . . . 7
⊢ ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴)))) |
75 | 74 | impcom 445 |
. . . . . 6
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴))) |
76 | | elfzo0 12376 |
. . . . . 6
⊢ ((𝐾 + 𝑀) ∈ (0..^(#‘𝐴)) ↔ ((𝐾 + 𝑀) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝐾 + 𝑀) < (#‘𝐴))) |
77 | 75, 76 | sylibr 223 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → (𝐾 + 𝑀) ∈ (0..^(#‘𝐴))) |
78 | | df-3an 1033 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ (0..^(#‘𝐴))) ↔ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝐾 + 𝑀) ∈ (0..^(#‘𝐴)))) |
79 | 1, 77, 78 | sylanbrc 695 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ (0..^(#‘𝐴)))) |
80 | | ccatval1 13214 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ (0..^(#‘𝐴))) → ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)) = (𝐴‘(𝐾 + 𝑀))) |
81 | 79, 80 | syl 17 |
. . 3
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)) = (𝐴‘(𝐾 + 𝑀))) |
82 | 3 | swrdccatin12lem2c 13339 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))))) |
83 | 82 | adantr 480 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵))))) |
84 | | simprl 790 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → 𝐾 ∈ (0..^(𝑁 − 𝑀))) |
85 | | swrdfv 13276 |
. . . 4
⊢ ((((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘(𝐴 ++ 𝐵)))) ∧ 𝐾 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀))) |
86 | 83, 84, 85 | syl2anc 691 |
. . 3
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀))) |
87 | | simpll 786 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → 𝐴 ∈ Word 𝑉) |
88 | 87 | adantr 480 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → 𝐴 ∈ Word 𝑉) |
89 | | simprl 790 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → 𝑀 ∈ (0...𝐿)) |
90 | 89 | adantr 480 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → 𝑀 ∈ (0...𝐿)) |
91 | 3 | eleq1i 2679 |
. . . . . . 7
⊢ (𝐿 ∈ ℕ0
↔ (#‘𝐴) ∈
ℕ0) |
92 | | elnn0uz 11601 |
. . . . . . . . 9
⊢ (𝐿 ∈ ℕ0
↔ 𝐿 ∈
(ℤ≥‘0)) |
93 | | eluzfz2 12220 |
. . . . . . . . 9
⊢ (𝐿 ∈
(ℤ≥‘0) → 𝐿 ∈ (0...𝐿)) |
94 | 92, 93 | sylbi 206 |
. . . . . . . 8
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈ (0...𝐿)) |
95 | 3 | eqcomi 2619 |
. . . . . . . . 9
⊢
(#‘𝐴) = 𝐿 |
96 | 95 | oveq2i 6560 |
. . . . . . . 8
⊢
(0...(#‘𝐴)) =
(0...𝐿) |
97 | 94, 96 | syl6eleqr 2699 |
. . . . . . 7
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
(0...(#‘𝐴))) |
98 | 91, 97 | sylbir 224 |
. . . . . 6
⊢
((#‘𝐴) ∈
ℕ0 → 𝐿 ∈ (0...(#‘𝐴))) |
99 | 4, 98 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ (0...(#‘𝐴))) |
100 | 99 | ad3antrrr 762 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → 𝐿 ∈ (0...(#‘𝐴))) |
101 | | simprr 792 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → 𝐾 ∈ (0..^(𝐿 − 𝑀))) |
102 | | swrdfv 13276 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(#‘𝐴))) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → ((𝐴 substr 〈𝑀, 𝐿〉)‘𝐾) = (𝐴‘(𝐾 + 𝑀))) |
103 | 88, 90, 100, 101, 102 | syl31anc 1321 |
. . 3
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → ((𝐴 substr 〈𝑀, 𝐿〉)‘𝐾) = (𝐴‘(𝐾 + 𝑀))) |
104 | 81, 86, 103 | 3eqtr4d 2654 |
. 2
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐴 substr 〈𝑀, 𝐿〉)‘𝐾)) |
105 | 104 | ex 449 |
1
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐴 substr 〈𝑀, 𝐿〉)‘𝐾))) |