Step | Hyp | Ref
| Expression |
1 | | lencl 14421 |
. . 3
β’ (π΄ β Word π΅ β (β―βπ΄) β
β0) |
2 | | eqeq2 2748 |
. . . . . 6
β’ (π = 0 β
((β―βπ₯) = π β (β―βπ₯) = 0)) |
3 | 2 | imbi1d 341 |
. . . . 5
β’ (π = 0 β
(((β―βπ₯) = π β π) β ((β―βπ₯) = 0 β π))) |
4 | 3 | ralbidv 3174 |
. . . 4
β’ (π = 0 β (βπ₯ β Word π΅((β―βπ₯) = π β π) β βπ₯ β Word π΅((β―βπ₯) = 0 β π))) |
5 | | eqeq2 2748 |
. . . . . 6
β’ (π = π β ((β―βπ₯) = π β (β―βπ₯) = π)) |
6 | 5 | imbi1d 341 |
. . . . 5
β’ (π = π β (((β―βπ₯) = π β π) β ((β―βπ₯) = π β π))) |
7 | 6 | ralbidv 3174 |
. . . 4
β’ (π = π β (βπ₯ β Word π΅((β―βπ₯) = π β π) β βπ₯ β Word π΅((β―βπ₯) = π β π))) |
8 | | eqeq2 2748 |
. . . . . 6
β’ (π = (π + 1) β ((β―βπ₯) = π β (β―βπ₯) = (π + 1))) |
9 | 8 | imbi1d 341 |
. . . . 5
β’ (π = (π + 1) β (((β―βπ₯) = π β π) β ((β―βπ₯) = (π + 1) β π))) |
10 | 9 | ralbidv 3174 |
. . . 4
β’ (π = (π + 1) β (βπ₯ β Word π΅((β―βπ₯) = π β π) β βπ₯ β Word π΅((β―βπ₯) = (π + 1) β π))) |
11 | | eqeq2 2748 |
. . . . . 6
β’ (π = (β―βπ΄) β ((β―βπ₯) = π β (β―βπ₯) = (β―βπ΄))) |
12 | 11 | imbi1d 341 |
. . . . 5
β’ (π = (β―βπ΄) β (((β―βπ₯) = π β π) β ((β―βπ₯) = (β―βπ΄) β π))) |
13 | 12 | ralbidv 3174 |
. . . 4
β’ (π = (β―βπ΄) β (βπ₯ β Word π΅((β―βπ₯) = π β π) β βπ₯ β Word π΅((β―βπ₯) = (β―βπ΄) β π))) |
14 | | hasheq0 14263 |
. . . . . 6
β’ (π₯ β Word π΅ β ((β―βπ₯) = 0 β π₯ = β
)) |
15 | | wrdind.5 |
. . . . . . 7
β’ π |
16 | | wrdind.1 |
. . . . . . 7
β’ (π₯ = β
β (π β π)) |
17 | 15, 16 | mpbiri 257 |
. . . . . 6
β’ (π₯ = β
β π) |
18 | 14, 17 | syl6bi 252 |
. . . . 5
β’ (π₯ β Word π΅ β ((β―βπ₯) = 0 β π)) |
19 | 18 | rgen 3066 |
. . . 4
β’
βπ₯ β
Word π΅((β―βπ₯) = 0 β π) |
20 | | fveqeq2 6851 |
. . . . . . 7
β’ (π₯ = π¦ β ((β―βπ₯) = π β (β―βπ¦) = π)) |
21 | | wrdind.2 |
. . . . . . 7
β’ (π₯ = π¦ β (π β π)) |
22 | 20, 21 | imbi12d 344 |
. . . . . 6
β’ (π₯ = π¦ β (((β―βπ₯) = π β π) β ((β―βπ¦) = π β π))) |
23 | 22 | cbvralvw 3225 |
. . . . 5
β’
(βπ₯ β
Word π΅((β―βπ₯) = π β π) β βπ¦ β Word π΅((β―βπ¦) = π β π)) |
24 | | simprl 769 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β π₯ β Word π΅) |
25 | | fzossfz 13591 |
. . . . . . . . . . . . . 14
β’
(0..^(β―βπ₯)) β (0...(β―βπ₯)) |
26 | | simprr 771 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β (β―βπ₯) = (π + 1)) |
27 | | nn0p1nn 12452 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (π + 1) β
β) |
28 | 27 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β (π + 1) β β) |
29 | 26, 28 | eqeltrd 2837 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β (β―βπ₯) β
β) |
30 | | fzo0end 13664 |
. . . . . . . . . . . . . . 15
β’
((β―βπ₯)
β β β ((β―βπ₯) β 1) β (0..^(β―βπ₯))) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β ((β―βπ₯) β 1) β
(0..^(β―βπ₯))) |
32 | 25, 31 | sselid 3942 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β ((β―βπ₯) β 1) β
(0...(β―βπ₯))) |
33 | | pfxlen 14571 |
. . . . . . . . . . . . 13
β’ ((π₯ β Word π΅ β§ ((β―βπ₯) β 1) β (0...(β―βπ₯))) β (β―β(π₯ prefix ((β―βπ₯) β 1))) =
((β―βπ₯) β
1)) |
34 | 24, 32, 33 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β (β―β(π₯ prefix ((β―βπ₯) β 1))) =
((β―βπ₯) β
1)) |
35 | 26 | oveq1d 7372 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β ((β―βπ₯) β 1) = ((π + 1) β
1)) |
36 | | nn0cn 12423 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β
β) |
37 | 36 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β π β β) |
38 | | ax-1cn 11109 |
. . . . . . . . . . . . 13
β’ 1 β
β |
39 | | pncan 11407 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
40 | 37, 38, 39 | sylancl 586 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β ((π + 1) β 1) = π) |
41 | 34, 35, 40 | 3eqtrd 2780 |
. . . . . . . . . . 11
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β (β―β(π₯ prefix ((β―βπ₯) β 1))) = π) |
42 | | fveqeq2 6851 |
. . . . . . . . . . . . 13
β’ (π¦ = (π₯ prefix ((β―βπ₯) β 1)) β ((β―βπ¦) = π β (β―β(π₯ prefix ((β―βπ₯) β 1))) = π)) |
43 | | vex 3449 |
. . . . . . . . . . . . . . 15
β’ π¦ β V |
44 | 43, 21 | sbcie 3782 |
. . . . . . . . . . . . . 14
β’
([π¦ / π₯]π β π) |
45 | | dfsbcq 3741 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π₯ prefix ((β―βπ₯) β 1)) β ([π¦ / π₯]π β [(π₯ prefix ((β―βπ₯) β 1)) / π₯]π)) |
46 | 44, 45 | bitr3id 284 |
. . . . . . . . . . . . 13
β’ (π¦ = (π₯ prefix ((β―βπ₯) β 1)) β (π β [(π₯ prefix ((β―βπ₯) β 1)) / π₯]π)) |
47 | 42, 46 | imbi12d 344 |
. . . . . . . . . . . 12
β’ (π¦ = (π₯ prefix ((β―βπ₯) β 1)) β (((β―βπ¦) = π β π) β ((β―β(π₯ prefix ((β―βπ₯) β 1))) = π β [(π₯ prefix ((β―βπ₯) β 1)) / π₯]π))) |
48 | | simplr 767 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β βπ¦ β Word π΅((β―βπ¦) = π β π)) |
49 | | pfxcl 14565 |
. . . . . . . . . . . . 13
β’ (π₯ β Word π΅ β (π₯ prefix ((β―βπ₯) β 1)) β Word π΅) |
50 | 49 | ad2antrl 726 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β (π₯ prefix ((β―βπ₯) β 1)) β Word π΅) |
51 | 47, 48, 50 | rspcdva 3582 |
. . . . . . . . . . 11
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β ((β―β(π₯ prefix ((β―βπ₯) β 1))) = π β [(π₯ prefix ((β―βπ₯) β 1)) / π₯]π)) |
52 | 41, 51 | mpd 15 |
. . . . . . . . . 10
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β [(π₯ prefix ((β―βπ₯) β 1)) / π₯]π) |
53 | 29 | nnge1d 12201 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β 1 β€ (β―βπ₯)) |
54 | | wrdlenge1n0 14438 |
. . . . . . . . . . . . . 14
β’ (π₯ β Word π΅ β (π₯ β β
β 1 β€
(β―βπ₯))) |
55 | 54 | ad2antrl 726 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β (π₯ β β
β 1 β€
(β―βπ₯))) |
56 | 53, 55 | mpbird 256 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β π₯ β β
) |
57 | | lswcl 14456 |
. . . . . . . . . . . 12
β’ ((π₯ β Word π΅ β§ π₯ β β
) β (lastSβπ₯) β π΅) |
58 | 24, 56, 57 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β (lastSβπ₯) β π΅) |
59 | | oveq1 7364 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π₯ prefix ((β―βπ₯) β 1)) β (π¦ ++ β¨βπ§ββ©) = ((π₯ prefix ((β―βπ₯) β 1)) ++ β¨βπ§ββ©)) |
60 | 59 | sbceq1d 3744 |
. . . . . . . . . . . . 13
β’ (π¦ = (π₯ prefix ((β―βπ₯) β 1)) β ([(π¦ ++ β¨βπ§ββ©) / π₯]π β [((π₯ prefix ((β―βπ₯) β 1)) ++ β¨βπ§ββ©) / π₯]π)) |
61 | 45, 60 | imbi12d 344 |
. . . . . . . . . . . 12
β’ (π¦ = (π₯ prefix ((β―βπ₯) β 1)) β (([π¦ / π₯]π β [(π¦ ++ β¨βπ§ββ©) / π₯]π) β ([(π₯ prefix ((β―βπ₯) β 1)) / π₯]π β [((π₯ prefix ((β―βπ₯) β 1)) ++ β¨βπ§ββ©) / π₯]π))) |
62 | | s1eq 14488 |
. . . . . . . . . . . . . . 15
β’ (π§ = (lastSβπ₯) β β¨βπ§ββ© =
β¨β(lastSβπ₯)ββ©) |
63 | 62 | oveq2d 7373 |
. . . . . . . . . . . . . 14
β’ (π§ = (lastSβπ₯) β ((π₯ prefix ((β―βπ₯) β 1)) ++ β¨βπ§ββ©) = ((π₯ prefix ((β―βπ₯) β 1)) ++
β¨β(lastSβπ₯)ββ©)) |
64 | 63 | sbceq1d 3744 |
. . . . . . . . . . . . 13
β’ (π§ = (lastSβπ₯) β ([((π₯ prefix ((β―βπ₯) β 1)) ++
β¨βπ§ββ©) / π₯]π β [((π₯ prefix ((β―βπ₯) β 1)) ++
β¨β(lastSβπ₯)ββ©) / π₯]π)) |
65 | 64 | imbi2d 340 |
. . . . . . . . . . . 12
β’ (π§ = (lastSβπ₯) β (([(π₯ prefix ((β―βπ₯) β 1)) / π₯]π β [((π₯ prefix ((β―βπ₯) β 1)) ++ β¨βπ§ββ©) / π₯]π) β ([(π₯ prefix ((β―βπ₯) β 1)) / π₯]π β [((π₯ prefix ((β―βπ₯) β 1)) ++
β¨β(lastSβπ₯)ββ©) / π₯]π))) |
66 | | wrdind.6 |
. . . . . . . . . . . . 13
β’ ((π¦ β Word π΅ β§ π§ β π΅) β (π β π)) |
67 | | ovex 7390 |
. . . . . . . . . . . . . 14
β’ (π¦ ++ β¨βπ§ββ©) β
V |
68 | | wrdind.3 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π¦ ++ β¨βπ§ββ©) β (π β π)) |
69 | 67, 68 | sbcie 3782 |
. . . . . . . . . . . . 13
β’
([(π¦ ++
β¨βπ§ββ©) / π₯]π β π) |
70 | 66, 44, 69 | 3imtr4g 295 |
. . . . . . . . . . . 12
β’ ((π¦ β Word π΅ β§ π§ β π΅) β ([π¦ / π₯]π β [(π¦ ++ β¨βπ§ββ©) / π₯]π)) |
71 | 61, 65, 70 | vtocl2ga 3535 |
. . . . . . . . . . 11
β’ (((π₯ prefix ((β―βπ₯) β 1)) β Word π΅ β§ (lastSβπ₯) β π΅) β ([(π₯ prefix ((β―βπ₯) β 1)) / π₯]π β [((π₯ prefix ((β―βπ₯) β 1)) ++
β¨β(lastSβπ₯)ββ©) / π₯]π)) |
72 | 50, 58, 71 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β ([(π₯ prefix ((β―βπ₯) β 1)) / π₯]π β [((π₯ prefix ((β―βπ₯) β 1)) ++
β¨β(lastSβπ₯)ββ©) / π₯]π)) |
73 | 52, 72 | mpd 15 |
. . . . . . . . 9
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β [((π₯ prefix ((β―βπ₯) β 1)) ++
β¨β(lastSβπ₯)ββ©) / π₯]π) |
74 | | wrdfin 14420 |
. . . . . . . . . . . . . 14
β’ (π₯ β Word π΅ β π₯ β Fin) |
75 | 74 | ad2antrl 726 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β π₯ β Fin) |
76 | | hashnncl 14266 |
. . . . . . . . . . . . 13
β’ (π₯ β Fin β
((β―βπ₯) β
β β π₯ β
β
)) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β ((β―βπ₯) β β β π₯ β β
)) |
78 | 29, 77 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β π₯ β β
) |
79 | | pfxlswccat 14601 |
. . . . . . . . . . . 12
β’ ((π₯ β Word π΅ β§ π₯ β β
) β ((π₯ prefix ((β―βπ₯) β 1)) ++
β¨β(lastSβπ₯)ββ©) = π₯) |
80 | 79 | eqcomd 2742 |
. . . . . . . . . . 11
β’ ((π₯ β Word π΅ β§ π₯ β β
) β π₯ = ((π₯ prefix ((β―βπ₯) β 1)) ++
β¨β(lastSβπ₯)ββ©)) |
81 | 24, 78, 80 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β π₯ = ((π₯ prefix ((β―βπ₯) β 1)) ++
β¨β(lastSβπ₯)ββ©)) |
82 | | sbceq1a 3750 |
. . . . . . . . . 10
β’ (π₯ = ((π₯ prefix ((β―βπ₯) β 1)) ++
β¨β(lastSβπ₯)ββ©) β (π β [((π₯ prefix ((β―βπ₯) β 1)) ++
β¨β(lastSβπ₯)ββ©) / π₯]π)) |
83 | 81, 82 | syl 17 |
. . . . . . . . 9
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β (π β [((π₯ prefix ((β―βπ₯) β 1)) ++
β¨β(lastSβπ₯)ββ©) / π₯]π)) |
84 | 73, 83 | mpbird 256 |
. . . . . . . 8
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ (π₯ β Word π΅ β§ (β―βπ₯) = (π + 1))) β π) |
85 | 84 | expr 457 |
. . . . . . 7
β’ (((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β§ π₯ β Word π΅) β ((β―βπ₯) = (π + 1) β π)) |
86 | 85 | ralrimiva 3143 |
. . . . . 6
β’ ((π β β0
β§ βπ¦ β Word
π΅((β―βπ¦) = π β π)) β βπ₯ β Word π΅((β―βπ₯) = (π + 1) β π)) |
87 | 86 | ex 413 |
. . . . 5
β’ (π β β0
β (βπ¦ β
Word π΅((β―βπ¦) = π β π) β βπ₯ β Word π΅((β―βπ₯) = (π + 1) β π))) |
88 | 23, 87 | biimtrid 241 |
. . . 4
β’ (π β β0
β (βπ₯ β
Word π΅((β―βπ₯) = π β π) β βπ₯ β Word π΅((β―βπ₯) = (π + 1) β π))) |
89 | 4, 7, 10, 13, 19, 88 | nn0ind 12598 |
. . 3
β’
((β―βπ΄)
β β0 β βπ₯ β Word π΅((β―βπ₯) = (β―βπ΄) β π)) |
90 | 1, 89 | syl 17 |
. 2
β’ (π΄ β Word π΅ β βπ₯ β Word π΅((β―βπ₯) = (β―βπ΄) β π)) |
91 | | eqidd 2737 |
. 2
β’ (π΄ β Word π΅ β (β―βπ΄) = (β―βπ΄)) |
92 | | fveqeq2 6851 |
. . . 4
β’ (π₯ = π΄ β ((β―βπ₯) = (β―βπ΄) β (β―βπ΄) = (β―βπ΄))) |
93 | | wrdind.4 |
. . . 4
β’ (π₯ = π΄ β (π β π)) |
94 | 92, 93 | imbi12d 344 |
. . 3
β’ (π₯ = π΄ β (((β―βπ₯) = (β―βπ΄) β π) β ((β―βπ΄) = (β―βπ΄) β π))) |
95 | 94 | rspcv 3577 |
. 2
β’ (π΄ β Word π΅ β (βπ₯ β Word π΅((β―βπ₯) = (β―βπ΄) β π) β ((β―βπ΄) = (β―βπ΄) β π))) |
96 | 90, 91, 95 | mp2d 49 |
1
β’ (π΄ β Word π΅ β π) |