Proof of Theorem pfxccatin12lem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpll 767 | . . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) | 
| 2 |  | elfzo0 13740 | . . . . . . . . 9
⊢ (𝐾 ∈ (0..^(𝐿 − 𝑀)) ↔ (𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀))) | 
| 3 |  | swrdccatin2.l | . . . . . . . . . . . . 13
⊢ 𝐿 = (♯‘𝐴) | 
| 4 |  | lencl 14571 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈
ℕ0) | 
| 5 |  | elfz2nn0 13658 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ (0...𝐿) ↔ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿)) | 
| 6 |  | nn0addcl 12561 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 + 𝑀) ∈
ℕ0) | 
| 7 | 6 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐾 ∈ ℕ0
→ (𝑀 ∈
ℕ0 → (𝐾 + 𝑀) ∈
ℕ0)) | 
| 8 | 7 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → (𝑀 ∈ ℕ0 → (𝐾 + 𝑀) ∈
ℕ0)) | 
| 9 | 8 | com12 32 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℕ0
→ ((𝐾 ∈
ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → (𝐾 + 𝑀) ∈
ℕ0)) | 
| 10 | 9 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → (𝐾 + 𝑀) ∈
ℕ0)) | 
| 11 | 10 | imp 406 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) ∧ (𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀))) → (𝐾 + 𝑀) ∈
ℕ0) | 
| 12 |  | elnnz 12623 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐿 − 𝑀) ∈ ℕ ↔ ((𝐿 − 𝑀) ∈ ℤ ∧ 0 < (𝐿 − 𝑀))) | 
| 13 |  | nn0re 12535 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) | 
| 14 |  | nn0re 12535 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) | 
| 15 |  | posdif 11756 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑀 < 𝐿 ↔ 0 < (𝐿 − 𝑀))) | 
| 16 | 13, 14, 15 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑀 < 𝐿 ↔ 0 < (𝐿 − 𝑀))) | 
| 17 |  | elnn0z 12626 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℤ
∧ 0 ≤ 𝑀)) | 
| 18 |  | 0re 11263 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 0 ∈
ℝ | 
| 19 |  | zre 12617 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) | 
| 20 |  | lelttr 11351 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((0
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 𝐿
∈ ℝ) → ((0 ≤ 𝑀 ∧ 𝑀 < 𝐿) → 0 < 𝐿)) | 
| 21 | 18, 19, 14, 20 | mp3an3an 1469 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0)
→ ((0 ≤ 𝑀 ∧
𝑀 < 𝐿) → 0 < 𝐿)) | 
| 22 |  | nn0z 12638 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℤ) | 
| 23 | 22 | anim1i 615 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐿 ∈ ℕ0
∧ 0 < 𝐿) →
(𝐿 ∈ ℤ ∧ 0
< 𝐿)) | 
| 24 |  | elnnz 12623 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 0 <
𝐿)) | 
| 25 | 23, 24 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐿 ∈ ℕ0
∧ 0 < 𝐿) →
𝐿 ∈
ℕ) | 
| 26 | 25 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝐿 ∈ ℕ0
→ (0 < 𝐿 →
𝐿 ∈
ℕ)) | 
| 27 | 26 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0)
→ (0 < 𝐿 →
𝐿 ∈
ℕ)) | 
| 28 | 21, 27 | syld 47 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0)
→ ((0 ≤ 𝑀 ∧
𝑀 < 𝐿) → 𝐿 ∈ ℕ)) | 
| 29 | 28 | expd 415 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0)
→ (0 ≤ 𝑀 →
(𝑀 < 𝐿 → 𝐿 ∈ ℕ))) | 
| 30 | 29 | impancom 451 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑀 ∈ ℤ ∧ 0 ≤
𝑀) → (𝐿 ∈ ℕ0
→ (𝑀 < 𝐿 → 𝐿 ∈ ℕ))) | 
| 31 | 17, 30 | sylbi 217 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑀 ∈ ℕ0
→ (𝐿 ∈
ℕ0 → (𝑀 < 𝐿 → 𝐿 ∈ ℕ))) | 
| 32 | 31 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑀 < 𝐿 → 𝐿 ∈ ℕ)) | 
| 33 | 16, 32 | sylbird 260 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (0 < (𝐿 − 𝑀) → 𝐿 ∈ ℕ)) | 
| 34 | 33 | com12 32 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 <
(𝐿 − 𝑀) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ 𝐿 ∈
ℕ)) | 
| 35 | 12, 34 | simplbiim 504 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐿 − 𝑀) ∈ ℕ → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ 𝐿 ∈
ℕ)) | 
| 36 | 35 | 3ad2ant2 1135 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)
→ 𝐿 ∈
ℕ)) | 
| 37 | 36 | com12 32 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → 𝐿 ∈ ℕ)) | 
| 38 | 37 | 3adant3 1133 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → 𝐿 ∈ ℕ)) | 
| 39 | 38 | imp 406 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) ∧ (𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀))) → 𝐿 ∈ ℕ) | 
| 40 |  | nn0re 12535 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) | 
| 41 | 40 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐾 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝐿
∈ ℕ0 ∧ 𝑀 ≤ 𝐿)) → 𝐾 ∈ ℝ) | 
| 42 | 13 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → 𝑀 ∈
ℝ) | 
| 43 | 42 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐾 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝐿
∈ ℕ0 ∧ 𝑀 ≤ 𝐿)) → 𝑀 ∈ ℝ) | 
| 44 | 14 | 3ad2ant2 1135 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → 𝐿 ∈
ℝ) | 
| 45 | 44 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐾 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝐿
∈ ℕ0 ∧ 𝑀 ≤ 𝐿)) → 𝐿 ∈ ℝ) | 
| 46 | 41, 43, 45 | ltaddsubd 11863 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐾 ∈ ℕ0
∧ (𝑀 ∈
ℕ0 ∧ 𝐿
∈ ℕ0 ∧ 𝑀 ≤ 𝐿)) → ((𝐾 + 𝑀) < 𝐿 ↔ 𝐾 < (𝐿 − 𝑀))) | 
| 47 | 46 | exbiri 811 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐾 ∈ ℕ0
→ ((𝑀 ∈
ℕ0 ∧ 𝐿
∈ ℕ0 ∧ 𝑀 ≤ 𝐿) → (𝐾 < (𝐿 − 𝑀) → (𝐾 + 𝑀) < 𝐿))) | 
| 48 | 47 | com23 86 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐾 ∈ ℕ0
→ (𝐾 < (𝐿 − 𝑀) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿) → (𝐾 + 𝑀) < 𝐿))) | 
| 49 | 48 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐾 ∈ ℕ0
∧ 𝐾 < (𝐿 − 𝑀)) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿) → (𝐾 + 𝑀) < 𝐿)) | 
| 50 | 49 | 3adant2 1132 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿) → (𝐾 + 𝑀) < 𝐿)) | 
| 51 | 50 | impcom 407 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) ∧ (𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀))) → (𝐾 + 𝑀) < 𝐿) | 
| 52 | 11, 39, 51 | 3jca 1129 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) ∧ (𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)) | 
| 53 | 52 | ex 412 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))) | 
| 54 | 53 | a1d 25 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)))) | 
| 55 | 5, 54 | sylbi 217 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ (0...𝐿) → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)))) | 
| 56 | 55 | imp 406 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))) | 
| 57 | 56 | 2a1i 12 | . . . . . . . . . . . . . . 15
⊢
((♯‘𝐴) =
𝐿 → (𝐿 ∈ ℕ0 → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))))) | 
| 58 |  | eleq1 2829 | . . . . . . . . . . . . . . 15
⊢
((♯‘𝐴) =
𝐿 →
((♯‘𝐴) ∈
ℕ0 ↔ 𝐿 ∈
ℕ0)) | 
| 59 |  | eleq1 2829 | . . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝐴) =
𝐿 →
((♯‘𝐴) ∈
ℕ ↔ 𝐿 ∈
ℕ)) | 
| 60 |  | breq2 5147 | . . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝐴) =
𝐿 → ((𝐾 + 𝑀) < (♯‘𝐴) ↔ (𝐾 + 𝑀) < 𝐿)) | 
| 61 | 59, 60 | 3anbi23d 1441 | . . . . . . . . . . . . . . . . 17
⊢
((♯‘𝐴) =
𝐿 → (((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)) ↔ ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))) | 
| 62 | 61 | imbi2d 340 | . . . . . . . . . . . . . . . 16
⊢
((♯‘𝐴) =
𝐿 → (((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴))) ↔ ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)))) | 
| 63 | 62 | imbi2d 340 | . . . . . . . . . . . . . . 15
⊢
((♯‘𝐴) =
𝐿 → (((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)))) ↔ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))))) | 
| 64 | 57, 58, 63 | 3imtr4d 294 | . . . . . . . . . . . . . 14
⊢
((♯‘𝐴) =
𝐿 →
((♯‘𝐴) ∈
ℕ0 → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)))))) | 
| 65 | 64 | eqcoms 2745 | . . . . . . . . . . . . 13
⊢ (𝐿 = (♯‘𝐴) → ((♯‘𝐴) ∈ ℕ0
→ ((𝑀 ∈
(0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)))))) | 
| 66 | 3, 4, 65 | mpsyl 68 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ Word 𝑉 → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴))))) | 
| 67 | 66 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴))))) | 
| 68 | 67 | imp 406 | . . . . . . . . . 10
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ ℕ0 ∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)))) | 
| 69 | 68 | com12 32 | . . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ (𝐿 − 𝑀) ∈ ℕ ∧ 𝐾 < (𝐿 − 𝑀)) → (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)))) | 
| 70 | 2, 69 | sylbi 217 | . . . . . . . 8
⊢ (𝐾 ∈ (0..^(𝐿 − 𝑀)) → (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)))) | 
| 71 | 70 | adantl 481 | . . . . . . 7
⊢ ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)))) | 
| 72 | 71 | impcom 407 | . . . . . 6
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴))) | 
| 73 |  | elfzo0 13740 | . . . . . 6
⊢ ((𝐾 + 𝑀) ∈ (0..^(♯‘𝐴)) ↔ ((𝐾 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴))) | 
| 74 | 72, 73 | sylibr 234 | . . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → (𝐾 + 𝑀) ∈ (0..^(♯‘𝐴))) | 
| 75 |  | df-3an 1089 | . . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ (0..^(♯‘𝐴))) ↔ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝐾 + 𝑀) ∈ (0..^(♯‘𝐴)))) | 
| 76 | 1, 74, 75 | sylanbrc 583 | . . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ (0..^(♯‘𝐴)))) | 
| 77 |  | ccatval1 14615 | . . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)) = (𝐴‘(𝐾 + 𝑀))) | 
| 78 | 76, 77 | syl 17 | . . 3
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)) = (𝐴‘(𝐾 + 𝑀))) | 
| 79 | 3 | pfxccatin12lem2c 14768 | . . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵))))) | 
| 80 |  | simpl 482 | . . . 4
⊢ ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → 𝐾 ∈ (0..^(𝑁 − 𝑀))) | 
| 81 |  | swrdfv 14686 | . . . 4
⊢ ((((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) ∧ 𝐾 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀))) | 
| 82 | 79, 80, 81 | syl2an 596 | . . 3
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀))) | 
| 83 |  | simplll 775 | . . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → 𝐴 ∈ Word 𝑉) | 
| 84 |  | simplrl 777 | . . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → 𝑀 ∈ (0...𝐿)) | 
| 85 | 3 | eleq1i 2832 | . . . . . . 7
⊢ (𝐿 ∈ ℕ0
↔ (♯‘𝐴)
∈ ℕ0) | 
| 86 |  | elnn0uz 12923 | . . . . . . . . 9
⊢ (𝐿 ∈ ℕ0
↔ 𝐿 ∈
(ℤ≥‘0)) | 
| 87 |  | eluzfz2 13572 | . . . . . . . . 9
⊢ (𝐿 ∈
(ℤ≥‘0) → 𝐿 ∈ (0...𝐿)) | 
| 88 | 86, 87 | sylbi 217 | . . . . . . . 8
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈ (0...𝐿)) | 
| 89 | 3 | oveq2i 7442 | . . . . . . . 8
⊢
(0...𝐿) =
(0...(♯‘𝐴)) | 
| 90 | 88, 89 | eleqtrdi 2851 | . . . . . . 7
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
(0...(♯‘𝐴))) | 
| 91 | 85, 90 | sylbir 235 | . . . . . 6
⊢
((♯‘𝐴)
∈ ℕ0 → 𝐿 ∈ (0...(♯‘𝐴))) | 
| 92 | 4, 91 | syl 17 | . . . . 5
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ (0...(♯‘𝐴))) | 
| 93 | 92 | ad3antrrr 730 | . . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → 𝐿 ∈ (0...(♯‘𝐴))) | 
| 94 |  | simprr 773 | . . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → 𝐾 ∈ (0..^(𝐿 − 𝑀))) | 
| 95 |  | swrdfv 14686 | . . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐴))) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → ((𝐴 substr 〈𝑀, 𝐿〉)‘𝐾) = (𝐴‘(𝐾 + 𝑀))) | 
| 96 | 83, 84, 93, 94, 95 | syl31anc 1375 | . . 3
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → ((𝐴 substr 〈𝑀, 𝐿〉)‘𝐾) = (𝐴‘(𝐾 + 𝑀))) | 
| 97 | 78, 82, 96 | 3eqtr4d 2787 | . 2
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀)))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐴 substr 〈𝑀, 𝐿〉)‘𝐾)) | 
| 98 | 97 | ex 412 | 1
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝐾 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝐾) = ((𝐴 substr 〈𝑀, 𝐿〉)‘𝐾))) |