Step | Hyp | Ref
| Expression |
1 | | cnvimass 6033 |
. . . . . . . 8
β’ (β‘(πΊβπ΄) β β) β dom (πΊβπ΄) |
2 | | eulerpart.p |
. . . . . . . . . . . . . 14
β’ π = {π β (β0
βm β) β£ ((β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π)} |
3 | | eulerpart.o |
. . . . . . . . . . . . . 14
β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} |
4 | | eulerpart.d |
. . . . . . . . . . . . . 14
β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} |
5 | | eulerpart.j |
. . . . . . . . . . . . . 14
β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} |
6 | | eulerpart.f |
. . . . . . . . . . . . . 14
β’ πΉ = (π₯ β π½, π¦ β β0 β¦
((2βπ¦) Β· π₯)) |
7 | | eulerpart.h |
. . . . . . . . . . . . . 14
β’ π» = {π β ((π« β0 β©
Fin) βm π½)
β£ (π supp β
)
β Fin} |
8 | | eulerpart.m |
. . . . . . . . . . . . . 14
β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) |
9 | | eulerpart.r |
. . . . . . . . . . . . . 14
β’ π
= {π β£ (β‘π β β) β
Fin} |
10 | | eulerpart.t |
. . . . . . . . . . . . . 14
β’ π = {π β (β0
βm β) β£ (β‘π β β) β π½} |
11 | | eulerpart.g |
. . . . . . . . . . . . . 14
β’ πΊ = (π β (π β© π
) β¦
((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) |
12 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | eulerpartgbij 32972 |
. . . . . . . . . . . . 13
β’ πΊ:(π β© π
)β1-1-ontoβ(({0,
1} βm β) β© π
) |
13 | | f1of 6784 |
. . . . . . . . . . . . 13
β’ (πΊ:(π β© π
)β1-1-ontoβ(({0,
1} βm β) β© π
) β πΊ:(π β© π
)βΆ(({0, 1} βm
β) β© π
)) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . . 12
β’ πΊ:(π β© π
)βΆ(({0, 1} βm
β) β© π
) |
15 | 14 | ffvelcdmi 7034 |
. . . . . . . . . . 11
β’ (π΄ β (π β© π
) β (πΊβπ΄) β (({0, 1} βm
β) β© π
)) |
16 | | elin 3926 |
. . . . . . . . . . 11
β’ ((πΊβπ΄) β (({0, 1} βm
β) β© π
) β
((πΊβπ΄) β ({0, 1} βm β)
β§ (πΊβπ΄) β π
)) |
17 | 15, 16 | sylib 217 |
. . . . . . . . . 10
β’ (π΄ β (π β© π
) β ((πΊβπ΄) β ({0, 1} βm β)
β§ (πΊβπ΄) β π
)) |
18 | 17 | simpld 495 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β (πΊβπ΄) β ({0, 1} βm
β)) |
19 | | elmapi 8787 |
. . . . . . . . 9
β’ ((πΊβπ΄) β ({0, 1} βm β)
β (πΊβπ΄):ββΆ{0,
1}) |
20 | | fdm 6677 |
. . . . . . . . 9
β’ ((πΊβπ΄):ββΆ{0, 1} β dom (πΊβπ΄) = β) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β dom (πΊβπ΄) = β) |
22 | 1, 21 | sseqtrid 3996 |
. . . . . . 7
β’ (π΄ β (π β© π
) β (β‘(πΊβπ΄) β β) β
β) |
23 | 22 | sselda 3944 |
. . . . . 6
β’ ((π΄ β (π β© π
) β§ π β (β‘(πΊβπ΄) β β)) β π β
β) |
24 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | eulerpartlemgvv 32976 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ π β β) β ((πΊβπ΄)βπ) = if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0)) |
25 | 24 | oveq1d 7372 |
. . . . . 6
β’ ((π΄ β (π β© π
) β§ π β β) β (((πΊβπ΄)βπ) Β· π) = (if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π)) |
26 | 23, 25 | syldan 591 |
. . . . 5
β’ ((π΄ β (π β© π
) β§ π β (β‘(πΊβπ΄) β β)) β (((πΊβπ΄)βπ) Β· π) = (if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π)) |
27 | 26 | sumeq2dv 15588 |
. . . 4
β’ (π΄ β (π β© π
) β Ξ£π β (β‘(πΊβπ΄) β β)(((πΊβπ΄)βπ) Β· π) = Ξ£π β (β‘(πΊβπ΄) β β)(if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π)) |
28 | | eqeq2 2748 |
. . . . . . . . . . . . 13
β’ (π = π β (((2βπ) Β· π‘) = π β ((2βπ) Β· π‘) = π)) |
29 | 28 | 2rexbidv 3213 |
. . . . . . . . . . . 12
β’ (π = π β (βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π β βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π)) |
30 | 29 | elrab 3645 |
. . . . . . . . . . 11
β’ (π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β (π β β β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π)) |
31 | 30 | simprbi 497 |
. . . . . . . . . 10
β’ (π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π) |
32 | 31 | iftrued 4494 |
. . . . . . . . 9
β’ (π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) = 1) |
33 | 32 | oveq1d 7372 |
. . . . . . . 8
β’ (π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β (if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π) = (1 Β· π)) |
34 | | elrabi 3639 |
. . . . . . . . . 10
β’ (π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β π β β) |
35 | 34 | nncnd 12169 |
. . . . . . . . 9
β’ (π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β π β β) |
36 | 35 | mulid2d 11173 |
. . . . . . . 8
β’ (π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β (1 Β· π) = π) |
37 | 33, 36 | eqtrd 2776 |
. . . . . . 7
β’ (π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β (if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π) = π) |
38 | 37 | sumeq2i 15584 |
. . . . . 6
β’
Ξ£π β
{π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} (if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π) = Ξ£π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}π |
39 | | id 22 |
. . . . . . 7
β’ (π = ((2β(2nd
βπ€)) Β·
(1st βπ€))
β π =
((2β(2nd βπ€)) Β· (1st βπ€))) |
40 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | eulerpartlemgf 32979 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β (β‘(πΊβπ΄) β β) β
Fin) |
41 | 34 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β π β β) |
42 | 41, 24 | syldan 591 |
. . . . . . . . . . . . . 14
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β ((πΊβπ΄)βπ) = if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0)) |
43 | 31 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π) |
44 | 43 | iftrued 4494 |
. . . . . . . . . . . . . 14
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) = 1) |
45 | 42, 44 | eqtrd 2776 |
. . . . . . . . . . . . 13
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β ((πΊβπ΄)βπ) = 1) |
46 | | 1nn 12164 |
. . . . . . . . . . . . 13
β’ 1 β
β |
47 | 45, 46 | eqeltrdi 2845 |
. . . . . . . . . . . 12
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β ((πΊβπ΄)βπ) β β) |
48 | 18, 19 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π΄ β (π β© π
) β (πΊβπ΄):ββΆ{0, 1}) |
49 | | ffn 6668 |
. . . . . . . . . . . . . 14
β’ ((πΊβπ΄):ββΆ{0, 1} β (πΊβπ΄) Fn β) |
50 | | elpreima 7008 |
. . . . . . . . . . . . . 14
β’ ((πΊβπ΄) Fn β β (π β (β‘(πΊβπ΄) β β) β (π β β β§ ((πΊβπ΄)βπ) β β))) |
51 | 48, 49, 50 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π΄ β (π β© π
) β (π β (β‘(πΊβπ΄) β β) β (π β β β§ ((πΊβπ΄)βπ) β β))) |
52 | 51 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β (π β (β‘(πΊβπ΄) β β) β (π β β β§ ((πΊβπ΄)βπ) β β))) |
53 | 41, 47, 52 | mpbir2and 711 |
. . . . . . . . . . 11
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β π β (β‘(πΊβπ΄) β β)) |
54 | 53 | ex 413 |
. . . . . . . . . 10
β’ (π΄ β (π β© π
) β (π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β π β (β‘(πΊβπ΄) β β))) |
55 | 54 | ssrdv 3950 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β (β‘(πΊβπ΄) β β)) |
56 | | ssfi 9117 |
. . . . . . . . 9
β’ (((β‘(πΊβπ΄) β β) β Fin β§ {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β (β‘(πΊβπ΄) β β)) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β Fin) |
57 | 40, 55, 56 | syl2anc 584 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β Fin) |
58 | | cnvexg 7861 |
. . . . . . . . . . 11
β’ (π΄ β (π β© π
) β β‘π΄ β V) |
59 | | imaexg 7852 |
. . . . . . . . . . 11
β’ (β‘π΄ β V β (β‘π΄ β β) β V) |
60 | | inex1g 5276 |
. . . . . . . . . . 11
β’ ((β‘π΄ β β) β V β ((β‘π΄ β β) β© π½) β V) |
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . . 10
β’ (π΄ β (π β© π
) β ((β‘π΄ β β) β© π½) β V) |
62 | | vsnex 5386 |
. . . . . . . . . . . 12
β’ {π‘} β V |
63 | | fvex 6855 |
. . . . . . . . . . . 12
β’
(bitsβ(π΄βπ‘)) β V |
64 | 62, 63 | xpex 7687 |
. . . . . . . . . . 11
β’ ({π‘} Γ (bitsβ(π΄βπ‘))) β V |
65 | 64 | rgenw 3068 |
. . . . . . . . . 10
β’
βπ‘ β
((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β V |
66 | | iunexg 7896 |
. . . . . . . . . 10
β’ ((((β‘π΄ β β) β© π½) β V β§ βπ‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β V) β βͺ π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β V) |
67 | 61, 65, 66 | sylancl 586 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β V) |
68 | | eqid 2736 |
. . . . . . . . . 10
β’ βͺ π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) = βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) |
69 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 68 | eulerpartlemgh 32978 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β (πΉ βΎ βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))):βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))β1-1-ontoβ{π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) |
70 | | f1oeng 8911 |
. . . . . . . . 9
β’
((βͺ π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β V β§ (πΉ βΎ βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))):βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))β1-1-ontoβ{π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) |
71 | 67, 69, 70 | syl2anc 584 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) |
72 | | enfii 9133 |
. . . . . . . 8
β’ (({π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β Fin β§ βͺ π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β Fin) |
73 | 57, 71, 72 | syl2anc 584 |
. . . . . . 7
β’ (π΄ β (π β© π
) β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β Fin) |
74 | | fvres 6861 |
. . . . . . . . 9
β’ (π€ β βͺ π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β ((πΉ βΎ βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))))βπ€) = (πΉβπ€)) |
75 | 74 | adantl 482 |
. . . . . . . 8
β’ ((π΄ β (π β© π
) β§ π€ β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))) β ((πΉ βΎ βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))))βπ€) = (πΉβπ€)) |
76 | | inss2 4189 |
. . . . . . . . . . . . . . 15
β’ ((β‘π΄ β β) β© π½) β π½ |
77 | | simpr 485 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β π‘ β ((β‘π΄ β β) β© π½)) |
78 | 76, 77 | sselid 3942 |
. . . . . . . . . . . . . 14
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β π‘ β π½) |
79 | 78 | snssd 4769 |
. . . . . . . . . . . . 13
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β {π‘} β π½) |
80 | | bitsss 16306 |
. . . . . . . . . . . . 13
β’
(bitsβ(π΄βπ‘)) β
β0 |
81 | | xpss12 5648 |
. . . . . . . . . . . . 13
β’ (({π‘} β π½ β§ (bitsβ(π΄βπ‘)) β β0) β
({π‘} Γ
(bitsβ(π΄βπ‘))) β (π½ Γ
β0)) |
82 | 79, 80, 81 | sylancl 586 |
. . . . . . . . . . . 12
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β ({π‘} Γ (bitsβ(π΄βπ‘))) β (π½ Γ
β0)) |
83 | 82 | ralrimiva 3143 |
. . . . . . . . . . 11
β’ (π΄ β (π β© π
) β βπ‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β (π½ Γ
β0)) |
84 | | iunss 5005 |
. . . . . . . . . . 11
β’ (βͺ π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β (π½ Γ β0) β
βπ‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β (π½ Γ
β0)) |
85 | 83, 84 | sylibr 233 |
. . . . . . . . . 10
β’ (π΄ β (π β© π
) β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))) β (π½ Γ
β0)) |
86 | 85 | sselda 3944 |
. . . . . . . . 9
β’ ((π΄ β (π β© π
) β§ π€ β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))) β π€ β (π½ Γ
β0)) |
87 | 5, 6 | oddpwdcv 32955 |
. . . . . . . . 9
β’ (π€ β (π½ Γ β0) β (πΉβπ€) = ((2β(2nd βπ€)) Β· (1st
βπ€))) |
88 | 86, 87 | syl 17 |
. . . . . . . 8
β’ ((π΄ β (π β© π
) β§ π€ β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))) β (πΉβπ€) = ((2β(2nd βπ€)) Β· (1st
βπ€))) |
89 | 75, 88 | eqtrd 2776 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ π€ β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))) β ((πΉ βΎ βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘))))βπ€) = ((2β(2nd βπ€)) Β· (1st
βπ€))) |
90 | 41 | nncnd 12169 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β π β β) |
91 | 39, 73, 69, 89, 90 | fsumf1o 15608 |
. . . . . 6
β’ (π΄ β (π β© π
) β Ξ£π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}π = Ξ£π€ β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))((2β(2nd βπ€)) Β· (1st
βπ€))) |
92 | 38, 91 | eqtrid 2788 |
. . . . 5
β’ (π΄ β (π β© π
) β Ξ£π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} (if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π) = Ξ£π€ β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))((2β(2nd βπ€)) Β· (1st
βπ€))) |
93 | | ax-1cn 11109 |
. . . . . . . . 9
β’ 1 β
β |
94 | | 0cn 11147 |
. . . . . . . . 9
β’ 0 β
β |
95 | 93, 94 | ifcli 4533 |
. . . . . . . 8
β’
if(βπ‘ β
β βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) β β |
96 | 95 | a1i 11 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) β β) |
97 | | ssrab2 4037 |
. . . . . . . . 9
β’ {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β β |
98 | | simpr 485 |
. . . . . . . . 9
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) |
99 | 97, 98 | sselid 3942 |
. . . . . . . 8
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β π β β) |
100 | 99 | nncnd 12169 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β π β β) |
101 | 96, 100 | mulcld 11175 |
. . . . . 6
β’ ((π΄ β (π β© π
) β§ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β (if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π) β β) |
102 | | simpr 485 |
. . . . . . . . . . 11
β’ ((π΄ β (π β© π
) β§ π β ((β‘(πΊβπ΄) β β) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π})) β π β ((β‘(πΊβπ΄) β β) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π})) |
103 | 102 | eldifbd 3923 |
. . . . . . . . . 10
β’ ((π΄ β (π β© π
) β§ π β ((β‘(πΊβπ΄) β β) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π})) β Β¬ π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) |
104 | 22 | ssdifssd 4102 |
. . . . . . . . . . 11
β’ (π΄ β (π β© π
) β ((β‘(πΊβπ΄) β β) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β β) |
105 | 104 | sselda 3944 |
. . . . . . . . . 10
β’ ((π΄ β (π β© π
) β§ π β ((β‘(πΊβπ΄) β β) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π})) β π β β) |
106 | 30 | notbii 319 |
. . . . . . . . . . 11
β’ (Β¬
π β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β Β¬ (π β β β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π)) |
107 | | imnan 400 |
. . . . . . . . . . 11
β’ ((π β β β Β¬
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π) β Β¬ (π β β β§ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π)) |
108 | 106, 107 | sylbb2 237 |
. . . . . . . . . 10
β’ (Β¬
π β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} β (π β β β Β¬ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π)) |
109 | 103, 105,
108 | sylc 65 |
. . . . . . . . 9
β’ ((π΄ β (π β© π
) β§ π β ((β‘(πΊβπ΄) β β) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π})) β Β¬ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π) |
110 | 109 | iffalsed 4497 |
. . . . . . . 8
β’ ((π΄ β (π β© π
) β§ π β ((β‘(πΊβπ΄) β β) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π})) β if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) = 0) |
111 | 110 | oveq1d 7372 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ π β ((β‘(πΊβπ΄) β β) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π})) β (if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π) = (0 Β· π)) |
112 | | nnsscn 12158 |
. . . . . . . . . 10
β’ β
β β |
113 | 104, 112 | sstrdi 3956 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β ((β‘(πΊβπ΄) β β) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π}) β β) |
114 | 113 | sselda 3944 |
. . . . . . . 8
β’ ((π΄ β (π β© π
) β§ π β ((β‘(πΊβπ΄) β β) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π})) β π β β) |
115 | 114 | mul02d 11353 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ π β ((β‘(πΊβπ΄) β β) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π})) β (0 Β· π) = 0) |
116 | 111, 115 | eqtrd 2776 |
. . . . . 6
β’ ((π΄ β (π β© π
) β§ π β ((β‘(πΊβπ΄) β β) β {π β β β£
βπ‘ β β
βπ β
(bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π})) β (if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π) = 0) |
117 | 55, 101, 116, 40 | fsumss 15610 |
. . . . 5
β’ (π΄ β (π β© π
) β Ξ£π β {π β β β£ βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π} (if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π) = Ξ£π β (β‘(πΊβπ΄) β β)(if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π)) |
118 | 92, 117 | eqtr3d 2778 |
. . . 4
β’ (π΄ β (π β© π
) β Ξ£π€ β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))((2β(2nd βπ€)) Β· (1st
βπ€)) = Ξ£π β (β‘(πΊβπ΄) β β)(if(βπ‘ β β βπ β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = π, 1, 0) Β· π)) |
119 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemt0 32969 |
. . . . . . . . . . . . 13
β’ (π΄ β (π β© π
) β (π΄ β (β0
βm β) β§ (β‘π΄ β β) β Fin β§ (β‘π΄ β β) β π½)) |
120 | 119 | simp1bi 1145 |
. . . . . . . . . . . 12
β’ (π΄ β (π β© π
) β π΄ β (β0
βm β)) |
121 | | elmapi 8787 |
. . . . . . . . . . . 12
β’ (π΄ β (β0
βm β) β π΄:ββΆβ0) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . 11
β’ (π΄ β (π β© π
) β π΄:ββΆβ0) |
123 | 122 | adantr 481 |
. . . . . . . . . 10
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β π΄:ββΆβ0) |
124 | | cnvimass 6033 |
. . . . . . . . . . . . 13
β’ (β‘π΄ β β) β dom π΄ |
125 | 124, 122 | fssdm 6688 |
. . . . . . . . . . . 12
β’ (π΄ β (π β© π
) β (β‘π΄ β β) β
β) |
126 | 125 | adantr 481 |
. . . . . . . . . . 11
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β (β‘π΄ β β) β
β) |
127 | | inss1 4188 |
. . . . . . . . . . . 12
β’ ((β‘π΄ β β) β© π½) β (β‘π΄ β β) |
128 | 127, 77 | sselid 3942 |
. . . . . . . . . . 11
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β π‘ β (β‘π΄ β β)) |
129 | 126, 128 | sseldd 3945 |
. . . . . . . . . 10
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β π‘ β β) |
130 | 123, 129 | ffvelcdmd 7036 |
. . . . . . . . 9
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β (π΄βπ‘) β
β0) |
131 | | bitsfi 16317 |
. . . . . . . . 9
β’ ((π΄βπ‘) β β0 β
(bitsβ(π΄βπ‘)) β Fin) |
132 | 130, 131 | syl 17 |
. . . . . . . 8
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β (bitsβ(π΄βπ‘)) β Fin) |
133 | 129 | nncnd 12169 |
. . . . . . . 8
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β π‘ β β) |
134 | | 2cnd 12231 |
. . . . . . . . . 10
β’ ((π΄ β (π β© π
) β§ (π‘ β ((β‘π΄ β β) β© π½) β§ π β (bitsβ(π΄βπ‘)))) β 2 β
β) |
135 | | simprr 771 |
. . . . . . . . . . 11
β’ ((π΄ β (π β© π
) β§ (π‘ β ((β‘π΄ β β) β© π½) β§ π β (bitsβ(π΄βπ‘)))) β π β (bitsβ(π΄βπ‘))) |
136 | 80, 135 | sselid 3942 |
. . . . . . . . . 10
β’ ((π΄ β (π β© π
) β§ (π‘ β ((β‘π΄ β β) β© π½) β§ π β (bitsβ(π΄βπ‘)))) β π β β0) |
137 | 134, 136 | expcld 14051 |
. . . . . . . . 9
β’ ((π΄ β (π β© π
) β§ (π‘ β ((β‘π΄ β β) β© π½) β§ π β (bitsβ(π΄βπ‘)))) β (2βπ) β β) |
138 | 137 | anassrs 468 |
. . . . . . . 8
β’ (((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β§ π β (bitsβ(π΄βπ‘))) β (2βπ) β β) |
139 | 132, 133,
138 | fsummulc1 15670 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β (Ξ£π β (bitsβ(π΄βπ‘))(2βπ) Β· π‘) = Ξ£π β (bitsβ(π΄βπ‘))((2βπ) Β· π‘)) |
140 | 139 | sumeq2dv 15588 |
. . . . . 6
β’ (π΄ β (π β© π
) β Ξ£π‘ β ((β‘π΄ β β) β© π½)(Ξ£π β (bitsβ(π΄βπ‘))(2βπ) Β· π‘) = Ξ£π‘ β ((β‘π΄ β β) β© π½)Ξ£π β (bitsβ(π΄βπ‘))((2βπ) Β· π‘)) |
141 | | bitsinv1 16322 |
. . . . . . . . 9
β’ ((π΄βπ‘) β β0 β
Ξ£π β
(bitsβ(π΄βπ‘))(2βπ) = (π΄βπ‘)) |
142 | 141 | oveq1d 7372 |
. . . . . . . 8
β’ ((π΄βπ‘) β β0 β
(Ξ£π β
(bitsβ(π΄βπ‘))(2βπ) Β· π‘) = ((π΄βπ‘) Β· π‘)) |
143 | 130, 142 | syl 17 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ π‘ β ((β‘π΄ β β) β© π½)) β (Ξ£π β (bitsβ(π΄βπ‘))(2βπ) Β· π‘) = ((π΄βπ‘) Β· π‘)) |
144 | 143 | sumeq2dv 15588 |
. . . . . 6
β’ (π΄ β (π β© π
) β Ξ£π‘ β ((β‘π΄ β β) β© π½)(Ξ£π β (bitsβ(π΄βπ‘))(2βπ) Β· π‘) = Ξ£π‘ β ((β‘π΄ β β) β© π½)((π΄βπ‘) Β· π‘)) |
145 | | vex 3449 |
. . . . . . . . . 10
β’ π‘ β V |
146 | | vex 3449 |
. . . . . . . . . 10
β’ π β V |
147 | 145, 146 | op2ndd 7932 |
. . . . . . . . 9
β’ (π€ = β¨π‘, πβ© β (2nd βπ€) = π) |
148 | 147 | oveq2d 7373 |
. . . . . . . 8
β’ (π€ = β¨π‘, πβ© β (2β(2nd
βπ€)) = (2βπ)) |
149 | 145, 146 | op1std 7931 |
. . . . . . . 8
β’ (π€ = β¨π‘, πβ© β (1st βπ€) = π‘) |
150 | 148, 149 | oveq12d 7375 |
. . . . . . 7
β’ (π€ = β¨π‘, πβ© β ((2β(2nd
βπ€)) Β·
(1st βπ€))
= ((2βπ) Β·
π‘)) |
151 | | inss2 4189 |
. . . . . . . . . 10
β’ (π β© π
) β π
|
152 | 151 | sseli 3940 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β π΄ β π
) |
153 | | cnveq 5829 |
. . . . . . . . . . . 12
β’ (π = π΄ β β‘π = β‘π΄) |
154 | 153 | imaeq1d 6012 |
. . . . . . . . . . 11
β’ (π = π΄ β (β‘π β β) = (β‘π΄ β β)) |
155 | 154 | eleq1d 2822 |
. . . . . . . . . 10
β’ (π = π΄ β ((β‘π β β) β Fin β (β‘π΄ β β) β
Fin)) |
156 | 155, 9 | elab2g 3632 |
. . . . . . . . 9
β’ (π΄ β (π β© π
) β (π΄ β π
β (β‘π΄ β β) β
Fin)) |
157 | 152, 156 | mpbid 231 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β (β‘π΄ β β) β
Fin) |
158 | | ssfi 9117 |
. . . . . . . 8
β’ (((β‘π΄ β β) β Fin β§ ((β‘π΄ β β) β© π½) β (β‘π΄ β β)) β ((β‘π΄ β β) β© π½) β Fin) |
159 | 157, 127,
158 | sylancl 586 |
. . . . . . 7
β’ (π΄ β (π β© π
) β ((β‘π΄ β β) β© π½) β Fin) |
160 | 133 | adantrr 715 |
. . . . . . . 8
β’ ((π΄ β (π β© π
) β§ (π‘ β ((β‘π΄ β β) β© π½) β§ π β (bitsβ(π΄βπ‘)))) β π‘ β β) |
161 | 137, 160 | mulcld 11175 |
. . . . . . 7
β’ ((π΄ β (π β© π
) β§ (π‘ β ((β‘π΄ β β) β© π½) β§ π β (bitsβ(π΄βπ‘)))) β ((2βπ) Β· π‘) β β) |
162 | 150, 159,
132, 161 | fsum2d 15656 |
. . . . . 6
β’ (π΄ β (π β© π
) β Ξ£π‘ β ((β‘π΄ β β) β© π½)Ξ£π β (bitsβ(π΄βπ‘))((2βπ) Β· π‘) = Ξ£π€ β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))((2β(2nd βπ€)) Β· (1st
βπ€))) |
163 | 140, 144,
162 | 3eqtr3d 2784 |
. . . . 5
β’ (π΄ β (π β© π
) β Ξ£π‘ β ((β‘π΄ β β) β© π½)((π΄βπ‘) Β· π‘) = Ξ£π€ β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))((2β(2nd βπ€)) Β· (1st
βπ€))) |
164 | | inss1 4188 |
. . . . . . . . 9
β’ (π β© π
) β π |
165 | 164 | sseli 3940 |
. . . . . . . 8
β’ (π΄ β (π β© π
) β π΄ β π) |
166 | 154 | sseq1d 3975 |
. . . . . . . . . 10
β’ (π = π΄ β ((β‘π β β) β π½ β (β‘π΄ β β) β π½)) |
167 | 166, 10 | elrab2 3648 |
. . . . . . . . 9
β’ (π΄ β π β (π΄ β (β0
βm β) β§ (β‘π΄ β β) β π½)) |
168 | 167 | simprbi 497 |
. . . . . . . 8
β’ (π΄ β π β (β‘π΄ β β) β π½) |
169 | 165, 168 | syl 17 |
. . . . . . 7
β’ (π΄ β (π β© π
) β (β‘π΄ β β) β π½) |
170 | | df-ss 3927 |
. . . . . . 7
β’ ((β‘π΄ β β) β π½ β ((β‘π΄ β β) β© π½) = (β‘π΄ β β)) |
171 | 169, 170 | sylib 217 |
. . . . . 6
β’ (π΄ β (π β© π
) β ((β‘π΄ β β) β© π½) = (β‘π΄ β β)) |
172 | 171 | sumeq1d 15586 |
. . . . 5
β’ (π΄ β (π β© π
) β Ξ£π‘ β ((β‘π΄ β β) β© π½)((π΄βπ‘) Β· π‘) = Ξ£π‘ β (β‘π΄ β β)((π΄βπ‘) Β· π‘)) |
173 | 163, 172 | eqtr3d 2778 |
. . . 4
β’ (π΄ β (π β© π
) β Ξ£π€ β βͺ
π‘ β ((β‘π΄ β β) β© π½)({π‘} Γ (bitsβ(π΄βπ‘)))((2β(2nd βπ€)) Β· (1st
βπ€)) = Ξ£π‘ β (β‘π΄ β β)((π΄βπ‘) Β· π‘)) |
174 | 27, 118, 173 | 3eqtr2d 2782 |
. . 3
β’ (π΄ β (π β© π
) β Ξ£π β (β‘(πΊβπ΄) β β)(((πΊβπ΄)βπ) Β· π) = Ξ£π‘ β (β‘π΄ β β)((π΄βπ‘) Β· π‘)) |
175 | | fveq2 6842 |
. . . . 5
β’ (π = π‘ β (π΄βπ) = (π΄βπ‘)) |
176 | | id 22 |
. . . . 5
β’ (π = π‘ β π = π‘) |
177 | 175, 176 | oveq12d 7375 |
. . . 4
β’ (π = π‘ β ((π΄βπ) Β· π) = ((π΄βπ‘) Β· π‘)) |
178 | 177 | cbvsumv 15581 |
. . 3
β’
Ξ£π β
(β‘π΄ β β)((π΄βπ) Β· π) = Ξ£π‘ β (β‘π΄ β β)((π΄βπ‘) Β· π‘) |
179 | 174, 178 | eqtr4di 2794 |
. 2
β’ (π΄ β (π β© π
) β Ξ£π β (β‘(πΊβπ΄) β β)(((πΊβπ΄)βπ) Β· π) = Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π)) |
180 | | 0nn0 12428 |
. . . . . . . 8
β’ 0 β
β0 |
181 | | 1nn0 12429 |
. . . . . . . 8
β’ 1 β
β0 |
182 | | prssi 4781 |
. . . . . . . 8
β’ ((0
β β0 β§ 1 β β0) β {0, 1}
β β0) |
183 | 180, 181,
182 | mp2an 690 |
. . . . . . 7
β’ {0, 1}
β β0 |
184 | | fss 6685 |
. . . . . . 7
β’ (((πΊβπ΄):ββΆ{0, 1} β§ {0, 1} β
β0) β (πΊβπ΄):ββΆβ0) |
185 | 183, 184 | mpan2 689 |
. . . . . 6
β’ ((πΊβπ΄):ββΆ{0, 1} β (πΊβπ΄):ββΆβ0) |
186 | | nn0ex 12419 |
. . . . . . . 8
β’
β0 β V |
187 | | nnex 12159 |
. . . . . . . 8
β’ β
β V |
188 | 186, 187 | elmap 8809 |
. . . . . . 7
β’ ((πΊβπ΄) β (β0
βm β) β (πΊβπ΄):ββΆβ0) |
189 | 188 | biimpri 227 |
. . . . . 6
β’ ((πΊβπ΄):ββΆβ0 β
(πΊβπ΄) β (β0
βm β)) |
190 | 19, 185, 189 | 3syl 18 |
. . . . 5
β’ ((πΊβπ΄) β ({0, 1} βm β)
β (πΊβπ΄) β (β0
βm β)) |
191 | 190 | anim1i 615 |
. . . 4
β’ (((πΊβπ΄) β ({0, 1} βm β)
β§ (πΊβπ΄) β π
) β ((πΊβπ΄) β (β0
βm β) β§ (πΊβπ΄) β π
)) |
192 | | elin 3926 |
. . . 4
β’ ((πΊβπ΄) β ((β0
βm β) β© π
) β ((πΊβπ΄) β (β0
βm β) β§ (πΊβπ΄) β π
)) |
193 | 191, 16, 192 | 3imtr4i 291 |
. . 3
β’ ((πΊβπ΄) β (({0, 1} βm
β) β© π
) β
(πΊβπ΄) β ((β0
βm β) β© π
)) |
194 | | eulerpart.s |
. . . 4
β’ π = (π β ((β0
βm β) β© π
) β¦ Ξ£π β β ((πβπ) Β· π)) |
195 | 9, 194 | eulerpartlemsv2 32958 |
. . 3
β’ ((πΊβπ΄) β ((β0
βm β) β© π
) β (πβ(πΊβπ΄)) = Ξ£π β (β‘(πΊβπ΄) β β)(((πΊβπ΄)βπ) Β· π)) |
196 | 15, 193, 195 | 3syl 18 |
. 2
β’ (π΄ β (π β© π
) β (πβ(πΊβπ΄)) = Ξ£π β (β‘(πΊβπ΄) β β)(((πΊβπ΄)βπ) Β· π)) |
197 | 120, 152 | elind 4154 |
. . 3
β’ (π΄ β (π β© π
) β π΄ β ((β0
βm β) β© π
)) |
198 | 9, 194 | eulerpartlemsv2 32958 |
. . 3
β’ (π΄ β ((β0
βm β) β© π
) β (πβπ΄) = Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π)) |
199 | 197, 198 | syl 17 |
. 2
β’ (π΄ β (π β© π
) β (πβπ΄) = Ξ£π β (β‘π΄ β β)((π΄βπ) Β· π)) |
200 | 179, 196,
199 | 3eqtr4d 2786 |
1
β’ (π΄ β (π β© π
) β (πβ(πΊβπ΄)) = (πβπ΄)) |