Step | Hyp | Ref
| Expression |
1 | | cycpmco2.c |
. . . 4
β’ π = (toCycβπ·) |
2 | | cycpmco2.d |
. . . 4
β’ (π β π· β π) |
3 | | cycpmco2.1 |
. . . . 5
β’ π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) |
4 | | ssrab2 4038 |
. . . . . . 7
β’ {π€ β Word π· β£ π€:dom π€β1-1βπ·} β Word π· |
5 | | cycpmco2.w |
. . . . . . . 8
β’ (π β π β dom π) |
6 | | cycpmco2.s |
. . . . . . . . . . 11
β’ π = (SymGrpβπ·) |
7 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
8 | 1, 6, 7 | tocycf 32015 |
. . . . . . . . . 10
β’ (π· β π β π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆ(Baseβπ)) |
9 | 2, 8 | syl 17 |
. . . . . . . . 9
β’ (π β π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆ(Baseβπ)) |
10 | 9 | fdmd 6680 |
. . . . . . . 8
β’ (π β dom π = {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
11 | 5, 10 | eleqtrd 2836 |
. . . . . . 7
β’ (π β π β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
12 | 4, 11 | sselid 3943 |
. . . . . 6
β’ (π β π β Word π·) |
13 | | cycpmco2.i |
. . . . . . . 8
β’ (π β πΌ β (π· β ran π)) |
14 | 13 | eldifad 3923 |
. . . . . . 7
β’ (π β πΌ β π·) |
15 | 14 | s1cld 14497 |
. . . . . 6
β’ (π β β¨βπΌββ© β Word π·) |
16 | | splcl 14646 |
. . . . . 6
β’ ((π β Word π· β§ β¨βπΌββ© β Word π·) β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β Word π·) |
17 | 12, 15, 16 | syl2anc 585 |
. . . . 5
β’ (π β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) β Word π·) |
18 | 3, 17 | eqeltrid 2838 |
. . . 4
β’ (π β π β Word π·) |
19 | | cycpmco2.j |
. . . . 5
β’ (π β π½ β ran π) |
20 | | cycpmco2.e |
. . . . 5
β’ πΈ = ((β‘πβπ½) + 1) |
21 | 1, 6, 2, 5, 13, 19, 20, 3 | cycpmco2f1 32022 |
. . . 4
β’ (π β π:dom πβ1-1βπ·) |
22 | | fz0ssnn0 13542 |
. . . . . . . 8
β’
(0...(β―βπ)) β
β0 |
23 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π β π€ = π) |
24 | | dmeq 5860 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π β dom π€ = dom π) |
25 | | eqidd 2734 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π β π· = π·) |
26 | 23, 24, 25 | f1eq123d 6777 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π β (π€:dom π€β1-1βπ· β π:dom πβ1-1βπ·)) |
27 | 26 | elrab 3646 |
. . . . . . . . . . . . . . 15
β’ (π β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β (π β Word π· β§ π:dom πβ1-1βπ·)) |
28 | 11, 27 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π β (π β Word π· β§ π:dom πβ1-1βπ·)) |
29 | 28 | simprd 497 |
. . . . . . . . . . . . 13
β’ (π β π:dom πβ1-1βπ·) |
30 | | f1cnv 6809 |
. . . . . . . . . . . . 13
β’ (π:dom πβ1-1βπ· β β‘π:ran πβ1-1-ontoβdom
π) |
31 | | f1of 6785 |
. . . . . . . . . . . . 13
β’ (β‘π:ran πβ1-1-ontoβdom
π β β‘π:ran πβΆdom π) |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β β‘π:ran πβΆdom π) |
33 | 32, 19 | ffvelcdmd 7037 |
. . . . . . . . . . 11
β’ (π β (β‘πβπ½) β dom π) |
34 | | wrddm 14415 |
. . . . . . . . . . . 12
β’ (π β Word π· β dom π = (0..^(β―βπ))) |
35 | 12, 34 | syl 17 |
. . . . . . . . . . 11
β’ (π β dom π = (0..^(β―βπ))) |
36 | 33, 35 | eleqtrd 2836 |
. . . . . . . . . 10
β’ (π β (β‘πβπ½) β (0..^(β―βπ))) |
37 | | fzofzp1 13675 |
. . . . . . . . . 10
β’ ((β‘πβπ½) β (0..^(β―βπ)) β ((β‘πβπ½) + 1) β (0...(β―βπ))) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
β’ (π β ((β‘πβπ½) + 1) β (0...(β―βπ))) |
39 | 20, 38 | eqeltrid 2838 |
. . . . . . . 8
β’ (π β πΈ β (0...(β―βπ))) |
40 | 22, 39 | sselid 3943 |
. . . . . . 7
β’ (π β πΈ β
β0) |
41 | | nn0uz 12810 |
. . . . . . 7
β’
β0 = (β€β₯β0) |
42 | 40, 41 | eleqtrdi 2844 |
. . . . . 6
β’ (π β πΈ β
(β€β₯β0)) |
43 | | fzoss1 13605 |
. . . . . 6
β’ (πΈ β
(β€β₯β0) β (πΈ..^((β―βπ) β 1)) β
(0..^((β―βπ)
β 1))) |
44 | 42, 43 | syl 17 |
. . . . 5
β’ (π β (πΈ..^((β―βπ) β 1)) β
(0..^((β―βπ)
β 1))) |
45 | | cycpmco2lem6.1 |
. . . . 5
β’ (π β (β‘πβπΎ) β (πΈ..^((β―βπ) β 1))) |
46 | 44, 45 | sseldd 3946 |
. . . 4
β’ (π β (β‘πβπΎ) β (0..^((β―βπ) β 1))) |
47 | 1, 2, 18, 21, 46 | cycpmfv1 32011 |
. . 3
β’ (π β ((πβπ)β(πβ(β‘πβπΎ))) = (πβ((β‘πβπΎ) + 1))) |
48 | | cycpmco2lem.1 |
. . . . 5
β’ (π β πΎ β ran π) |
49 | | f1f1orn 6796 |
. . . . . . 7
β’ (π:dom πβ1-1βπ· β π:dom πβ1-1-ontoβran
π) |
50 | 21, 49 | syl 17 |
. . . . . 6
β’ (π β π:dom πβ1-1-ontoβran
π) |
51 | | ssun1 4133 |
. . . . . . . 8
β’ ran π β (ran π βͺ {πΌ}) |
52 | 1, 6, 2, 5, 13, 19, 20, 3 | cycpmco2rn 32023 |
. . . . . . . 8
β’ (π β ran π = (ran π βͺ {πΌ})) |
53 | 51, 52 | sseqtrrid 3998 |
. . . . . . 7
β’ (π β ran π β ran π) |
54 | 53 | sselda 3945 |
. . . . . 6
β’ ((π β§ πΎ β ran π) β πΎ β ran π) |
55 | | f1ocnvfv2 7224 |
. . . . . 6
β’ ((π:dom πβ1-1-ontoβran
π β§ πΎ β ran π) β (πβ(β‘πβπΎ)) = πΎ) |
56 | 50, 54, 55 | syl2an2r 684 |
. . . . 5
β’ ((π β§ πΎ β ran π) β (πβ(β‘πβπΎ)) = πΎ) |
57 | 48, 56 | mpdan 686 |
. . . 4
β’ (π β (πβ(β‘πβπΎ)) = πΎ) |
58 | 57 | fveq2d 6847 |
. . 3
β’ (π β ((πβπ)β(πβ(β‘πβπΎ))) = ((πβπ)βπΎ)) |
59 | 3 | a1i 11 |
. . . 4
β’ (π β π = (π splice β¨πΈ, πΈ, β¨βπΌββ©β©)) |
60 | | fzossz 13598 |
. . . . . . . 8
β’ (πΈ..^((β―βπ) β 1)) β
β€ |
61 | 60, 45 | sselid 3943 |
. . . . . . 7
β’ (π β (β‘πβπΎ) β β€) |
62 | 61 | zcnd 12613 |
. . . . . 6
β’ (π β (β‘πβπΎ) β β) |
63 | 40 | nn0cnd 12480 |
. . . . . 6
β’ (π β πΈ β β) |
64 | | 1cnd 11155 |
. . . . . 6
β’ (π β 1 β
β) |
65 | 62, 63, 64 | nppcan3d 11544 |
. . . . 5
β’ (π β (((β‘πβπΎ) β πΈ) + (1 + πΈ)) = ((β‘πβπΎ) + 1)) |
66 | 65 | eqcomd 2739 |
. . . 4
β’ (π β ((β‘πβπΎ) + 1) = (((β‘πβπΎ) β πΈ) + (1 + πΈ))) |
67 | 59, 66 | fveq12d 6850 |
. . 3
β’ (π β (πβ((β‘πβπΎ) + 1)) = ((π splice β¨πΈ, πΈ, β¨βπΌββ©β©)β(((β‘πβπΎ) β πΈ) + (1 + πΈ)))) |
68 | 47, 58, 67 | 3eqtr3d 2781 |
. 2
β’ (π β ((πβπ)βπΎ) = ((π splice β¨πΈ, πΈ, β¨βπΌββ©β©)β(((β‘πβπΎ) β πΈ) + (1 + πΈ)))) |
69 | 62, 63 | npcand 11521 |
. . . 4
β’ (π β (((β‘πβπΎ) β πΈ) + πΈ) = (β‘πβπΎ)) |
70 | 69 | fveq2d 6847 |
. . 3
β’ (π β (πβ(((β‘πβπΎ) β πΈ) + πΈ)) = (πβ(β‘πβπΎ))) |
71 | | nn0fz0 13545 |
. . . . 5
β’ (πΈ β β0
β πΈ β (0...πΈ)) |
72 | 40, 71 | sylib 217 |
. . . 4
β’ (π β πΈ β (0...πΈ)) |
73 | | lencl 14427 |
. . . . . . . . . . 11
β’ (π β Word π· β (β―βπ) β
β0) |
74 | 12, 73 | syl 17 |
. . . . . . . . . 10
β’ (π β (β―βπ) β
β0) |
75 | 74 | nn0cnd 12480 |
. . . . . . . . 9
β’ (π β (β―βπ) β
β) |
76 | | ovexd 7393 |
. . . . . . . . . . . . . . . 16
β’ (π β ((β‘πβπ½) + 1) β V) |
77 | 20, 76 | eqeltrid 2838 |
. . . . . . . . . . . . . . 15
β’ (π β πΈ β V) |
78 | | splval 14645 |
. . . . . . . . . . . . . . 15
β’ ((π β dom π β§ (πΈ β V β§ πΈ β V β§ β¨βπΌββ© β Word π·)) β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
79 | 5, 77, 77, 15, 78 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ (π β (π splice β¨πΈ, πΈ, β¨βπΌββ©β©) = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
80 | 3, 79 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ (π β π = (((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) |
81 | 80 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π β (β―βπ) = (β―β(((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©)))) |
82 | | pfxcl 14571 |
. . . . . . . . . . . . . . 15
β’ (π β Word π· β (π prefix πΈ) β Word π·) |
83 | 12, 82 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π prefix πΈ) β Word π·) |
84 | | ccatcl 14468 |
. . . . . . . . . . . . . 14
β’ (((π prefix πΈ) β Word π· β§ β¨βπΌββ© β Word π·) β ((π prefix πΈ) ++ β¨βπΌββ©) β Word π·) |
85 | 83, 15, 84 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β ((π prefix πΈ) ++ β¨βπΌββ©) β Word π·) |
86 | | swrdcl 14539 |
. . . . . . . . . . . . . 14
β’ (π β Word π· β (π substr β¨πΈ, (β―βπ)β©) β Word π·) |
87 | 12, 86 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (π substr β¨πΈ, (β―βπ)β©) β Word π·) |
88 | | ccatlen 14469 |
. . . . . . . . . . . . 13
β’ ((((π prefix πΈ) ++ β¨βπΌββ©) β Word π· β§ (π substr β¨πΈ, (β―βπ)β©) β Word π·) β (β―β(((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) = ((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©)))) |
89 | 85, 87, 88 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (β―β(((π prefix πΈ) ++ β¨βπΌββ©) ++ (π substr β¨πΈ, (β―βπ)β©))) = ((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©)))) |
90 | | ccatws1len 14514 |
. . . . . . . . . . . . . . 15
β’ ((π prefix πΈ) β Word π· β (β―β((π prefix πΈ) ++ β¨βπΌββ©)) = ((β―β(π prefix πΈ)) + 1)) |
91 | 12, 82, 90 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β (β―β((π prefix πΈ) ++ β¨βπΌββ©)) = ((β―β(π prefix πΈ)) + 1)) |
92 | | pfxlen 14577 |
. . . . . . . . . . . . . . . 16
β’ ((π β Word π· β§ πΈ β (0...(β―βπ))) β (β―β(π prefix πΈ)) = πΈ) |
93 | 12, 39, 92 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (β―β(π prefix πΈ)) = πΈ) |
94 | 93 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ (π β ((β―β(π prefix πΈ)) + 1) = (πΈ + 1)) |
95 | 91, 94 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π β (β―β((π prefix πΈ) ++ β¨βπΌββ©)) = (πΈ + 1)) |
96 | | nn0fz0 13545 |
. . . . . . . . . . . . . . 15
β’
((β―βπ)
β β0 β (β―βπ) β (0...(β―βπ))) |
97 | 74, 96 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π β (β―βπ) β
(0...(β―βπ))) |
98 | | swrdlen 14541 |
. . . . . . . . . . . . . 14
β’ ((π β Word π· β§ πΈ β (0...(β―βπ)) β§ (β―βπ) β
(0...(β―βπ)))
β (β―β(π
substr β¨πΈ,
(β―βπ)β©)) =
((β―βπ) β
πΈ)) |
99 | 12, 39, 97, 98 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (π β (β―β(π substr β¨πΈ, (β―βπ)β©)) = ((β―βπ) β πΈ)) |
100 | 95, 99 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π β ((β―β((π prefix πΈ) ++ β¨βπΌββ©)) + (β―β(π substr β¨πΈ, (β―βπ)β©))) = ((πΈ + 1) + ((β―βπ) β πΈ))) |
101 | 81, 89, 100 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ (π β (β―βπ) = ((πΈ + 1) + ((β―βπ) β πΈ))) |
102 | 40 | nn0zd 12530 |
. . . . . . . . . . . . . 14
β’ (π β πΈ β β€) |
103 | 102 | peano2zd 12615 |
. . . . . . . . . . . . 13
β’ (π β (πΈ + 1) β β€) |
104 | 103 | zcnd 12613 |
. . . . . . . . . . . 12
β’ (π β (πΈ + 1) β β) |
105 | 104, 75, 63 | addsubassd 11537 |
. . . . . . . . . . 11
β’ (π β (((πΈ + 1) + (β―βπ)) β πΈ) = ((πΈ + 1) + ((β―βπ) β πΈ))) |
106 | 63, 64, 75 | addassd 11182 |
. . . . . . . . . . . 12
β’ (π β ((πΈ + 1) + (β―βπ)) = (πΈ + (1 + (β―βπ)))) |
107 | 106 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π β (((πΈ + 1) + (β―βπ)) β πΈ) = ((πΈ + (1 + (β―βπ))) β πΈ)) |
108 | 101, 105,
107 | 3eqtr2d 2779 |
. . . . . . . . . 10
β’ (π β (β―βπ) = ((πΈ + (1 + (β―βπ))) β πΈ)) |
109 | 64, 75 | addcld 11179 |
. . . . . . . . . . 11
β’ (π β (1 + (β―βπ)) β
β) |
110 | 63, 109 | pncan2d 11519 |
. . . . . . . . . 10
β’ (π β ((πΈ + (1 + (β―βπ))) β πΈ) = (1 + (β―βπ))) |
111 | 64, 75 | addcomd 11362 |
. . . . . . . . . 10
β’ (π β (1 + (β―βπ)) = ((β―βπ) + 1)) |
112 | 108, 110,
111 | 3eqtrd 2777 |
. . . . . . . . 9
β’ (π β (β―βπ) = ((β―βπ) + 1)) |
113 | 75, 64, 112 | mvrraddd 11572 |
. . . . . . . 8
β’ (π β ((β―βπ) β 1) =
(β―βπ)) |
114 | 113 | oveq2d 7374 |
. . . . . . 7
β’ (π β (πΈ..^((β―βπ) β 1)) = (πΈ..^(β―βπ))) |
115 | 45, 114 | eleqtrd 2836 |
. . . . . 6
β’ (π β (β‘πβπΎ) β (πΈ..^(β―βπ))) |
116 | | fzosubel 13637 |
. . . . . 6
β’ (((β‘πβπΎ) β (πΈ..^(β―βπ)) β§ πΈ β β€) β ((β‘πβπΎ) β πΈ) β ((πΈ β πΈ)..^((β―βπ) β πΈ))) |
117 | 115, 102,
116 | syl2anc 585 |
. . . . 5
β’ (π β ((β‘πβπΎ) β πΈ) β ((πΈ β πΈ)..^((β―βπ) β πΈ))) |
118 | 63 | subidd 11505 |
. . . . . 6
β’ (π β (πΈ β πΈ) = 0) |
119 | 118 | oveq1d 7373 |
. . . . 5
β’ (π β ((πΈ β πΈ)..^((β―βπ) β πΈ)) = (0..^((β―βπ) β πΈ))) |
120 | 117, 119 | eleqtrd 2836 |
. . . 4
β’ (π β ((β‘πβπΎ) β πΈ) β (0..^((β―βπ) β πΈ))) |
121 | 64, 63 | addcomd 11362 |
. . . . 5
β’ (π β (1 + πΈ) = (πΈ + 1)) |
122 | | s1len 14500 |
. . . . . 6
β’
(β―ββ¨βπΌββ©) = 1 |
123 | 122 | oveq2i 7369 |
. . . . 5
β’ (πΈ +
(β―ββ¨βπΌββ©)) = (πΈ + 1) |
124 | 121, 123 | eqtr4di 2791 |
. . . 4
β’ (π β (1 + πΈ) = (πΈ + (β―ββ¨βπΌββ©))) |
125 | 12, 72, 39, 15, 120, 124 | splfv3 31861 |
. . 3
β’ (π β ((π splice β¨πΈ, πΈ, β¨βπΌββ©β©)β(((β‘πβπΎ) β πΈ) + (1 + πΈ))) = (πβ(((β‘πβπΎ) β πΈ) + πΈ))) |
126 | 113 | oveq1d 7373 |
. . . . . . . 8
β’ (π β (((β―βπ) β 1) β 1) =
((β―βπ) β
1)) |
127 | 126 | oveq2d 7374 |
. . . . . . 7
β’ (π β (πΈ..^(((β―βπ) β 1) β 1)) = (πΈ..^((β―βπ) β 1))) |
128 | | fzoss1 13605 |
. . . . . . . 8
β’ (πΈ β
(β€β₯β0) β (πΈ..^((β―βπ) β 1)) β
(0..^((β―βπ)
β 1))) |
129 | 42, 128 | syl 17 |
. . . . . . 7
β’ (π β (πΈ..^((β―βπ) β 1)) β
(0..^((β―βπ)
β 1))) |
130 | 127, 129 | eqsstrd 3983 |
. . . . . 6
β’ (π β (πΈ..^(((β―βπ) β 1) β 1)) β
(0..^((β―βπ)
β 1))) |
131 | | f1ocnvdm 7232 |
. . . . . . . . . 10
β’ ((π:dom πβ1-1-ontoβran
π β§ πΎ β ran π) β (β‘πβπΎ) β dom π) |
132 | 50, 54, 131 | syl2an2r 684 |
. . . . . . . . 9
β’ ((π β§ πΎ β ran π) β (β‘πβπΎ) β dom π) |
133 | 48, 132 | mpdan 686 |
. . . . . . . 8
β’ (π β (β‘πβπΎ) β dom π) |
134 | 74 | nn0zd 12530 |
. . . . . . . . . . . . . 14
β’ (π β (β―βπ) β
β€) |
135 | 134 | peano2zd 12615 |
. . . . . . . . . . . . 13
β’ (π β ((β―βπ) + 1) β
β€) |
136 | | elfzonn0 13623 |
. . . . . . . . . . . . . . . . 17
β’ ((β‘πβπ½) β (0..^(β―βπ)) β (β‘πβπ½) β
β0) |
137 | | nn0p1nn 12457 |
. . . . . . . . . . . . . . . . 17
β’ ((β‘πβπ½) β β0 β ((β‘πβπ½) + 1) β β) |
138 | 36, 136, 137 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β ((β‘πβπ½) + 1) β β) |
139 | 20, 138 | eqeltrid 2838 |
. . . . . . . . . . . . . . 15
β’ (π β πΈ β β) |
140 | 139 | nnred 12173 |
. . . . . . . . . . . . . 14
β’ (π β πΈ β β) |
141 | 134 | zred 12612 |
. . . . . . . . . . . . . 14
β’ (π β (β―βπ) β
β) |
142 | | 1red 11161 |
. . . . . . . . . . . . . 14
β’ (π β 1 β
β) |
143 | | elfzle2 13451 |
. . . . . . . . . . . . . . 15
β’ (πΈ β
(0...(β―βπ))
β πΈ β€
(β―βπ)) |
144 | 39, 143 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β πΈ β€ (β―βπ)) |
145 | 140, 141,
142, 144 | leadd1dd 11774 |
. . . . . . . . . . . . 13
β’ (π β (πΈ + 1) β€ ((β―βπ) + 1)) |
146 | | eluz2 12774 |
. . . . . . . . . . . . 13
β’
(((β―βπ)
+ 1) β (β€β₯β(πΈ + 1)) β ((πΈ + 1) β β€ β§
((β―βπ) + 1)
β β€ β§ (πΈ +
1) β€ ((β―βπ)
+ 1))) |
147 | 103, 135,
145, 146 | syl3anbrc 1344 |
. . . . . . . . . . . 12
β’ (π β ((β―βπ) + 1) β
(β€β₯β(πΈ + 1))) |
148 | | fzoss2 13606 |
. . . . . . . . . . . 12
β’
(((β―βπ)
+ 1) β (β€β₯β(πΈ + 1)) β (0..^(πΈ + 1)) β (0..^((β―βπ) + 1))) |
149 | 147, 148 | syl 17 |
. . . . . . . . . . 11
β’ (π β (0..^(πΈ + 1)) β (0..^((β―βπ) + 1))) |
150 | | fzonn0p1 13655 |
. . . . . . . . . . . 12
β’ (πΈ β β0
β πΈ β (0..^(πΈ + 1))) |
151 | 40, 150 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΈ β (0..^(πΈ + 1))) |
152 | 149, 151 | sseldd 3946 |
. . . . . . . . . 10
β’ (π β πΈ β (0..^((β―βπ) + 1))) |
153 | 112 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π β (0..^(β―βπ)) = (0..^((β―βπ) + 1))) |
154 | 152, 153 | eleqtrrd 2837 |
. . . . . . . . 9
β’ (π β πΈ β (0..^(β―βπ))) |
155 | | wrddm 14415 |
. . . . . . . . . 10
β’ (π β Word π· β dom π = (0..^(β―βπ))) |
156 | 18, 155 | syl 17 |
. . . . . . . . 9
β’ (π β dom π = (0..^(β―βπ))) |
157 | 154, 156 | eleqtrrd 2837 |
. . . . . . . 8
β’ (π β πΈ β dom π) |
158 | | cycpmco2lem6.2 |
. . . . . . . . 9
β’ (π β πΎ β πΌ) |
159 | 1, 6, 2, 5, 13, 19, 20, 3 | cycpmco2lem2 32025 |
. . . . . . . . 9
β’ (π β (πβπΈ) = πΌ) |
160 | 158, 57, 159 | 3netr4d 3018 |
. . . . . . . 8
β’ (π β (πβ(β‘πβπΎ)) β (πβπΈ)) |
161 | | f1fveq 7210 |
. . . . . . . . . 10
β’ ((π:dom πβ1-1βπ· β§ ((β‘πβπΎ) β dom π β§ πΈ β dom π)) β ((πβ(β‘πβπΎ)) = (πβπΈ) β (β‘πβπΎ) = πΈ)) |
162 | 161 | necon3bid 2985 |
. . . . . . . . 9
β’ ((π:dom πβ1-1βπ· β§ ((β‘πβπΎ) β dom π β§ πΈ β dom π)) β ((πβ(β‘πβπΎ)) β (πβπΈ) β (β‘πβπΎ) β πΈ)) |
163 | 162 | biimp3a 1470 |
. . . . . . . 8
β’ ((π:dom πβ1-1βπ· β§ ((β‘πβπΎ) β dom π β§ πΈ β dom π) β§ (πβ(β‘πβπΎ)) β (πβπΈ)) β (β‘πβπΎ) β πΈ) |
164 | 21, 133, 157, 160, 163 | syl121anc 1376 |
. . . . . . 7
β’ (π β (β‘πβπΎ) β πΈ) |
165 | | fzom1ne1 31751 |
. . . . . . 7
β’ (((β‘πβπΎ) β (πΈ..^((β―βπ) β 1)) β§ (β‘πβπΎ) β πΈ) β ((β‘πβπΎ) β 1) β (πΈ..^(((β―βπ) β 1) β 1))) |
166 | 45, 164, 165 | syl2anc 585 |
. . . . . 6
β’ (π β ((β‘πβπΎ) β 1) β (πΈ..^(((β―βπ) β 1) β 1))) |
167 | 130, 166 | sseldd 3946 |
. . . . 5
β’ (π β ((β‘πβπΎ) β 1) β
(0..^((β―βπ)
β 1))) |
168 | 1, 2, 12, 29, 167 | cycpmfv1 32011 |
. . . 4
β’ (π β ((πβπ)β(πβ((β‘πβπΎ) β 1))) = (πβ(((β‘πβπΎ) β 1) + 1))) |
169 | 62, 64, 63 | subsub4d 11548 |
. . . . . . . . . 10
β’ (π β (((β‘πβπΎ) β 1) β πΈ) = ((β‘πβπΎ) β (1 + πΈ))) |
170 | 169 | oveq1d 7373 |
. . . . . . . . 9
β’ (π β ((((β‘πβπΎ) β 1) β πΈ) + (1 + πΈ)) = (((β‘πβπΎ) β (1 + πΈ)) + (1 + πΈ))) |
171 | 64, 63 | addcld 11179 |
. . . . . . . . . 10
β’ (π β (1 + πΈ) β β) |
172 | 62, 171 | npcand 11521 |
. . . . . . . . 9
β’ (π β (((β‘πβπΎ) β (1 + πΈ)) + (1 + πΈ)) = (β‘πβπΎ)) |
173 | 170, 172 | eqtr2d 2774 |
. . . . . . . 8
β’ (π β (β‘πβπΎ) = ((((β‘πβπΎ) β 1) β πΈ) + (1 + πΈ))) |
174 | 59, 173 | fveq12d 6850 |
. . . . . . 7
β’ (π β (πβ(β‘πβπΎ)) = ((π splice β¨πΈ, πΈ, β¨βπΌββ©β©)β((((β‘πβπΎ) β 1) β πΈ) + (1 + πΈ)))) |
175 | 63, 75 | pncan3d 11520 |
. . . . . . . . . . . 12
β’ (π β (πΈ + ((β―βπ) β πΈ)) = (β―βπ)) |
176 | 113, 134 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ (π β ((β―βπ) β 1) β
β€) |
177 | | 1zzd 12539 |
. . . . . . . . . . . . . 14
β’ (π β 1 β
β€) |
178 | 176, 177 | zsubcld 12617 |
. . . . . . . . . . . . 13
β’ (π β (((β―βπ) β 1) β 1) β
β€) |
179 | 178 | zred 12612 |
. . . . . . . . . . . . . 14
β’ (π β (((β―βπ) β 1) β 1) β
β) |
180 | 113, 141 | eqeltrd 2834 |
. . . . . . . . . . . . . . . 16
β’ (π β ((β―βπ) β 1) β
β) |
181 | 180 | ltm1d 12092 |
. . . . . . . . . . . . . . 15
β’ (π β (((β―βπ) β 1) β 1) <
((β―βπ) β
1)) |
182 | 181, 113 | breqtrd 5132 |
. . . . . . . . . . . . . 14
β’ (π β (((β―βπ) β 1) β 1) <
(β―βπ)) |
183 | 179, 141,
182 | ltled 11308 |
. . . . . . . . . . . . 13
β’ (π β (((β―βπ) β 1) β 1) β€
(β―βπ)) |
184 | | eluz1 12772 |
. . . . . . . . . . . . . 14
β’
((((β―βπ)
β 1) β 1) β β€ β ((β―βπ) β
(β€β₯β(((β―βπ) β 1) β 1)) β
((β―βπ) β
β€ β§ (((β―βπ) β 1) β 1) β€
(β―βπ)))) |
185 | 184 | biimpar 479 |
. . . . . . . . . . . . 13
β’
(((((β―βπ) β 1) β 1) β β€ β§
((β―βπ) β
β€ β§ (((β―βπ) β 1) β 1) β€
(β―βπ))) β
(β―βπ) β
(β€β₯β(((β―βπ) β 1) β 1))) |
186 | 178, 134,
183, 185 | syl12anc 836 |
. . . . . . . . . . . 12
β’ (π β (β―βπ) β
(β€β₯β(((β―βπ) β 1) β 1))) |
187 | 175, 186 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (π β (πΈ + ((β―βπ) β πΈ)) β
(β€β₯β(((β―βπ) β 1) β 1))) |
188 | | fzoss2 13606 |
. . . . . . . . . . 11
β’ ((πΈ + ((β―βπ) β πΈ)) β
(β€β₯β(((β―βπ) β 1) β 1)) β (πΈ..^(((β―βπ) β 1) β 1)) β
(πΈ..^(πΈ + ((β―βπ) β πΈ)))) |
189 | 187, 188 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΈ..^(((β―βπ) β 1) β 1)) β (πΈ..^(πΈ + ((β―βπ) β πΈ)))) |
190 | 189, 166 | sseldd 3946 |
. . . . . . . . 9
β’ (π β ((β‘πβπΎ) β 1) β (πΈ..^(πΈ + ((β―βπ) β πΈ)))) |
191 | 134, 102 | zsubcld 12617 |
. . . . . . . . 9
β’ (π β ((β―βπ) β πΈ) β β€) |
192 | | fzosubel3 13639 |
. . . . . . . . 9
β’ ((((β‘πβπΎ) β 1) β (πΈ..^(πΈ + ((β―βπ) β πΈ))) β§ ((β―βπ) β πΈ) β β€) β (((β‘πβπΎ) β 1) β πΈ) β (0..^((β―βπ) β πΈ))) |
193 | 190, 191,
192 | syl2anc 585 |
. . . . . . . 8
β’ (π β (((β‘πβπΎ) β 1) β πΈ) β (0..^((β―βπ) β πΈ))) |
194 | 12, 72, 39, 15, 193, 124 | splfv3 31861 |
. . . . . . 7
β’ (π β ((π splice β¨πΈ, πΈ, β¨βπΌββ©β©)β((((β‘πβπΎ) β 1) β πΈ) + (1 + πΈ))) = (πβ((((β‘πβπΎ) β 1) β πΈ) + πΈ))) |
195 | 62, 64 | subcld 11517 |
. . . . . . . . 9
β’ (π β ((β‘πβπΎ) β 1) β
β) |
196 | 195, 63 | npcand 11521 |
. . . . . . . 8
β’ (π β ((((β‘πβπΎ) β 1) β πΈ) + πΈ) = ((β‘πβπΎ) β 1)) |
197 | 196 | fveq2d 6847 |
. . . . . . 7
β’ (π β (πβ((((β‘πβπΎ) β 1) β πΈ) + πΈ)) = (πβ((β‘πβπΎ) β 1))) |
198 | 174, 194,
197 | 3eqtrd 2777 |
. . . . . 6
β’ (π β (πβ(β‘πβπΎ)) = (πβ((β‘πβπΎ) β 1))) |
199 | 198, 57 | eqtr3d 2775 |
. . . . 5
β’ (π β (πβ((β‘πβπΎ) β 1)) = πΎ) |
200 | 199 | fveq2d 6847 |
. . . 4
β’ (π β ((πβπ)β(πβ((β‘πβπΎ) β 1))) = ((πβπ)βπΎ)) |
201 | 62, 64 | npcand 11521 |
. . . . 5
β’ (π β (((β‘πβπΎ) β 1) + 1) = (β‘πβπΎ)) |
202 | 201 | fveq2d 6847 |
. . . 4
β’ (π β (πβ(((β‘πβπΎ) β 1) + 1)) = (πβ(β‘πβπΎ))) |
203 | 168, 200,
202 | 3eqtr3d 2781 |
. . 3
β’ (π β ((πβπ)βπΎ) = (πβ(β‘πβπΎ))) |
204 | 70, 125, 203 | 3eqtr4rd 2784 |
. 2
β’ (π β ((πβπ)βπΎ) = ((π splice β¨πΈ, πΈ, β¨βπΌββ©β©)β(((β‘πβπΎ) β πΈ) + (1 + πΈ)))) |
205 | 68, 204 | eqtr4d 2776 |
1
β’ (π β ((πβπ)βπΎ) = ((πβπ)βπΎ)) |