Proof of Theorem pfxccat3a
Step | Hyp | Ref
| Expression |
1 | | simprl 790 |
. . . . . 6
⊢ ((𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
2 | | elfznn0 12302 |
. . . . . . . . 9
⊢ (𝑁 ∈ (0...(𝐿 + 𝑀)) → 𝑁 ∈
ℕ0) |
3 | 2 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀))) → 𝑁 ∈
ℕ0) |
4 | 3 | adantl 481 |
. . . . . . 7
⊢ ((𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → 𝑁 ∈
ℕ0) |
5 | | pfxccatin12.l |
. . . . . . . . . . 11
⊢ 𝐿 = (#‘𝐴) |
6 | | lencl 13179 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈
ℕ0) |
7 | 5, 6 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈
ℕ0) |
8 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐿 ∈
ℕ0) |
9 | 8 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀))) → 𝐿 ∈
ℕ0) |
10 | 9 | adantl 481 |
. . . . . . 7
⊢ ((𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → 𝐿 ∈
ℕ0) |
11 | | simpl 472 |
. . . . . . 7
⊢ ((𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → 𝑁 ≤ 𝐿) |
12 | | elfz2nn0 12300 |
. . . . . . 7
⊢ (𝑁 ∈ (0...𝐿) ↔ (𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑁 ≤ 𝐿)) |
13 | 4, 10, 11, 12 | syl3anbrc 1239 |
. . . . . 6
⊢ ((𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → 𝑁 ∈ (0...𝐿)) |
14 | | df-3an 1033 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...𝐿)) ↔ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...𝐿))) |
15 | 1, 13, 14 | sylanbrc 695 |
. . . . 5
⊢ ((𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...𝐿))) |
16 | 5 | pfxccatpfx1 40290 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...𝐿)) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 prefix 𝑁)) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ ((𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 prefix 𝑁)) |
18 | | iftrue 4042 |
. . . . 5
⊢ (𝑁 ≤ 𝐿 → if(𝑁 ≤ 𝐿, (𝐴 prefix 𝑁), (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) = (𝐴 prefix 𝑁)) |
19 | 18 | adantr 480 |
. . . 4
⊢ ((𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → if(𝑁 ≤ 𝐿, (𝐴 prefix 𝑁), (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) = (𝐴 prefix 𝑁)) |
20 | 17, 19 | eqtr4d 2647 |
. . 3
⊢ ((𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → ((𝐴 ++ 𝐵) prefix 𝑁) = if(𝑁 ≤ 𝐿, (𝐴 prefix 𝑁), (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿))))) |
21 | | simprl 790 |
. . . . . 6
⊢ ((¬
𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
22 | | elfz2nn0 12300 |
. . . . . . . . 9
⊢ (𝑁 ∈ (0...(𝐿 + 𝑀)) ↔ (𝑁 ∈ ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) |
23 | 5 | eleq1i 2679 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ ℕ0
↔ (#‘𝐴) ∈
ℕ0) |
24 | | nn0ltp1le 11312 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐿 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐿 < 𝑁 ↔ (𝐿 + 1) ≤ 𝑁)) |
25 | | nn0re 11178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) |
26 | | nn0re 11178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
27 | | ltnle 9996 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿)) |
28 | 25, 26, 27 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐿 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿)) |
29 | 24, 28 | bitr3d 269 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝐿 + 1) ≤ 𝑁 ↔ ¬ 𝑁 ≤ 𝐿)) |
30 | 29 | 3ad2antr1 1219 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) → ((𝐿 + 1) ≤ 𝑁 ↔ ¬ 𝑁 ≤ 𝐿)) |
31 | | simpr3 1062 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) → 𝑁 ≤ (𝐿 + 𝑀)) |
32 | 31 | anim1i 590 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) ∧ (𝐿 + 1) ≤ 𝑁) → (𝑁 ≤ (𝐿 + 𝑀) ∧ (𝐿 + 1) ≤ 𝑁)) |
33 | 32 | ancomd 466 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) ∧ (𝐿 + 1) ≤ 𝑁) → ((𝐿 + 1) ≤ 𝑁 ∧ 𝑁 ≤ (𝐿 + 𝑀))) |
34 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
35 | 34 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ0
∧ (𝐿 + 𝑀) ∈ ℕ0
∧ 𝑁 ≤ (𝐿 + 𝑀)) → 𝑁 ∈ ℤ) |
36 | 35 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) → 𝑁 ∈ ℤ) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) ∧ (𝐿 + 1) ≤ 𝑁) → 𝑁 ∈ ℤ) |
38 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 ∈ ℕ0
→ (𝐿 + 1) ∈
ℕ0) |
39 | 38 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 ∈ ℕ0
→ (𝐿 + 1) ∈
ℤ) |
40 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) → (𝐿 + 1) ∈ ℤ) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) ∧ (𝐿 + 1) ≤ 𝑁) → (𝐿 + 1) ∈ ℤ) |
42 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 + 𝑀) ∈ ℕ0 → (𝐿 + 𝑀) ∈ ℤ) |
43 | 42 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ0
∧ (𝐿 + 𝑀) ∈ ℕ0
∧ 𝑁 ≤ (𝐿 + 𝑀)) → (𝐿 + 𝑀) ∈ ℤ) |
44 | 43 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) → (𝐿 + 𝑀) ∈ ℤ) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) ∧ (𝐿 + 1) ≤ 𝑁) → (𝐿 + 𝑀) ∈ ℤ) |
46 | | elfz 12203 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ (𝐿 + 1) ∈ ℤ ∧
(𝐿 + 𝑀) ∈ ℤ) → (𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)) ↔ ((𝐿 + 1) ≤ 𝑁 ∧ 𝑁 ≤ (𝐿 + 𝑀)))) |
47 | 37, 41, 45, 46 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) ∧ (𝐿 + 1) ≤ 𝑁) → (𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)) ↔ ((𝐿 + 1) ≤ 𝑁 ∧ 𝑁 ≤ (𝐿 + 𝑀)))) |
48 | 33, 47 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ (((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) ∧ (𝐿 + 1) ≤ 𝑁) → 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) |
49 | 48 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) → ((𝐿 + 1) ≤ 𝑁 → 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)))) |
50 | 30, 49 | sylbird 249 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀))) → (¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)))) |
51 | 50 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ ℕ0
→ ((𝑁 ∈
ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀)) → (¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))))) |
52 | 23, 51 | sylbir 224 |
. . . . . . . . . . 11
⊢
((#‘𝐴) ∈
ℕ0 → ((𝑁 ∈ ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀)) → (¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))))) |
53 | 6, 52 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → ((𝑁 ∈ ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀)) → (¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))))) |
54 | 53 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑁 ∈ ℕ0 ∧ (𝐿 + 𝑀) ∈ ℕ0 ∧ 𝑁 ≤ (𝐿 + 𝑀)) → (¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))))) |
55 | 22, 54 | syl5bi 231 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(𝐿 + 𝑀)) → (¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))))) |
56 | 55 | imp 444 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀))) → (¬ 𝑁 ≤ 𝐿 → 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)))) |
57 | 56 | impcom 445 |
. . . . . 6
⊢ ((¬
𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) |
58 | | df-3an 1033 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) ↔ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)))) |
59 | 21, 57, 58 | sylanbrc 695 |
. . . . 5
⊢ ((¬
𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)))) |
60 | | pfxccatpfx2.m |
. . . . . 6
⊢ 𝑀 = (#‘𝐵) |
61 | 5, 60 | pfxccatpfx2 40291 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |
62 | 59, 61 | syl 17 |
. . . 4
⊢ ((¬
𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |
63 | | iffalse 4045 |
. . . . 5
⊢ (¬
𝑁 ≤ 𝐿 → if(𝑁 ≤ 𝐿, (𝐴 prefix 𝑁), (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |
64 | 63 | adantr 480 |
. . . 4
⊢ ((¬
𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → if(𝑁 ≤ 𝐿, (𝐴 prefix 𝑁), (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |
65 | 62, 64 | eqtr4d 2647 |
. . 3
⊢ ((¬
𝑁 ≤ 𝐿 ∧ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀)))) → ((𝐴 ++ 𝐵) prefix 𝑁) = if(𝑁 ≤ 𝐿, (𝐴 prefix 𝑁), (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿))))) |
66 | 20, 65 | pm2.61ian 827 |
. 2
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = if(𝑁 ≤ 𝐿, (𝐴 prefix 𝑁), (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿))))) |
67 | 66 | ex 449 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(𝐿 + 𝑀)) → ((𝐴 ++ 𝐵) prefix 𝑁) = if(𝑁 ≤ 𝐿, (𝐴 prefix 𝑁), (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))))) |