Step | Hyp | Ref
| Expression |
1 | | oveq1 7369 |
. . . 4
β’ (π = (π prefix (β―βπ)) β (π ++ β¨β(lastSβπ)ββ©) = ((π prefix (β―βπ)) ++
β¨β(lastSβπ)ββ©)) |
2 | 1 | adantl 483 |
. . 3
β’ (((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β§ π = (π prefix (β―βπ))) β (π ++ β¨β(lastSβπ)ββ©) = ((π prefix (β―βπ)) ++
β¨β(lastSβπ)ββ©)) |
3 | | lencl 14428 |
. . . . . . . . . . . 12
β’ (π β Word π β (β―βπ) β
β0) |
4 | 3 | nn0cnd 12482 |
. . . . . . . . . . 11
β’ (π β Word π β (β―βπ) β β) |
5 | | pncan1 11586 |
. . . . . . . . . . 11
β’
((β―βπ)
β β β (((β―βπ) + 1) β 1) = (β―βπ)) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
β’ (π β Word π β (((β―βπ) + 1) β 1) = (β―βπ)) |
7 | 6 | eqcomd 2743 |
. . . . . . . . 9
β’ (π β Word π β (β―βπ) = (((β―βπ) + 1) β 1)) |
8 | 7 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (β―βπ) = (((β―βπ) + 1) β
1)) |
9 | | oveq1 7369 |
. . . . . . . . . 10
β’
((β―βπ) =
((β―βπ) + 1)
β ((β―βπ)
β 1) = (((β―βπ) + 1) β 1)) |
10 | 9 | eqcomd 2743 |
. . . . . . . . 9
β’
((β―βπ) =
((β―βπ) + 1)
β (((β―βπ)
+ 1) β 1) = ((β―βπ) β 1)) |
11 | 10 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (((β―βπ) + 1) β 1) =
((β―βπ) β
1)) |
12 | 8, 11 | eqtrd 2777 |
. . . . . . 7
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (β―βπ) = ((β―βπ) β 1)) |
13 | 12 | oveq2d 7378 |
. . . . . 6
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π prefix (β―βπ)) = (π prefix ((β―βπ) β 1))) |
14 | 13 | oveq1d 7377 |
. . . . 5
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β ((π prefix (β―βπ)) ++ β¨β(lastSβπ)ββ©) = ((π prefix ((β―βπ) β 1)) ++
β¨β(lastSβπ)ββ©)) |
15 | | simp2 1138 |
. . . . . 6
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β π β Word π) |
16 | | nn0p1gt0 12449 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β 0 < ((β―βπ) + 1)) |
17 | 3, 16 | syl 17 |
. . . . . . . . 9
β’ (π β Word π β 0 < ((β―βπ) + 1)) |
18 | 17 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β 0 < ((β―βπ) + 1)) |
19 | | breq2 5114 |
. . . . . . . . 9
β’
((β―βπ) =
((β―βπ) + 1)
β (0 < (β―βπ) β 0 < ((β―βπ) + 1))) |
20 | 19 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (0 < (β―βπ) β 0 <
((β―βπ) +
1))) |
21 | 18, 20 | mpbird 257 |
. . . . . . 7
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β 0 < (β―βπ)) |
22 | | hashneq0 14271 |
. . . . . . . 8
β’ (π β Word π β (0 < (β―βπ) β π β β
)) |
23 | 22 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (0 < (β―βπ) β π β β
)) |
24 | 21, 23 | mpbid 231 |
. . . . . 6
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β π β β
) |
25 | | pfxlswccat 14608 |
. . . . . 6
β’ ((π β Word π β§ π β β
) β ((π prefix ((β―βπ) β 1)) ++
β¨β(lastSβπ)ββ©) = π) |
26 | 15, 24, 25 | syl2anc 585 |
. . . . 5
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β ((π prefix ((β―βπ) β 1)) ++
β¨β(lastSβπ)ββ©) = π) |
27 | 14, 26 | eqtrd 2777 |
. . . 4
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β ((π prefix (β―βπ)) ++ β¨β(lastSβπ)ββ©) = π) |
28 | 27 | adantr 482 |
. . 3
β’ (((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β§ π = (π prefix (β―βπ))) β ((π prefix (β―βπ)) ++ β¨β(lastSβπ)ββ©) = π) |
29 | 2, 28 | eqtr2d 2778 |
. 2
β’ (((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β§ π = (π prefix (β―βπ))) β π = (π ++ β¨β(lastSβπ)ββ©)) |
30 | 29 | ex 414 |
1
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π = (π prefix (β―βπ)) β π = (π ++ β¨β(lastSβπ)ββ©))) |