Step | Hyp | Ref
| Expression |
1 | | pfxcl 14629 |
. . . . 5
β’ (π β Word π β (π prefix πΏ) β Word π) |
2 | | revcl 14713 |
. . . . 5
β’ ((π prefix πΏ) β Word π β (reverseβ(π prefix πΏ)) β Word π) |
3 | | wrdfn 14480 |
. . . . 5
β’
((reverseβ(π
prefix πΏ)) β Word
π β
(reverseβ(π prefix
πΏ)) Fn
(0..^(β―β(reverseβ(π prefix πΏ))))) |
4 | 1, 2, 3 | 3syl 18 |
. . . 4
β’ (π β Word π β (reverseβ(π prefix πΏ)) Fn
(0..^(β―β(reverseβ(π prefix πΏ))))) |
5 | 4 | adantr 481 |
. . 3
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β (reverseβ(π prefix πΏ)) Fn
(0..^(β―β(reverseβ(π prefix πΏ))))) |
6 | | revlen 14714 |
. . . . . . . 8
β’ ((π prefix πΏ) β Word π β (β―β(reverseβ(π prefix πΏ))) = (β―β(π prefix πΏ))) |
7 | 1, 6 | syl 17 |
. . . . . . 7
β’ (π β Word π β (β―β(reverseβ(π prefix πΏ))) = (β―β(π prefix πΏ))) |
8 | 7 | adantr 481 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β
(β―β(reverseβ(π prefix πΏ))) = (β―β(π prefix πΏ))) |
9 | | pfxlen 14635 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β (β―β(π prefix πΏ)) = πΏ) |
10 | 8, 9 | eqtrd 2772 |
. . . . 5
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β
(β―β(reverseβ(π prefix πΏ))) = πΏ) |
11 | 10 | oveq2d 7427 |
. . . 4
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β
(0..^(β―β(reverseβ(π prefix πΏ)))) = (0..^πΏ)) |
12 | 11 | fneq2d 6643 |
. . 3
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β
((reverseβ(π prefix
πΏ)) Fn
(0..^(β―β(reverseβ(π prefix πΏ)))) β (reverseβ(π prefix πΏ)) Fn (0..^πΏ))) |
13 | 5, 12 | mpbid 231 |
. 2
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β (reverseβ(π prefix πΏ)) Fn (0..^πΏ)) |
14 | | revcl 14713 |
. . . . 5
β’ (π β Word π β (reverseβπ) β Word π) |
15 | | swrdcl 14597 |
. . . . 5
β’
((reverseβπ)
β Word π β
((reverseβπ) substr
β¨((β―βπ)
β πΏ),
(β―βπ)β©)
β Word π) |
16 | | wrdfn 14480 |
. . . . 5
β’
(((reverseβπ)
substr β¨((β―βπ) β πΏ), (β―βπ)β©) β Word π β ((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©) Fn
(0..^(β―β((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©)))) |
17 | 14, 15, 16 | 3syl 18 |
. . . 4
β’ (π β Word π β ((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©) Fn
(0..^(β―β((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©)))) |
18 | 17 | adantr 481 |
. . 3
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β ((reverseβπ) substr
β¨((β―βπ)
β πΏ),
(β―βπ)β©) Fn
(0..^(β―β((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©)))) |
19 | | fznn0sub2 13610 |
. . . . . . . 8
β’ (πΏ β
(0...(β―βπ))
β ((β―βπ)
β πΏ) β
(0...(β―βπ))) |
20 | | lencl 14485 |
. . . . . . . . . 10
β’ (π β Word π β (β―βπ) β
β0) |
21 | | nn0fz0 13601 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β (β―βπ) β (0...(β―βπ))) |
22 | 20, 21 | sylib 217 |
. . . . . . . . 9
β’ (π β Word π β (β―βπ) β (0...(β―βπ))) |
23 | | revlen 14714 |
. . . . . . . . . 10
β’ (π β Word π β (β―β(reverseβπ)) = (β―βπ)) |
24 | 23 | oveq2d 7427 |
. . . . . . . . 9
β’ (π β Word π β
(0...(β―β(reverseβπ))) = (0...(β―βπ))) |
25 | 22, 24 | eleqtrrd 2836 |
. . . . . . . 8
β’ (π β Word π β (β―βπ) β
(0...(β―β(reverseβπ)))) |
26 | | swrdlen 14599 |
. . . . . . . 8
β’
(((reverseβπ)
β Word π β§
((β―βπ) β
πΏ) β
(0...(β―βπ))
β§ (β―βπ)
β (0...(β―β(reverseβπ)))) β
(β―β((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©)) = ((β―βπ) β ((β―βπ) β πΏ))) |
27 | 14, 19, 25, 26 | syl3an 1160 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π β Word π) β
(β―β((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©)) = ((β―βπ) β ((β―βπ) β πΏ))) |
28 | 27 | 3anidm13 1420 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β
(β―β((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©)) = ((β―βπ) β ((β―βπ) β πΏ))) |
29 | 20 | nn0cnd 12536 |
. . . . . . . 8
β’ (π β Word π β (β―βπ) β β) |
30 | 29 | adantr 481 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β (β―βπ) β
β) |
31 | | elfzelz 13503 |
. . . . . . . . 9
β’ (πΏ β
(0...(β―βπ))
β πΏ β
β€) |
32 | 31 | zcnd 12669 |
. . . . . . . 8
β’ (πΏ β
(0...(β―βπ))
β πΏ β
β) |
33 | 32 | adantl 482 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β πΏ β β) |
34 | 30, 33 | nncand 11578 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β ((β―βπ) β ((β―βπ) β πΏ)) = πΏ) |
35 | 28, 34 | eqtrd 2772 |
. . . . 5
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β
(β―β((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©)) = πΏ) |
36 | 35 | oveq2d 7427 |
. . . 4
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β
(0..^(β―β((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©))) = (0..^πΏ)) |
37 | 36 | fneq2d 6643 |
. . 3
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β
(((reverseβπ) substr
β¨((β―βπ)
β πΏ),
(β―βπ)β©) Fn
(0..^(β―β((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©))) β ((reverseβπ) substr
β¨((β―βπ)
β πΏ),
(β―βπ)β©) Fn
(0..^πΏ))) |
38 | 18, 37 | mpbid 231 |
. 2
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β ((reverseβπ) substr
β¨((β―βπ)
β πΏ),
(β―βπ)β©) Fn
(0..^πΏ)) |
39 | | simp1 1136 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β π β Word π) |
40 | | simp3 1138 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β π₯ β (0..^πΏ)) |
41 | 9 | oveq2d 7427 |
. . . . . . . 8
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β
(0..^(β―β(π
prefix πΏ))) = (0..^πΏ)) |
42 | 41 | 3adant3 1132 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (0..^(β―β(π prefix πΏ))) = (0..^πΏ)) |
43 | 40, 42 | eleqtrrd 2836 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β π₯ β (0..^(β―β(π prefix πΏ)))) |
44 | | revfv 14715 |
. . . . . . 7
β’ (((π prefix πΏ) β Word π β§ π₯ β (0..^(β―β(π prefix πΏ)))) β ((reverseβ(π prefix πΏ))βπ₯) = ((π prefix πΏ)β(((β―β(π prefix πΏ)) β 1) β π₯))) |
45 | 1, 44 | sylan 580 |
. . . . . 6
β’ ((π β Word π β§ π₯ β (0..^(β―β(π prefix πΏ)))) β ((reverseβ(π prefix πΏ))βπ₯) = ((π prefix πΏ)β(((β―β(π prefix πΏ)) β 1) β π₯))) |
46 | 39, 43, 45 | syl2anc 584 |
. . . . 5
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((reverseβ(π prefix πΏ))βπ₯) = ((π prefix πΏ)β(((β―β(π prefix πΏ)) β 1) β π₯))) |
47 | 9 | oveq1d 7426 |
. . . . . . . 8
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β
((β―β(π prefix
πΏ)) β 1) = (πΏ β 1)) |
48 | 47 | oveq1d 7426 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β
(((β―β(π prefix
πΏ)) β 1) β
π₯) = ((πΏ β 1) β π₯)) |
49 | 48 | fveq2d 6895 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β ((π prefix πΏ)β(((β―β(π prefix πΏ)) β 1) β π₯)) = ((π prefix πΏ)β((πΏ β 1) β π₯))) |
50 | 49 | 3adant3 1132 |
. . . . 5
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((π prefix πΏ)β(((β―β(π prefix πΏ)) β 1) β π₯)) = ((π prefix πΏ)β((πΏ β 1) β π₯))) |
51 | 32 | 3ad2ant2 1134 |
. . . . . . . 8
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β πΏ β β) |
52 | | elfzoelz 13634 |
. . . . . . . . . 10
β’ (π₯ β (0..^πΏ) β π₯ β β€) |
53 | 52 | zcnd 12669 |
. . . . . . . . 9
β’ (π₯ β (0..^πΏ) β π₯ β β) |
54 | 53 | 3ad2ant3 1135 |
. . . . . . . 8
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β π₯ β β) |
55 | | 1cnd 11211 |
. . . . . . . 8
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β 1 β β) |
56 | 51, 54, 55 | sub32d 11605 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((πΏ β π₯) β 1) = ((πΏ β 1) β π₯)) |
57 | | ubmelm1fzo 13730 |
. . . . . . . 8
β’ (π₯ β (0..^πΏ) β ((πΏ β π₯) β 1) β (0..^πΏ)) |
58 | 57 | 3ad2ant3 1135 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((πΏ β π₯) β 1) β (0..^πΏ)) |
59 | 56, 58 | eqeltrrd 2834 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((πΏ β 1) β π₯) β (0..^πΏ)) |
60 | | pfxfv 14634 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ ((πΏ β 1) β π₯) β (0..^πΏ)) β ((π prefix πΏ)β((πΏ β 1) β π₯)) = (πβ((πΏ β 1) β π₯))) |
61 | 59, 60 | syld3an3 1409 |
. . . . 5
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((π prefix πΏ)β((πΏ β 1) β π₯)) = (πβ((πΏ β 1) β π₯))) |
62 | 46, 50, 61 | 3eqtrd 2776 |
. . . 4
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((reverseβ(π prefix πΏ))βπ₯) = (πβ((πΏ β 1) β π₯))) |
63 | 34 | oveq2d 7427 |
. . . . . . . 8
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β
(0..^((β―βπ)
β ((β―βπ)
β πΏ))) = (0..^πΏ)) |
64 | 63 | eleq2d 2819 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β (π₯ β (0..^((β―βπ) β ((β―βπ) β πΏ))) β π₯ β (0..^πΏ))) |
65 | 64 | biimp3ar 1470 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β π₯ β (0..^((β―βπ) β ((β―βπ) β πΏ)))) |
66 | | id 22 |
. . . . . . . . 9
β’ ((π β Word π β§ ((β―βπ) β πΏ) β (0...(β―βπ)) β§ π β Word π) β (π β Word π β§ ((β―βπ) β πΏ) β (0...(β―βπ)) β§ π β Word π)) |
67 | 66 | 3anidm13 1420 |
. . . . . . . 8
β’ ((π β Word π β§ ((β―βπ) β πΏ) β (0...(β―βπ))) β (π β Word π β§ ((β―βπ) β πΏ) β (0...(β―βπ)) β§ π β Word π)) |
68 | | swrdfv 14600 |
. . . . . . . . . 10
β’
((((reverseβπ)
β Word π β§
((β―βπ) β
πΏ) β
(0...(β―βπ))
β§ (β―βπ)
β (0...(β―β(reverseβπ)))) β§ π₯ β (0..^((β―βπ) β ((β―βπ) β πΏ)))) β (((reverseβπ) substr
β¨((β―βπ)
β πΏ),
(β―βπ)β©)βπ₯) = ((reverseβπ)β(π₯ + ((β―βπ) β πΏ)))) |
69 | 14, 68 | syl3anl1 1412 |
. . . . . . . . 9
β’ (((π β Word π β§ ((β―βπ) β πΏ) β (0...(β―βπ)) β§ (β―βπ) β
(0...(β―β(reverseβπ)))) β§ π₯ β (0..^((β―βπ) β ((β―βπ) β πΏ)))) β (((reverseβπ) substr
β¨((β―βπ)
β πΏ),
(β―βπ)β©)βπ₯) = ((reverseβπ)β(π₯ + ((β―βπ) β πΏ)))) |
70 | 25, 69 | syl3anl3 1414 |
. . . . . . . 8
β’ (((π β Word π β§ ((β―βπ) β πΏ) β (0...(β―βπ)) β§ π β Word π) β§ π₯ β (0..^((β―βπ) β ((β―βπ) β πΏ)))) β (((reverseβπ) substr
β¨((β―βπ)
β πΏ),
(β―βπ)β©)βπ₯) = ((reverseβπ)β(π₯ + ((β―βπ) β πΏ)))) |
71 | 67, 70 | stoic3 1778 |
. . . . . . 7
β’ ((π β Word π β§ ((β―βπ) β πΏ) β (0...(β―βπ)) β§ π₯ β (0..^((β―βπ) β ((β―βπ) β πΏ)))) β (((reverseβπ) substr
β¨((β―βπ)
β πΏ),
(β―βπ)β©)βπ₯) = ((reverseβπ)β(π₯ + ((β―βπ) β πΏ)))) |
72 | 19, 71 | syl3an2 1164 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^((β―βπ) β ((β―βπ) β πΏ)))) β (((reverseβπ) substr
β¨((β―βπ)
β πΏ),
(β―βπ)β©)βπ₯) = ((reverseβπ)β(π₯ + ((β―βπ) β πΏ)))) |
73 | 65, 72 | syld3an3 1409 |
. . . . 5
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©)βπ₯) = ((reverseβπ)β(π₯ + ((β―βπ) β πΏ)))) |
74 | | 0z 12571 |
. . . . . . . . . 10
β’ 0 β
β€ |
75 | | elfzuz3 13500 |
. . . . . . . . . . 11
β’ (πΏ β
(0...(β―βπ))
β (β―βπ)
β (β€β₯βπΏ)) |
76 | 32 | addlidd 11417 |
. . . . . . . . . . . 12
β’ (πΏ β
(0...(β―βπ))
β (0 + πΏ) = πΏ) |
77 | 76 | fveq2d 6895 |
. . . . . . . . . . 11
β’ (πΏ β
(0...(β―βπ))
β (β€β₯β(0 + πΏ)) = (β€β₯βπΏ)) |
78 | 75, 77 | eleqtrrd 2836 |
. . . . . . . . . 10
β’ (πΏ β
(0...(β―βπ))
β (β―βπ)
β (β€β₯β(0 + πΏ))) |
79 | | eluzsub 12854 |
. . . . . . . . . 10
β’ ((0
β β€ β§ πΏ
β β€ β§ (β―βπ) β (β€β₯β(0 +
πΏ))) β
((β―βπ) β
πΏ) β
(β€β₯β0)) |
80 | 74, 31, 78, 79 | mp3an2i 1466 |
. . . . . . . . 9
β’ (πΏ β
(0...(β―βπ))
β ((β―βπ)
β πΏ) β
(β€β₯β0)) |
81 | | fzoss1 13661 |
. . . . . . . . 9
β’
(((β―βπ)
β πΏ) β
(β€β₯β0) β (((β―βπ) β πΏ)..^(β―βπ)) β (0..^(β―βπ))) |
82 | 80, 81 | syl 17 |
. . . . . . . 8
β’ (πΏ β
(0...(β―βπ))
β (((β―βπ)
β πΏ)..^(β―βπ)) β (0..^(β―βπ))) |
83 | 82 | 3ad2ant2 1134 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (((β―βπ) β πΏ)..^(β―βπ)) β (0..^(β―βπ))) |
84 | 20 | nn0zd 12586 |
. . . . . . . . . . 11
β’ (π β Word π β (β―βπ) β β€) |
85 | 84 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (β―βπ) β β€) |
86 | 31 | 3ad2ant2 1134 |
. . . . . . . . . 10
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β πΏ β β€) |
87 | 85, 86 | zsubcld 12673 |
. . . . . . . . 9
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((β―βπ) β πΏ) β β€) |
88 | | fzo0addel 13688 |
. . . . . . . . 9
β’ ((π₯ β (0..^πΏ) β§ ((β―βπ) β πΏ) β β€) β (π₯ + ((β―βπ) β πΏ)) β (((β―βπ) β πΏ)..^(πΏ + ((β―βπ) β πΏ)))) |
89 | 40, 87, 88 | syl2anc 584 |
. . . . . . . 8
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (π₯ + ((β―βπ) β πΏ)) β (((β―βπ) β πΏ)..^(πΏ + ((β―βπ) β πΏ)))) |
90 | 30 | 3adant3 1132 |
. . . . . . . . . 10
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (β―βπ) β β) |
91 | 51, 90 | pncan3d 11576 |
. . . . . . . . 9
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (πΏ + ((β―βπ) β πΏ)) = (β―βπ)) |
92 | 91 | oveq2d 7427 |
. . . . . . . 8
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (((β―βπ) β πΏ)..^(πΏ + ((β―βπ) β πΏ))) = (((β―βπ) β πΏ)..^(β―βπ))) |
93 | 89, 92 | eleqtrd 2835 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (π₯ + ((β―βπ) β πΏ)) β (((β―βπ) β πΏ)..^(β―βπ))) |
94 | 83, 93 | sseldd 3983 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (π₯ + ((β―βπ) β πΏ)) β (0..^(β―βπ))) |
95 | | revfv 14715 |
. . . . . 6
β’ ((π β Word π β§ (π₯ + ((β―βπ) β πΏ)) β (0..^(β―βπ))) β ((reverseβπ)β(π₯ + ((β―βπ) β πΏ))) = (πβ(((β―βπ) β 1) β (π₯ + ((β―βπ) β πΏ))))) |
96 | 39, 94, 95 | syl2anc 584 |
. . . . 5
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((reverseβπ)β(π₯ + ((β―βπ) β πΏ))) = (πβ(((β―βπ) β 1) β (π₯ + ((β―βπ) β πΏ))))) |
97 | 90, 55 | subcld 11573 |
. . . . . . . . 9
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((β―βπ) β 1) β
β) |
98 | 87 | zcnd 12669 |
. . . . . . . . 9
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((β―βπ) β πΏ) β β) |
99 | 97, 54, 98 | sub32d 11605 |
. . . . . . . 8
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((((β―βπ) β 1) β π₯) β ((β―βπ) β πΏ)) = ((((β―βπ) β 1) β ((β―βπ) β πΏ)) β π₯)) |
100 | 97, 54, 98 | subsub4d 11604 |
. . . . . . . 8
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((((β―βπ) β 1) β π₯) β ((β―βπ) β πΏ)) = (((β―βπ) β 1) β (π₯ + ((β―βπ) β πΏ)))) |
101 | 90, 55, 98 | sub32d 11605 |
. . . . . . . . 9
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (((β―βπ) β 1) β ((β―βπ) β πΏ)) = (((β―βπ) β ((β―βπ) β πΏ)) β 1)) |
102 | 101 | oveq1d 7426 |
. . . . . . . 8
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((((β―βπ) β 1) β
((β―βπ) β
πΏ)) β π₯) = ((((β―βπ) β ((β―βπ) β πΏ)) β 1) β π₯)) |
103 | 99, 100, 102 | 3eqtr3d 2780 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (((β―βπ) β 1) β (π₯ + ((β―βπ) β πΏ))) = ((((β―βπ) β ((β―βπ) β πΏ)) β 1) β π₯)) |
104 | 34 | 3adant3 1132 |
. . . . . . . . 9
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((β―βπ) β ((β―βπ) β πΏ)) = πΏ) |
105 | 104 | oveq1d 7426 |
. . . . . . . 8
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (((β―βπ) β ((β―βπ) β πΏ)) β 1) = (πΏ β 1)) |
106 | 105 | oveq1d 7426 |
. . . . . . 7
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((((β―βπ) β ((β―βπ) β πΏ)) β 1) β π₯) = ((πΏ β 1) β π₯)) |
107 | 103, 106 | eqtrd 2772 |
. . . . . 6
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (((β―βπ) β 1) β (π₯ + ((β―βπ) β πΏ))) = ((πΏ β 1) β π₯)) |
108 | 107 | fveq2d 6895 |
. . . . 5
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (πβ(((β―βπ) β 1) β (π₯ + ((β―βπ) β πΏ)))) = (πβ((πΏ β 1) β π₯))) |
109 | 73, 96, 108 | 3eqtrd 2776 |
. . . 4
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β (((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©)βπ₯) = (πβ((πΏ β 1) β π₯))) |
110 | 62, 109 | eqtr4d 2775 |
. . 3
β’ ((π β Word π β§ πΏ β (0...(β―βπ)) β§ π₯ β (0..^πΏ)) β ((reverseβ(π prefix πΏ))βπ₯) = (((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©)βπ₯)) |
111 | 110 | 3expa 1118 |
. 2
β’ (((π β Word π β§ πΏ β (0...(β―βπ))) β§ π₯ β (0..^πΏ)) β ((reverseβ(π prefix πΏ))βπ₯) = (((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©)βπ₯)) |
112 | 13, 38, 111 | eqfnfvd 7035 |
1
β’ ((π β Word π β§ πΏ β (0...(β―βπ))) β (reverseβ(π prefix πΏ)) = ((reverseβπ) substr β¨((β―βπ) β πΏ), (β―βπ)β©)) |