Step | Hyp | Ref
| Expression |
1 | | ccatcl 14469 |
. . . 4
β’ ((π β Word π΄ β§ π β Word π΄) β (π ++ π) β Word π΄) |
2 | | revcl 14656 |
. . . 4
β’ ((π ++ π) β Word π΄ β (reverseβ(π ++ π)) β Word π΄) |
3 | | wrdfn 14423 |
. . . 4
β’
((reverseβ(π
++ π)) β Word π΄ β (reverseβ(π ++ π)) Fn
(0..^(β―β(reverseβ(π ++ π))))) |
4 | 1, 2, 3 | 3syl 18 |
. . 3
β’ ((π β Word π΄ β§ π β Word π΄) β (reverseβ(π ++ π)) Fn
(0..^(β―β(reverseβ(π ++ π))))) |
5 | | revlen 14657 |
. . . . . . 7
β’ ((π ++ π) β Word π΄ β (β―β(reverseβ(π ++ π))) = (β―β(π ++ π))) |
6 | 1, 5 | syl 17 |
. . . . . 6
β’ ((π β Word π΄ β§ π β Word π΄) β
(β―β(reverseβ(π ++ π))) = (β―β(π ++ π))) |
7 | | ccatlen 14470 |
. . . . . 6
β’ ((π β Word π΄ β§ π β Word π΄) β (β―β(π ++ π)) = ((β―βπ) + (β―βπ))) |
8 | | lencl 14428 |
. . . . . . . 8
β’ (π β Word π΄ β (β―βπ) β
β0) |
9 | 8 | nn0cnd 12482 |
. . . . . . 7
β’ (π β Word π΄ β (β―βπ) β β) |
10 | | lencl 14428 |
. . . . . . . 8
β’ (π β Word π΄ β (β―βπ) β
β0) |
11 | 10 | nn0cnd 12482 |
. . . . . . 7
β’ (π β Word π΄ β (β―βπ) β β) |
12 | | addcom 11348 |
. . . . . . 7
β’
(((β―βπ)
β β β§ (β―βπ) β β) β
((β―βπ) +
(β―βπ)) =
((β―βπ) +
(β―βπ))) |
13 | 9, 11, 12 | syl2an 597 |
. . . . . 6
β’ ((π β Word π΄ β§ π β Word π΄) β ((β―βπ) + (β―βπ)) = ((β―βπ) + (β―βπ))) |
14 | 6, 7, 13 | 3eqtrd 2781 |
. . . . 5
β’ ((π β Word π΄ β§ π β Word π΄) β
(β―β(reverseβ(π ++ π))) = ((β―βπ) + (β―βπ))) |
15 | 14 | oveq2d 7378 |
. . . 4
β’ ((π β Word π΄ β§ π β Word π΄) β
(0..^(β―β(reverseβ(π ++ π)))) = (0..^((β―βπ) + (β―βπ)))) |
16 | 15 | fneq2d 6601 |
. . 3
β’ ((π β Word π΄ β§ π β Word π΄) β ((reverseβ(π ++ π)) Fn
(0..^(β―β(reverseβ(π ++ π)))) β (reverseβ(π ++ π)) Fn (0..^((β―βπ) + (β―βπ))))) |
17 | 4, 16 | mpbid 231 |
. 2
β’ ((π β Word π΄ β§ π β Word π΄) β (reverseβ(π ++ π)) Fn (0..^((β―βπ) + (β―βπ)))) |
18 | | revcl 14656 |
. . . . 5
β’ (π β Word π΄ β (reverseβπ) β Word π΄) |
19 | | revcl 14656 |
. . . . 5
β’ (π β Word π΄ β (reverseβπ) β Word π΄) |
20 | | ccatcl 14469 |
. . . . 5
β’
(((reverseβπ)
β Word π΄ β§
(reverseβπ) β
Word π΄) β
((reverseβπ) ++
(reverseβπ)) β
Word π΄) |
21 | 18, 19, 20 | syl2anr 598 |
. . . 4
β’ ((π β Word π΄ β§ π β Word π΄) β ((reverseβπ) ++ (reverseβπ)) β Word π΄) |
22 | | wrdfn 14423 |
. . . 4
β’
(((reverseβπ)
++ (reverseβπ))
β Word π΄ β
((reverseβπ) ++
(reverseβπ)) Fn
(0..^(β―β((reverseβπ) ++ (reverseβπ))))) |
23 | 21, 22 | syl 17 |
. . 3
β’ ((π β Word π΄ β§ π β Word π΄) β ((reverseβπ) ++ (reverseβπ)) Fn
(0..^(β―β((reverseβπ) ++ (reverseβπ))))) |
24 | | ccatlen 14470 |
. . . . . . 7
β’
(((reverseβπ)
β Word π΄ β§
(reverseβπ) β
Word π΄) β
(β―β((reverseβπ) ++ (reverseβπ))) = ((β―β(reverseβπ)) +
(β―β(reverseβπ)))) |
25 | 18, 19, 24 | syl2anr 598 |
. . . . . 6
β’ ((π β Word π΄ β§ π β Word π΄) β
(β―β((reverseβπ) ++ (reverseβπ))) = ((β―β(reverseβπ)) +
(β―β(reverseβπ)))) |
26 | | revlen 14657 |
. . . . . . 7
β’ (π β Word π΄ β (β―β(reverseβπ)) = (β―βπ)) |
27 | | revlen 14657 |
. . . . . . 7
β’ (π β Word π΄ β (β―β(reverseβπ)) = (β―βπ)) |
28 | 26, 27 | oveqan12rd 7382 |
. . . . . 6
β’ ((π β Word π΄ β§ π β Word π΄) β
((β―β(reverseβπ)) + (β―β(reverseβπ))) = ((β―βπ) + (β―βπ))) |
29 | 25, 28 | eqtrd 2777 |
. . . . 5
β’ ((π β Word π΄ β§ π β Word π΄) β
(β―β((reverseβπ) ++ (reverseβπ))) = ((β―βπ) + (β―βπ))) |
30 | 29 | oveq2d 7378 |
. . . 4
β’ ((π β Word π΄ β§ π β Word π΄) β
(0..^(β―β((reverseβπ) ++ (reverseβπ)))) = (0..^((β―βπ) + (β―βπ)))) |
31 | 30 | fneq2d 6601 |
. . 3
β’ ((π β Word π΄ β§ π β Word π΄) β (((reverseβπ) ++ (reverseβπ)) Fn
(0..^(β―β((reverseβπ) ++ (reverseβπ)))) β ((reverseβπ) ++ (reverseβπ)) Fn (0..^((β―βπ) + (β―βπ))))) |
32 | 23, 31 | mpbid 231 |
. 2
β’ ((π β Word π΄ β§ π β Word π΄) β ((reverseβπ) ++ (reverseβπ)) Fn (0..^((β―βπ) + (β―βπ)))) |
33 | | id 22 |
. . . 4
β’ (π₯ β
(0..^((β―βπ) +
(β―βπ))) β
π₯ β
(0..^((β―βπ) +
(β―βπ)))) |
34 | 10 | nn0zd 12532 |
. . . . 5
β’ (π β Word π΄ β (β―βπ) β β€) |
35 | 34 | adantl 483 |
. . . 4
β’ ((π β Word π΄ β§ π β Word π΄) β (β―βπ) β β€) |
36 | | fzospliti 13611 |
. . . 4
β’ ((π₯ β
(0..^((β―βπ) +
(β―βπ))) β§
(β―βπ) β
β€) β (π₯ β
(0..^(β―βπ))
β¨ π₯ β
((β―βπ)..^((β―βπ) + (β―βπ))))) |
37 | 33, 35, 36 | syl2anr 598 |
. . 3
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^((β―βπ) + (β―βπ)))) β (π₯ β (0..^(β―βπ)) β¨ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ))))) |
38 | | simpll 766 |
. . . . . . 7
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β π β Word π΄) |
39 | | simplr 768 |
. . . . . . 7
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β π β Word π΄) |
40 | | fzoval 13580 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β β€ β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
41 | 34, 40 | syl 17 |
. . . . . . . . . . . 12
β’ (π β Word π΄ β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
42 | 41 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β Word π΄ β§ π β Word π΄) β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
43 | 42 | eleq2d 2824 |
. . . . . . . . . 10
β’ ((π β Word π΄ β§ π β Word π΄) β (π₯ β (0..^(β―βπ)) β π₯ β (0...((β―βπ) β 1)))) |
44 | 43 | biimpa 478 |
. . . . . . . . 9
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β π₯ β (0...((β―βπ) β 1))) |
45 | | fznn0sub2 13555 |
. . . . . . . . 9
β’ (π₯ β
(0...((β―βπ)
β 1)) β (((β―βπ) β 1) β π₯) β (0...((β―βπ) β 1))) |
46 | 44, 45 | syl 17 |
. . . . . . . 8
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β (((β―βπ) β 1) β π₯) β
(0...((β―βπ)
β 1))) |
47 | 41 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
48 | 46, 47 | eleqtrrd 2841 |
. . . . . . 7
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β (((β―βπ) β 1) β π₯) β
(0..^(β―βπ))) |
49 | | ccatval3 14474 |
. . . . . . 7
β’ ((π β Word π΄ β§ π β Word π΄ β§ (((β―βπ) β 1) β π₯) β (0..^(β―βπ))) β ((π ++ π)β((((β―βπ) β 1) β π₯) + (β―βπ))) = (πβ(((β―βπ) β 1) β π₯))) |
50 | 38, 39, 48, 49 | syl3anc 1372 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β ((π ++ π)β((((β―βπ) β 1) β π₯) + (β―βπ))) = (πβ(((β―βπ) β 1) β π₯))) |
51 | 7, 13 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π β Word π΄ β§ π β Word π΄) β (β―β(π ++ π)) = ((β―βπ) + (β―βπ))) |
52 | 51 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π β Word π΄ β§ π β Word π΄) β ((β―β(π ++ π)) β 1) = (((β―βπ) + (β―βπ)) β 1)) |
53 | 11 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β Word π΄ β§ π β Word π΄) β (β―βπ) β β) |
54 | 9 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β Word π΄ β§ π β Word π΄) β (β―βπ) β β) |
55 | | 1cnd 11157 |
. . . . . . . . . . . 12
β’ ((π β Word π΄ β§ π β Word π΄) β 1 β β) |
56 | 53, 54, 55 | addsubd 11540 |
. . . . . . . . . . 11
β’ ((π β Word π΄ β§ π β Word π΄) β (((β―βπ) + (β―βπ)) β 1) = (((β―βπ) β 1) +
(β―βπ))) |
57 | 52, 56 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β Word π΄ β§ π β Word π΄) β ((β―β(π ++ π)) β 1) = (((β―βπ) β 1) +
(β―βπ))) |
58 | 57 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π β Word π΄ β§ π β Word π΄) β (((β―β(π ++ π)) β 1) β π₯) = ((((β―βπ) β 1) + (β―βπ)) β π₯)) |
59 | 58 | adantr 482 |
. . . . . . . 8
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β (((β―β(π ++ π)) β 1) β π₯) = ((((β―βπ) β 1) + (β―βπ)) β π₯)) |
60 | | peano2zm 12553 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β€ β ((β―βπ) β 1) β
β€) |
61 | 34, 60 | syl 17 |
. . . . . . . . . . 11
β’ (π β Word π΄ β ((β―βπ) β 1) β
β€) |
62 | 61 | zcnd 12615 |
. . . . . . . . . 10
β’ (π β Word π΄ β ((β―βπ) β 1) β
β) |
63 | 62 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β ((β―βπ) β 1) β
β) |
64 | 9 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β (β―βπ) β β) |
65 | | elfzoelz 13579 |
. . . . . . . . . . 11
β’ (π₯ β
(0..^(β―βπ))
β π₯ β
β€) |
66 | 65 | zcnd 12615 |
. . . . . . . . . 10
β’ (π₯ β
(0..^(β―βπ))
β π₯ β
β) |
67 | 66 | adantl 483 |
. . . . . . . . 9
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β π₯ β β) |
68 | 63, 64, 67 | addsubd 11540 |
. . . . . . . 8
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β ((((β―βπ) β 1) +
(β―βπ)) β
π₯) =
((((β―βπ)
β 1) β π₯) +
(β―βπ))) |
69 | 59, 68 | eqtrd 2777 |
. . . . . . 7
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β (((β―β(π ++ π)) β 1) β π₯) = ((((β―βπ) β 1) β π₯) + (β―βπ))) |
70 | 69 | fveq2d 6851 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β ((π ++ π)β(((β―β(π ++ π)) β 1) β π₯)) = ((π ++ π)β((((β―βπ) β 1) β π₯) + (β―βπ)))) |
71 | | revfv 14658 |
. . . . . . 7
β’ ((π β Word π΄ β§ π₯ β (0..^(β―βπ))) β ((reverseβπ)βπ₯) = (πβ(((β―βπ) β 1) β π₯))) |
72 | 71 | adantll 713 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β ((reverseβπ)βπ₯) = (πβ(((β―βπ) β 1) β π₯))) |
73 | 50, 70, 72 | 3eqtr4d 2787 |
. . . . 5
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β ((π ++ π)β(((β―β(π ++ π)) β 1) β π₯)) = ((reverseβπ)βπ₯)) |
74 | 34 | uzidd 12786 |
. . . . . . . . . 10
β’ (π β Word π΄ β (β―βπ) β
(β€β₯β(β―βπ))) |
75 | | uzaddcl 12836 |
. . . . . . . . . 10
β’
(((β―βπ)
β (β€β₯β(β―βπ)) β§ (β―βπ) β β0) β
((β―βπ) +
(β―βπ)) β
(β€β₯β(β―βπ))) |
76 | 74, 8, 75 | syl2anr 598 |
. . . . . . . . 9
β’ ((π β Word π΄ β§ π β Word π΄) β ((β―βπ) + (β―βπ)) β
(β€β₯β(β―βπ))) |
77 | 51, 76 | eqeltrd 2838 |
. . . . . . . 8
β’ ((π β Word π΄ β§ π β Word π΄) β (β―β(π ++ π)) β
(β€β₯β(β―βπ))) |
78 | | fzoss2 13607 |
. . . . . . . 8
β’
((β―β(π
++ π)) β
(β€β₯β(β―βπ)) β (0..^(β―βπ)) β
(0..^(β―β(π ++
π)))) |
79 | 77, 78 | syl 17 |
. . . . . . 7
β’ ((π β Word π΄ β§ π β Word π΄) β (0..^(β―βπ)) β
(0..^(β―β(π ++
π)))) |
80 | 79 | sselda 3949 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β π₯ β (0..^(β―β(π ++ π)))) |
81 | | revfv 14658 |
. . . . . 6
β’ (((π ++ π) β Word π΄ β§ π₯ β (0..^(β―β(π ++ π)))) β ((reverseβ(π ++ π))βπ₯) = ((π ++ π)β(((β―β(π ++ π)) β 1) β π₯))) |
82 | 1, 80, 81 | syl2an2r 684 |
. . . . 5
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β ((reverseβ(π ++ π))βπ₯) = ((π ++ π)β(((β―β(π ++ π)) β 1) β π₯))) |
83 | 18 | ad2antlr 726 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β (reverseβπ) β Word π΄) |
84 | 19 | ad2antrr 725 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β (reverseβπ) β Word π΄) |
85 | 26 | adantl 483 |
. . . . . . . . 9
β’ ((π β Word π΄ β§ π β Word π΄) β (β―β(reverseβπ)) = (β―βπ)) |
86 | 85 | oveq2d 7378 |
. . . . . . . 8
β’ ((π β Word π΄ β§ π β Word π΄) β
(0..^(β―β(reverseβπ))) = (0..^(β―βπ))) |
87 | 86 | eleq2d 2824 |
. . . . . . 7
β’ ((π β Word π΄ β§ π β Word π΄) β (π₯ β
(0..^(β―β(reverseβπ))) β π₯ β (0..^(β―βπ)))) |
88 | 87 | biimpar 479 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β π₯ β
(0..^(β―β(reverseβπ)))) |
89 | | ccatval1 14472 |
. . . . . 6
β’
(((reverseβπ)
β Word π΄ β§
(reverseβπ) β
Word π΄ β§ π₯ β
(0..^(β―β(reverseβπ)))) β (((reverseβπ) ++ (reverseβπ))βπ₯) = ((reverseβπ)βπ₯)) |
90 | 83, 84, 88, 89 | syl3anc 1372 |
. . . . 5
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β (((reverseβπ) ++ (reverseβπ))βπ₯) = ((reverseβπ)βπ₯)) |
91 | 73, 82, 90 | 3eqtr4d 2787 |
. . . 4
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^(β―βπ))) β ((reverseβ(π ++ π))βπ₯) = (((reverseβπ) ++ (reverseβπ))βπ₯)) |
92 | 8 | nn0zd 12532 |
. . . . . . . . . . . 12
β’ (π β Word π΄ β (β―βπ) β β€) |
93 | | peano2zm 12553 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β€ β ((β―βπ) β 1) β
β€) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . 11
β’ (π β Word π΄ β ((β―βπ) β 1) β
β€) |
95 | 94 | zcnd 12615 |
. . . . . . . . . 10
β’ (π β Word π΄ β ((β―βπ) β 1) β
β) |
96 | 95 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β ((β―βπ) β 1) β
β) |
97 | | elfzoelz 13579 |
. . . . . . . . . . 11
β’ (π₯ β ((β―βπ)..^((β―βπ) + (β―βπ))) β π₯ β β€) |
98 | 97 | zcnd 12615 |
. . . . . . . . . 10
β’ (π₯ β ((β―βπ)..^((β―βπ) + (β―βπ))) β π₯ β β) |
99 | 98 | adantl 483 |
. . . . . . . . 9
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β π₯ β β) |
100 | 11 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (β―βπ) β β) |
101 | 96, 99, 100 | subsub3d 11549 |
. . . . . . . 8
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (((β―βπ) β 1) β (π₯ β (β―βπ))) = ((((β―βπ) β 1) +
(β―βπ)) β
π₯)) |
102 | 26 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π β Word π΄ β (π₯ β (β―β(reverseβπ))) = (π₯ β (β―βπ))) |
103 | 102 | oveq2d 7378 |
. . . . . . . . 9
β’ (π β Word π΄ β (((β―βπ) β 1) β (π₯ β (β―β(reverseβπ)))) = (((β―βπ) β 1) β (π₯ β (β―βπ)))) |
104 | 103 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (((β―βπ) β 1) β (π₯ β
(β―β(reverseβπ)))) = (((β―βπ) β 1) β (π₯ β (β―βπ)))) |
105 | 7 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π β Word π΄ β§ π β Word π΄) β ((β―β(π ++ π)) β 1) = (((β―βπ) + (β―βπ)) β 1)) |
106 | 54, 53, 55 | addsubd 11540 |
. . . . . . . . . . 11
β’ ((π β Word π΄ β§ π β Word π΄) β (((β―βπ) + (β―βπ)) β 1) = (((β―βπ) β 1) +
(β―βπ))) |
107 | 105, 106 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β Word π΄ β§ π β Word π΄) β ((β―β(π ++ π)) β 1) = (((β―βπ) β 1) +
(β―βπ))) |
108 | 107 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π β Word π΄ β§ π β Word π΄) β (((β―β(π ++ π)) β 1) β π₯) = ((((β―βπ) β 1) + (β―βπ)) β π₯)) |
109 | 108 | adantr 482 |
. . . . . . . 8
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (((β―β(π ++ π)) β 1) β π₯) = ((((β―βπ) β 1) + (β―βπ)) β π₯)) |
110 | 101, 104,
109 | 3eqtr4rd 2788 |
. . . . . . 7
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (((β―β(π ++ π)) β 1) β π₯) = (((β―βπ) β 1) β (π₯ β (β―β(reverseβπ))))) |
111 | 110 | fveq2d 6851 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (πβ(((β―β(π ++ π)) β 1) β π₯)) = (πβ(((β―βπ) β 1) β (π₯ β (β―β(reverseβπ)))))) |
112 | | simpll 766 |
. . . . . . 7
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β π β Word π΄) |
113 | | simplr 768 |
. . . . . . 7
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β π β Word π΄) |
114 | | zaddcl 12550 |
. . . . . . . . . . 11
β’
(((β―βπ)
β β€ β§ (β―βπ) β β€) β
((β―βπ) +
(β―βπ)) β
β€) |
115 | 34, 92, 114 | syl2anr 598 |
. . . . . . . . . 10
β’ ((π β Word π΄ β§ π β Word π΄) β ((β―βπ) + (β―βπ)) β β€) |
116 | | peano2zm 12553 |
. . . . . . . . . 10
β’
(((β―βπ)
+ (β―βπ)) β
β€ β (((β―βπ) + (β―βπ)) β 1) β
β€) |
117 | 115, 116 | syl 17 |
. . . . . . . . 9
β’ ((π β Word π΄ β§ π β Word π΄) β (((β―βπ) + (β―βπ)) β 1) β
β€) |
118 | | fzoval 13580 |
. . . . . . . . . . . 12
β’
(((β―βπ)
+ (β―βπ)) β
β€ β ((β―βπ)..^((β―βπ) + (β―βπ))) = ((β―βπ)...(((β―βπ) + (β―βπ)) β 1))) |
119 | 115, 118 | syl 17 |
. . . . . . . . . . 11
β’ ((π β Word π΄ β§ π β Word π΄) β ((β―βπ)..^((β―βπ) + (β―βπ))) = ((β―βπ)...(((β―βπ) + (β―βπ)) β 1))) |
120 | 119 | eleq2d 2824 |
. . . . . . . . . 10
β’ ((π β Word π΄ β§ π β Word π΄) β (π₯ β ((β―βπ)..^((β―βπ) + (β―βπ))) β π₯ β ((β―βπ)...(((β―βπ) + (β―βπ)) β 1)))) |
121 | 120 | biimpa 478 |
. . . . . . . . 9
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β π₯ β ((β―βπ)...(((β―βπ) + (β―βπ)) β 1))) |
122 | | fzrev2i 13513 |
. . . . . . . . 9
β’
(((((β―βπ) + (β―βπ)) β 1) β β€ β§ π₯ β ((β―βπ)...(((β―βπ) + (β―βπ)) β 1))) β
((((β―βπ) +
(β―βπ)) β
1) β π₯) β
(((((β―βπ) +
(β―βπ)) β
1) β (((β―βπ) + (β―βπ)) β 1))...((((β―βπ) + (β―βπ)) β 1) β
(β―βπ)))) |
123 | 117, 121,
122 | syl2an2r 684 |
. . . . . . . 8
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β ((((β―βπ) + (β―βπ)) β 1) β π₯) β
(((((β―βπ) +
(β―βπ)) β
1) β (((β―βπ) + (β―βπ)) β 1))...((((β―βπ) + (β―βπ)) β 1) β
(β―βπ)))) |
124 | 52 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π β Word π΄ β§ π β Word π΄) β (((β―β(π ++ π)) β 1) β π₯) = ((((β―βπ) + (β―βπ)) β 1) β π₯)) |
125 | 124 | adantr 482 |
. . . . . . . 8
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (((β―β(π ++ π)) β 1) β π₯) = ((((β―βπ) + (β―βπ)) β 1) β π₯)) |
126 | 92 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β Word π΄ β§ π β Word π΄) β (β―βπ) β β€) |
127 | | fzoval 13580 |
. . . . . . . . . . 11
β’
((β―βπ)
β β€ β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
128 | 126, 127 | syl 17 |
. . . . . . . . . 10
β’ ((π β Word π΄ β§ π β Word π΄) β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
129 | 117 | zcnd 12615 |
. . . . . . . . . . . 12
β’ ((π β Word π΄ β§ π β Word π΄) β (((β―βπ) + (β―βπ)) β 1) β
β) |
130 | 129 | subidd 11507 |
. . . . . . . . . . 11
β’ ((π β Word π΄ β§ π β Word π΄) β ((((β―βπ) + (β―βπ)) β 1) β (((β―βπ) + (β―βπ)) β 1)) =
0) |
131 | | addcl 11140 |
. . . . . . . . . . . . . 14
β’
(((β―βπ)
β β β§ (β―βπ) β β) β
((β―βπ) +
(β―βπ)) β
β) |
132 | 11, 9, 131 | syl2anr 598 |
. . . . . . . . . . . . 13
β’ ((π β Word π΄ β§ π β Word π΄) β ((β―βπ) + (β―βπ)) β β) |
133 | 132, 55, 53 | sub32d 11551 |
. . . . . . . . . . . 12
β’ ((π β Word π΄ β§ π β Word π΄) β ((((β―βπ) + (β―βπ)) β 1) β (β―βπ)) = ((((β―βπ) + (β―βπ)) β (β―βπ)) β 1)) |
134 | | pncan2 11415 |
. . . . . . . . . . . . . 14
β’
(((β―βπ)
β β β§ (β―βπ) β β) β
(((β―βπ) +
(β―βπ)) β
(β―βπ)) =
(β―βπ)) |
135 | 11, 9, 134 | syl2anr 598 |
. . . . . . . . . . . . 13
β’ ((π β Word π΄ β§ π β Word π΄) β (((β―βπ) + (β―βπ)) β (β―βπ)) = (β―βπ)) |
136 | 135 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ ((π β Word π΄ β§ π β Word π΄) β ((((β―βπ) + (β―βπ)) β (β―βπ)) β 1) = ((β―βπ) β 1)) |
137 | 133, 136 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β Word π΄ β§ π β Word π΄) β ((((β―βπ) + (β―βπ)) β 1) β (β―βπ)) = ((β―βπ) β 1)) |
138 | 130, 137 | oveq12d 7380 |
. . . . . . . . . 10
β’ ((π β Word π΄ β§ π β Word π΄) β (((((β―βπ) + (β―βπ)) β 1) β
(((β―βπ) +
(β―βπ)) β
1))...((((β―βπ)
+ (β―βπ))
β 1) β (β―βπ))) = (0...((β―βπ) β 1))) |
139 | 128, 138 | eqtr4d 2780 |
. . . . . . . . 9
β’ ((π β Word π΄ β§ π β Word π΄) β (0..^(β―βπ)) = (((((β―βπ) + (β―βπ)) β 1) β
(((β―βπ) +
(β―βπ)) β
1))...((((β―βπ)
+ (β―βπ))
β 1) β (β―βπ)))) |
140 | 139 | adantr 482 |
. . . . . . . 8
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (0..^(β―βπ)) = (((((β―βπ) + (β―βπ)) β 1) β
(((β―βπ) +
(β―βπ)) β
1))...((((β―βπ)
+ (β―βπ))
β 1) β (β―βπ)))) |
141 | 123, 125,
140 | 3eltr4d 2853 |
. . . . . . 7
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (((β―β(π ++ π)) β 1) β π₯) β (0..^(β―βπ))) |
142 | | ccatval1 14472 |
. . . . . . 7
β’ ((π β Word π΄ β§ π β Word π΄ β§ (((β―β(π ++ π)) β 1) β π₯) β (0..^(β―βπ))) β ((π ++ π)β(((β―β(π ++ π)) β 1) β π₯)) = (πβ(((β―β(π ++ π)) β 1) β π₯))) |
143 | 112, 113,
141, 142 | syl3anc 1372 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β ((π ++ π)β(((β―β(π ++ π)) β 1) β π₯)) = (πβ(((β―β(π ++ π)) β 1) β π₯))) |
144 | | simpl 484 |
. . . . . . 7
β’ ((π β Word π΄ β§ π β Word π΄) β π β Word π΄) |
145 | 102 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (π₯ β (β―β(reverseβπ))) = (π₯ β (β―βπ))) |
146 | | id 22 |
. . . . . . . . 9
β’ (π₯ β ((β―βπ)..^((β―βπ) + (β―βπ))) β π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) |
147 | | fzosubel3 13640 |
. . . . . . . . 9
β’ ((π₯ β ((β―βπ)..^((β―βπ) + (β―βπ))) β§ (β―βπ) β β€) β (π₯ β (β―βπ)) β
(0..^(β―βπ))) |
148 | 146, 126,
147 | syl2anr 598 |
. . . . . . . 8
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (π₯ β (β―βπ)) β (0..^(β―βπ))) |
149 | 145, 148 | eqeltrd 2838 |
. . . . . . 7
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (π₯ β (β―β(reverseβπ))) β
(0..^(β―βπ))) |
150 | | revfv 14658 |
. . . . . . 7
β’ ((π β Word π΄ β§ (π₯ β (β―β(reverseβπ))) β
(0..^(β―βπ)))
β ((reverseβπ)β(π₯ β (β―β(reverseβπ)))) = (πβ(((β―βπ) β 1) β (π₯ β (β―β(reverseβπ)))))) |
151 | 144, 149,
150 | syl2an2r 684 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β ((reverseβπ)β(π₯ β (β―β(reverseβπ)))) = (πβ(((β―βπ) β 1) β (π₯ β (β―β(reverseβπ)))))) |
152 | 111, 143,
151 | 3eqtr4d 2787 |
. . . . 5
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β ((π ++ π)β(((β―β(π ++ π)) β 1) β π₯)) = ((reverseβπ)β(π₯ β (β―β(reverseβπ))))) |
153 | | fzoss1 13606 |
. . . . . . . . . . 11
β’
((β―βπ)
β (β€β₯β0) β ((β―βπ)..^((β―βπ) + (β―βπ))) β
(0..^((β―βπ) +
(β―βπ)))) |
154 | | nn0uz 12812 |
. . . . . . . . . . 11
β’
β0 = (β€β₯β0) |
155 | 153, 154 | eleq2s 2856 |
. . . . . . . . . 10
β’
((β―βπ)
β β0 β ((β―βπ)..^((β―βπ) + (β―βπ))) β (0..^((β―βπ) + (β―βπ)))) |
156 | 10, 155 | syl 17 |
. . . . . . . . 9
β’ (π β Word π΄ β ((β―βπ)..^((β―βπ) + (β―βπ))) β (0..^((β―βπ) + (β―βπ)))) |
157 | 156 | adantl 483 |
. . . . . . . 8
β’ ((π β Word π΄ β§ π β Word π΄) β ((β―βπ)..^((β―βπ) + (β―βπ))) β (0..^((β―βπ) + (β―βπ)))) |
158 | 51 | oveq2d 7378 |
. . . . . . . 8
β’ ((π β Word π΄ β§ π β Word π΄) β (0..^(β―β(π ++ π))) = (0..^((β―βπ) + (β―βπ)))) |
159 | 157, 158 | sseqtrrd 3990 |
. . . . . . 7
β’ ((π β Word π΄ β§ π β Word π΄) β ((β―βπ)..^((β―βπ) + (β―βπ))) β (0..^(β―β(π ++ π)))) |
160 | 159 | sselda 3949 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β π₯ β (0..^(β―β(π ++ π)))) |
161 | 1, 160, 81 | syl2an2r 684 |
. . . . 5
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β ((reverseβ(π ++ π))βπ₯) = ((π ++ π)β(((β―β(π ++ π)) β 1) β π₯))) |
162 | 18 | ad2antlr 726 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (reverseβπ) β Word π΄) |
163 | 19 | ad2antrr 725 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (reverseβπ) β Word π΄) |
164 | 85, 28 | oveq12d 7380 |
. . . . . . . 8
β’ ((π β Word π΄ β§ π β Word π΄) β
((β―β(reverseβπ))..^((β―β(reverseβπ)) +
(β―β(reverseβπ)))) = ((β―βπ)..^((β―βπ) + (β―βπ)))) |
165 | 164 | eleq2d 2824 |
. . . . . . 7
β’ ((π β Word π΄ β§ π β Word π΄) β (π₯ β ((β―β(reverseβπ))..^((β―β(reverseβπ)) +
(β―β(reverseβπ)))) β π₯ β ((β―βπ)..^((β―βπ) + (β―βπ))))) |
166 | 165 | biimpar 479 |
. . . . . 6
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β π₯ β ((β―β(reverseβπ))..^((β―β(reverseβπ)) +
(β―β(reverseβπ))))) |
167 | | ccatval2 14473 |
. . . . . 6
β’
(((reverseβπ)
β Word π΄ β§
(reverseβπ) β
Word π΄ β§ π₯ β
((β―β(reverseβπ))..^((β―β(reverseβπ)) +
(β―β(reverseβπ))))) β (((reverseβπ) ++ (reverseβπ))βπ₯) = ((reverseβπ)β(π₯ β (β―β(reverseβπ))))) |
168 | 162, 163,
166, 167 | syl3anc 1372 |
. . . . 5
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β (((reverseβπ) ++ (reverseβπ))βπ₯) = ((reverseβπ)β(π₯ β (β―β(reverseβπ))))) |
169 | 152, 161,
168 | 3eqtr4d 2787 |
. . . 4
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ)))) β ((reverseβ(π ++ π))βπ₯) = (((reverseβπ) ++ (reverseβπ))βπ₯)) |
170 | 91, 169 | jaodan 957 |
. . 3
β’ (((π β Word π΄ β§ π β Word π΄) β§ (π₯ β (0..^(β―βπ)) β¨ π₯ β ((β―βπ)..^((β―βπ) + (β―βπ))))) β ((reverseβ(π ++ π))βπ₯) = (((reverseβπ) ++ (reverseβπ))βπ₯)) |
171 | 37, 170 | syldan 592 |
. 2
β’ (((π β Word π΄ β§ π β Word π΄) β§ π₯ β (0..^((β―βπ) + (β―βπ)))) β
((reverseβ(π ++ π))βπ₯) = (((reverseβπ) ++ (reverseβπ))βπ₯)) |
172 | 17, 32, 171 | eqfnfvd 6990 |
1
β’ ((π β Word π΄ β§ π β Word π΄) β (reverseβ(π ++ π)) = ((reverseβπ) ++ (reverseβπ))) |