Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
β’ ((π β Word π β§ 2 β€ π) β π β Word π) |
2 | | simpr 486 |
. . . . . 6
β’ ((π β Word π β§ 2 β€ π) β 2 β€ π) |
3 | | pfxlsw2ccat.n |
. . . . . 6
β’ π = (β―βπ) |
4 | 2, 3 | breqtrdi 5150 |
. . . . 5
β’ ((π β Word π β§ 2 β€ π) β 2 β€ (β―βπ)) |
5 | | wrdlenge2n0 14449 |
. . . . 5
β’ ((π β Word π β§ 2 β€ (β―βπ)) β π β β
) |
6 | 1, 4, 5 | syl2anc 585 |
. . . 4
β’ ((π β Word π β§ 2 β€ π) β π β β
) |
7 | | pfxlswccat 14610 |
. . . 4
β’ ((π β Word π β§ π β β
) β ((π prefix ((β―βπ) β 1)) ++
β¨β(lastSβπ)ββ©) = π) |
8 | 1, 6, 7 | syl2anc 585 |
. . 3
β’ ((π β Word π β§ 2 β€ π) β ((π prefix ((β―βπ) β 1)) ++
β¨β(lastSβπ)ββ©) = π) |
9 | | lsw 14461 |
. . . . . . 7
β’ (π β Word π β (lastSβπ) = (πβ((β―βπ) β 1))) |
10 | 3 | oveq1i 7371 |
. . . . . . . 8
β’ (π β 1) =
((β―βπ) β
1) |
11 | 10 | fveq2i 6849 |
. . . . . . 7
β’ (πβ(π β 1)) = (πβ((β―βπ) β 1)) |
12 | 9, 11 | eqtr4di 2791 |
. . . . . 6
β’ (π β Word π β (lastSβπ) = (πβ(π β 1))) |
13 | 1, 12 | syl 17 |
. . . . 5
β’ ((π β Word π β§ 2 β€ π) β (lastSβπ) = (πβ(π β 1))) |
14 | 13 | s1eqd 14498 |
. . . 4
β’ ((π β Word π β§ 2 β€ π) β β¨β(lastSβπ)ββ© =
β¨β(πβ(π β 1))ββ©) |
15 | 14 | oveq2d 7377 |
. . 3
β’ ((π β Word π β§ 2 β€ π) β ((π prefix ((β―βπ) β 1)) ++
β¨β(lastSβπ)ββ©) = ((π prefix ((β―βπ) β 1)) ++ β¨β(πβ(π β 1))ββ©)) |
16 | 8, 15 | eqtr3d 2775 |
. 2
β’ ((π β Word π β§ 2 β€ π) β π = ((π prefix ((β―βπ) β 1)) ++ β¨β(πβ(π β 1))ββ©)) |
17 | | pfxcl 14574 |
. . . . . 6
β’ (π β Word π β (π prefix ((β―βπ) β 1)) β Word π) |
18 | 1, 17 | syl 17 |
. . . . 5
β’ ((π β Word π β§ 2 β€ π) β (π prefix ((β―βπ) β 1)) β Word π) |
19 | | lencl 14430 |
. . . . . . . . . 10
β’ (π β Word π β (β―βπ) β
β0) |
20 | 1, 19 | syl 17 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ π) β (β―βπ) β
β0) |
21 | 3, 20 | eqeltrid 2838 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ π) β π β
β0) |
22 | | nn0ge2m1nn 12490 |
. . . . . . . 8
β’ ((π β β0
β§ 2 β€ π) β
(π β 1) β
β) |
23 | 21, 2, 22 | syl2anc 585 |
. . . . . . 7
β’ ((π β Word π β§ 2 β€ π) β (π β 1) β β) |
24 | 10, 23 | eqeltrrid 2839 |
. . . . . 6
β’ ((π β Word π β§ 2 β€ π) β ((β―βπ) β 1) β
β) |
25 | 20 | nn0red 12482 |
. . . . . . 7
β’ ((π β Word π β§ 2 β€ π) β (β―βπ) β β) |
26 | 25 | lem1d 12096 |
. . . . . 6
β’ ((π β Word π β§ 2 β€ π) β ((β―βπ) β 1) β€ (β―βπ)) |
27 | | pfxn0 14583 |
. . . . . 6
β’ ((π β Word π β§ ((β―βπ) β 1) β β β§
((β―βπ) β
1) β€ (β―βπ))
β (π prefix
((β―βπ) β
1)) β β
) |
28 | 1, 24, 26, 27 | syl3anc 1372 |
. . . . 5
β’ ((π β Word π β§ 2 β€ π) β (π prefix ((β―βπ) β 1)) β β
) |
29 | | pfxlswccat 14610 |
. . . . 5
β’ (((π prefix ((β―βπ) β 1)) β Word π β§ (π prefix ((β―βπ) β 1)) β β
) β (((π prefix ((β―βπ) β 1)) prefix
((β―β(π prefix
((β―βπ) β
1))) β 1)) ++ β¨β(lastSβ(π prefix ((β―βπ) β 1)))ββ©) = (π prefix ((β―βπ) β 1))) |
30 | 18, 28, 29 | syl2anc 585 |
. . . 4
β’ ((π β Word π β§ 2 β€ π) β (((π prefix ((β―βπ) β 1)) prefix ((β―β(π prefix ((β―βπ) β 1))) β 1)) ++
β¨β(lastSβ(π prefix ((β―βπ) β 1)))ββ©) = (π prefix ((β―βπ) β 1))) |
31 | | ige2m1fz 13540 |
. . . . . . . 8
β’
(((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β ((β―βπ) β 1) β
(0...(β―βπ))) |
32 | 20, 4, 31 | syl2anc 585 |
. . . . . . 7
β’ ((π β Word π β§ 2 β€ π) β ((β―βπ) β 1) β
(0...(β―βπ))) |
33 | | pfxlen 14580 |
. . . . . . . . . 10
β’ ((π β Word π β§ ((β―βπ) β 1) β
(0...(β―βπ)))
β (β―β(π
prefix ((β―βπ)
β 1))) = ((β―βπ) β 1)) |
34 | 1, 32, 33 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ π) β (β―β(π prefix ((β―βπ) β 1))) = ((β―βπ) β 1)) |
35 | 34 | oveq1d 7376 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ π) β ((β―β(π prefix ((β―βπ) β 1))) β 1) =
(((β―βπ) β
1) β 1)) |
36 | | 0zd 12519 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ π) β 0 β β€) |
37 | | nn0ge2m1nn0 12491 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ 2 β€ π) β
(π β 1) β
β0) |
38 | 21, 2, 37 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β Word π β§ 2 β€ π) β (π β 1) β
β0) |
39 | 10, 38 | eqeltrrid 2839 |
. . . . . . . . . 10
β’ ((π β Word π β§ 2 β€ π) β ((β―βπ) β 1) β
β0) |
40 | 39 | nn0zd 12533 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ π) β ((β―βπ) β 1) β
β€) |
41 | | 1zzd 12542 |
. . . . . . . . . 10
β’ ((π β Word π β§ 2 β€ π) β 1 β β€) |
42 | 40, 41 | zsubcld 12620 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ π) β (((β―βπ) β 1) β 1) β
β€) |
43 | | 2nn0 12438 |
. . . . . . . . . . . . . 14
β’ 2 β
β0 |
44 | 43 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β Word π β§ 2 β€ π) β 2 β
β0) |
45 | | nn0sub 12471 |
. . . . . . . . . . . . . 14
β’ ((2
β β0 β§ π β β0) β (2 β€
π β (π β 2) β
β0)) |
46 | 45 | biimpa 478 |
. . . . . . . . . . . . 13
β’ (((2
β β0 β§ π β β0) β§ 2 β€
π) β (π β 2) β
β0) |
47 | 44, 21, 2, 46 | syl21anc 837 |
. . . . . . . . . . . 12
β’ ((π β Word π β§ 2 β€ π) β (π β 2) β
β0) |
48 | 47 | nn0ge0d 12484 |
. . . . . . . . . . 11
β’ ((π β Word π β§ 2 β€ π) β 0 β€ (π β 2)) |
49 | 21 | nn0cnd 12483 |
. . . . . . . . . . . 12
β’ ((π β Word π β§ 2 β€ π) β π β β) |
50 | | sub1m1 12413 |
. . . . . . . . . . . 12
β’ (π β β β ((π β 1) β 1) = (π β 2)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . 11
β’ ((π β Word π β§ 2 β€ π) β ((π β 1) β 1) = (π β 2)) |
52 | 48, 51 | breqtrrd 5137 |
. . . . . . . . . 10
β’ ((π β Word π β§ 2 β€ π) β 0 β€ ((π β 1) β 1)) |
53 | 10 | oveq1i 7371 |
. . . . . . . . . 10
β’ ((π β 1) β 1) =
(((β―βπ) β
1) β 1) |
54 | 52, 53 | breqtrdi 5150 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ π) β 0 β€ (((β―βπ) β 1) β
1)) |
55 | 24 | nnred 12176 |
. . . . . . . . . 10
β’ ((π β Word π β§ 2 β€ π) β ((β―βπ) β 1) β
β) |
56 | 55 | lem1d 12096 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ π) β (((β―βπ) β 1) β 1) β€
((β―βπ) β
1)) |
57 | 36, 40, 42, 54, 56 | elfzd 13441 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ π) β (((β―βπ) β 1) β 1) β
(0...((β―βπ)
β 1))) |
58 | 35, 57 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β Word π β§ 2 β€ π) β ((β―β(π prefix ((β―βπ) β 1))) β 1) β
(0...((β―βπ)
β 1))) |
59 | | pfxpfx 14605 |
. . . . . . 7
β’ ((π β Word π β§ ((β―βπ) β 1) β
(0...(β―βπ))
β§ ((β―β(π
prefix ((β―βπ)
β 1))) β 1) β (0...((β―βπ) β 1))) β ((π prefix ((β―βπ) β 1)) prefix ((β―β(π prefix ((β―βπ) β 1))) β 1)) =
(π prefix
((β―β(π prefix
((β―βπ) β
1))) β 1))) |
60 | 1, 32, 58, 59 | syl3anc 1372 |
. . . . . 6
β’ ((π β Word π β§ 2 β€ π) β ((π prefix ((β―βπ) β 1)) prefix ((β―β(π prefix ((β―βπ) β 1))) β 1)) =
(π prefix
((β―β(π prefix
((β―βπ) β
1))) β 1))) |
61 | 34, 10 | eqtr4di 2791 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ π) β (β―β(π prefix ((β―βπ) β 1))) = (π β 1)) |
62 | 61 | oveq1d 7376 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ π) β ((β―β(π prefix ((β―βπ) β 1))) β 1) = ((π β 1) β
1)) |
63 | 62, 51 | eqtrd 2773 |
. . . . . . 7
β’ ((π β Word π β§ 2 β€ π) β ((β―β(π prefix ((β―βπ) β 1))) β 1) = (π β 2)) |
64 | 63 | oveq2d 7377 |
. . . . . 6
β’ ((π β Word π β§ 2 β€ π) β (π prefix ((β―β(π prefix ((β―βπ) β 1))) β 1)) = (π prefix (π β 2))) |
65 | 60, 64 | eqtrd 2773 |
. . . . 5
β’ ((π β Word π β§ 2 β€ π) β ((π prefix ((β―βπ) β 1)) prefix ((β―β(π prefix ((β―βπ) β 1))) β 1)) =
(π prefix (π β 2))) |
66 | | pfxtrcfvl 14594 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (lastSβ(π prefix ((β―βπ) β 1))) = (πβ((β―βπ) β 2))) |
67 | 1, 4, 66 | syl2anc 585 |
. . . . . . 7
β’ ((π β Word π β§ 2 β€ π) β (lastSβ(π prefix ((β―βπ) β 1))) = (πβ((β―βπ) β 2))) |
68 | 3 | a1i 11 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ π) β π = (β―βπ)) |
69 | 68 | fvoveq1d 7383 |
. . . . . . 7
β’ ((π β Word π β§ 2 β€ π) β (πβ(π β 2)) = (πβ((β―βπ) β 2))) |
70 | 67, 69 | eqtr4d 2776 |
. . . . . 6
β’ ((π β Word π β§ 2 β€ π) β (lastSβ(π prefix ((β―βπ) β 1))) = (πβ(π β 2))) |
71 | 70 | s1eqd 14498 |
. . . . 5
β’ ((π β Word π β§ 2 β€ π) β β¨β(lastSβ(π prefix ((β―βπ) β 1)))ββ© =
β¨β(πβ(π β 2))ββ©) |
72 | 65, 71 | oveq12d 7379 |
. . . 4
β’ ((π β Word π β§ 2 β€ π) β (((π prefix ((β―βπ) β 1)) prefix ((β―β(π prefix ((β―βπ) β 1))) β 1)) ++
β¨β(lastSβ(π prefix ((β―βπ) β 1)))ββ©) = ((π prefix (π β 2)) ++ β¨β(πβ(π β 2))ββ©)) |
73 | 30, 72 | eqtr3d 2775 |
. . 3
β’ ((π β Word π β§ 2 β€ π) β (π prefix ((β―βπ) β 1)) = ((π prefix (π β 2)) ++ β¨β(πβ(π β 2))ββ©)) |
74 | 73 | oveq1d 7376 |
. 2
β’ ((π β Word π β§ 2 β€ π) β ((π prefix ((β―βπ) β 1)) ++ β¨β(πβ(π β 1))ββ©) = (((π prefix (π β 2)) ++ β¨β(πβ(π β 2))ββ©) ++
β¨β(πβ(π β 1))ββ©)) |
75 | | pfxcl 14574 |
. . . 4
β’ (π β Word π β (π prefix (π β 2)) β Word π) |
76 | 1, 75 | syl 17 |
. . 3
β’ ((π β Word π β§ 2 β€ π) β (π prefix (π β 2)) β Word π) |
77 | | ccatw2s1ccatws2 14852 |
. . 3
β’ ((π prefix (π β 2)) β Word π β (((π prefix (π β 2)) ++ β¨β(πβ(π β 2))ββ©) ++
β¨β(πβ(π β 1))ββ©) = ((π prefix (π β 2)) ++ β¨β(πβ(π β 2))(πβ(π β 1))ββ©)) |
78 | 76, 77 | syl 17 |
. 2
β’ ((π β Word π β§ 2 β€ π) β (((π prefix (π β 2)) ++ β¨β(πβ(π β 2))ββ©) ++
β¨β(πβ(π β 1))ββ©) = ((π prefix (π β 2)) ++ β¨β(πβ(π β 2))(πβ(π β 1))ββ©)) |
79 | 16, 74, 78 | 3eqtrd 2777 |
1
β’ ((π β Word π β§ 2 β€ π) β π = ((π prefix (π β 2)) ++ β¨β(πβ(π β 2))(πβ(π β 1))ββ©)) |