Step | Hyp | Ref
| Expression |
1 | | hashneq0 14271 |
. . . . 5
β’ (π β Word π β (0 < (β―βπ) β π β β
)) |
2 | | lencl 14428 |
. . . . . 6
β’ (π β Word π β (β―βπ) β
β0) |
3 | | nn0z 12531 |
. . . . . 6
β’
((β―βπ)
β β0 β (β―βπ) β β€) |
4 | | elnnz 12516 |
. . . . . . . 8
β’
((β―βπ)
β β β ((β―βπ) β β€ β§ 0 <
(β―βπ))) |
5 | | fzo0end 13671 |
. . . . . . . 8
β’
((β―βπ)
β β β ((β―βπ) β 1) β
(0..^(β―βπ))) |
6 | 4, 5 | sylbir 234 |
. . . . . . 7
β’
(((β―βπ)
β β€ β§ 0 < (β―βπ)) β ((β―βπ) β 1) β
(0..^(β―βπ))) |
7 | 6 | ex 414 |
. . . . . 6
β’
((β―βπ)
β β€ β (0 < (β―βπ) β ((β―βπ) β 1) β
(0..^(β―βπ)))) |
8 | 2, 3, 7 | 3syl 18 |
. . . . 5
β’ (π β Word π β (0 < (β―βπ) β ((β―βπ) β 1) β
(0..^(β―βπ)))) |
9 | 1, 8 | sylbird 260 |
. . . 4
β’ (π β Word π β (π β β
β ((β―βπ) β 1) β
(0..^(β―βπ)))) |
10 | 9 | imp 408 |
. . 3
β’ ((π β Word π β§ π β β
) β ((β―βπ) β 1) β
(0..^(β―βπ))) |
11 | | swrds1 14561 |
. . 3
β’ ((π β Word π β§ ((β―βπ) β 1) β
(0..^(β―βπ)))
β (π substr
β¨((β―βπ)
β 1), (((β―βπ) β 1) + 1)β©) =
β¨β(πβ((β―βπ) β 1))ββ©) |
12 | 10, 11 | syldan 592 |
. 2
β’ ((π β Word π β§ π β β
) β (π substr β¨((β―βπ) β 1),
(((β―βπ) β
1) + 1)β©) = β¨β(πβ((β―βπ) β 1))ββ©) |
13 | | nn0cn 12430 |
. . . . . . 7
β’
((β―βπ)
β β0 β (β―βπ) β β) |
14 | | ax-1cn 11116 |
. . . . . . 7
β’ 1 β
β |
15 | 13, 14 | jctir 522 |
. . . . . 6
β’
((β―βπ)
β β0 β ((β―βπ) β β β§ 1 β
β)) |
16 | | npcan 11417 |
. . . . . . 7
β’
(((β―βπ)
β β β§ 1 β β) β (((β―βπ) β 1) + 1) =
(β―βπ)) |
17 | 16 | eqcomd 2743 |
. . . . . 6
β’
(((β―βπ)
β β β§ 1 β β) β (β―βπ) = (((β―βπ) β 1) + 1)) |
18 | 2, 15, 17 | 3syl 18 |
. . . . 5
β’ (π β Word π β (β―βπ) = (((β―βπ) β 1) + 1)) |
19 | 18 | adantr 482 |
. . . 4
β’ ((π β Word π β§ π β β
) β (β―βπ) = (((β―βπ) β 1) +
1)) |
20 | 19 | opeq2d 4842 |
. . 3
β’ ((π β Word π β§ π β β
) β
β¨((β―βπ)
β 1), (β―βπ)β© = β¨((β―βπ) β 1),
(((β―βπ) β
1) + 1)β©) |
21 | 20 | oveq2d 7378 |
. 2
β’ ((π β Word π β§ π β β
) β (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 1), (((β―βπ) β 1) + 1)β©)) |
22 | | lsw 14459 |
. . . 4
β’ (π β Word π β (lastSβπ) = (πβ((β―βπ) β 1))) |
23 | 22 | adantr 482 |
. . 3
β’ ((π β Word π β§ π β β
) β (lastSβπ) = (πβ((β―βπ) β 1))) |
24 | 23 | s1eqd 14496 |
. 2
β’ ((π β Word π β§ π β β
) β
β¨β(lastSβπ)ββ© = β¨β(πβ((β―βπ) β
1))ββ©) |
25 | 12, 21, 24 | 3eqtr4d 2787 |
1
β’ ((π β Word π β§ π β β
) β (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
β¨β(lastSβπ)ββ©) |