Step | Hyp | Ref
| Expression |
1 | | eulerpart.p |
. . . . . . 7
β’ π = {π β (β0
βm β) β£ ((β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π)} |
2 | | eulerpart.o |
. . . . . . 7
β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} |
3 | | eulerpart.d |
. . . . . . 7
β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} |
4 | | eulerpart.j |
. . . . . . 7
β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} |
5 | | eulerpart.f |
. . . . . . 7
β’ πΉ = (π₯ β π½, π¦ β β0 β¦
((2βπ¦) Β· π₯)) |
6 | | eulerpart.h |
. . . . . . 7
β’ π» = {π β ((π« β0 β©
Fin) βm π½)
β£ (π supp β
)
β Fin} |
7 | | eulerpart.m |
. . . . . . 7
β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) |
8 | | eulerpart.r |
. . . . . . 7
β’ π
= {π β£ (β‘π β β) β
Fin} |
9 | | eulerpart.t |
. . . . . . 7
β’ π = {π β (β0
βm β) β£ (β‘π β β) β π½} |
10 | | eulerpart.g |
. . . . . . 7
β’ πΊ = (π β (π β© π
) β¦
((πββ)β(πΉ β (πβ(bits β (π βΎ π½)))))) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemgv 33013 |
. . . . . 6
β’ (π΄ β (π β© π
) β (πΊβπ΄) = ((πββ)β(πΉ β (πβ(bits β (π΄ βΎ π½)))))) |
12 | 11 | cnveqd 5836 |
. . . . 5
β’ (π΄ β (π β© π
) β β‘(πΊβπ΄) = β‘((πββ)β(πΉ β (πβ(bits β (π΄ βΎ π½)))))) |
13 | 12 | imaeq1d 6017 |
. . . 4
β’ (π΄ β (π β© π
) β (β‘(πΊβπ΄) β {1}) = (β‘((πββ)β(πΉ β (πβ(bits β (π΄ βΎ π½))))) β {1})) |
14 | | nnex 12166 |
. . . . 5
β’ β
β V |
15 | | imassrn 6029 |
. . . . . 6
β’ (πΉ β (πβ(bits β (π΄ βΎ π½)))) β ran πΉ |
16 | 4, 5 | oddpwdc 32994 |
. . . . . . 7
β’ πΉ:(π½ Γ β0)β1-1-ontoββ |
17 | | f1of 6789 |
. . . . . . 7
β’ (πΉ:(π½ Γ β0)β1-1-ontoββ β πΉ:(π½ Γ
β0)βΆβ) |
18 | | frn 6680 |
. . . . . . 7
β’ (πΉ:(π½ Γ β0)βΆβ
β ran πΉ β
β) |
19 | 16, 17, 18 | mp2b 10 |
. . . . . 6
β’ ran πΉ β
β |
20 | 15, 19 | sstri 3958 |
. . . . 5
β’ (πΉ β (πβ(bits β (π΄ βΎ π½)))) β β |
21 | | indpi1 32659 |
. . . . 5
β’ ((β
β V β§ (πΉ β
(πβ(bits β
(π΄ βΎ π½)))) β β) β
(β‘((πββ)β(πΉ β (πβ(bits β (π΄ βΎ π½))))) β {1}) = (πΉ β (πβ(bits β (π΄ βΎ π½))))) |
22 | 14, 20, 21 | mp2an 691 |
. . . 4
β’ (β‘((πββ)β(πΉ β (πβ(bits β (π΄ βΎ π½))))) β {1}) = (πΉ β (πβ(bits β (π΄ βΎ π½)))) |
23 | 13, 22 | eqtrdi 2793 |
. . 3
β’ (π΄ β (π β© π
) β (β‘(πΊβπ΄) β {1}) = (πΉ β (πβ(bits β (π΄ βΎ π½))))) |
24 | | ffun 6676 |
. . . . 5
β’ (πΉ:(π½ Γ β0)βΆβ
β Fun πΉ) |
25 | 16, 17, 24 | mp2b 10 |
. . . 4
β’ Fun πΉ |
26 | | inss2 4194 |
. . . . 5
β’
(π« (π½
Γ β0) β© Fin) β Fin |
27 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartlemmf 33015 |
. . . . . 6
β’ (π΄ β (π β© π
) β (bits β (π΄ βΎ π½)) β π») |
28 | 1, 2, 3, 4, 5, 6, 7 | eulerpartlem1 33007 |
. . . . . . . 8
β’ π:π»β1-1-ontoβ(π« (π½ Γ β0) β©
Fin) |
29 | | f1of 6789 |
. . . . . . . 8
β’ (π:π»β1-1-ontoβ(π« (π½ Γ β0) β© Fin)
β π:π»βΆ(π« (π½ Γ β0) β©
Fin)) |
30 | 28, 29 | ax-mp 5 |
. . . . . . 7
β’ π:π»βΆ(π« (π½ Γ β0) β©
Fin) |
31 | 30 | ffvelcdmi 7039 |
. . . . . 6
β’ ((bits
β (π΄ βΎ π½)) β π» β (πβ(bits β (π΄ βΎ π½))) β (π« (π½ Γ β0) β©
Fin)) |
32 | 27, 31 | syl 17 |
. . . . 5
β’ (π΄ β (π β© π
) β (πβ(bits β (π΄ βΎ π½))) β (π« (π½ Γ β0) β©
Fin)) |
33 | 26, 32 | sselid 3947 |
. . . 4
β’ (π΄ β (π β© π
) β (πβ(bits β (π΄ βΎ π½))) β Fin) |
34 | | imafi 9126 |
. . . 4
β’ ((Fun
πΉ β§ (πβ(bits β (π΄ βΎ π½))) β Fin) β (πΉ β (πβ(bits β (π΄ βΎ π½)))) β Fin) |
35 | 25, 33, 34 | sylancr 588 |
. . 3
β’ (π΄ β (π β© π
) β (πΉ β (πβ(bits β (π΄ βΎ π½)))) β Fin) |
36 | 23, 35 | eqeltrd 2838 |
. 2
β’ (π΄ β (π β© π
) β (β‘(πΊβπ΄) β {1}) β Fin) |
37 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | eulerpartgbij 33012 |
. . . . . . . 8
β’ πΊ:(π β© π
)β1-1-ontoβ(({0,
1} βm β) β© π
) |
38 | | f1of 6789 |
. . . . . . . 8
β’ (πΊ:(π β© π
)β1-1-ontoβ(({0,
1} βm β) β© π
) β πΊ:(π β© π
)βΆ(({0, 1} βm
β) β© π
)) |
39 | 37, 38 | ax-mp 5 |
. . . . . . 7
β’ πΊ:(π β© π
)βΆ(({0, 1} βm
β) β© π
) |
40 | 39 | ffvelcdmi 7039 |
. . . . . 6
β’ (π΄ β (π β© π
) β (πΊβπ΄) β (({0, 1} βm
β) β© π
)) |
41 | | elin 3931 |
. . . . . . 7
β’ ((πΊβπ΄) β (({0, 1} βm
β) β© π
) β
((πΊβπ΄) β ({0, 1} βm β)
β§ (πΊβπ΄) β π
)) |
42 | 41 | simplbi 499 |
. . . . . 6
β’ ((πΊβπ΄) β (({0, 1} βm
β) β© π
) β
(πΊβπ΄) β ({0, 1} βm
β)) |
43 | | elmapi 8794 |
. . . . . 6
β’ ((πΊβπ΄) β ({0, 1} βm β)
β (πΊβπ΄):ββΆ{0,
1}) |
44 | 40, 42, 43 | 3syl 18 |
. . . . 5
β’ (π΄ β (π β© π
) β (πΊβπ΄):ββΆ{0, 1}) |
45 | 44 | ffund 6677 |
. . . 4
β’ (π΄ β (π β© π
) β Fun (πΊβπ΄)) |
46 | | ssv 3973 |
. . . . 5
β’
β0 β V |
47 | | dfn2 12433 |
. . . . . 6
β’ β =
(β0 β {0}) |
48 | | ssdif 4104 |
. . . . . 6
β’
(β0 β V β (β0 β {0})
β (V β {0})) |
49 | 47, 48 | eqsstrid 3997 |
. . . . 5
β’
(β0 β V β β β (V β
{0})) |
50 | 46, 49 | ax-mp 5 |
. . . 4
β’ β
β (V β {0}) |
51 | | sspreima 7023 |
. . . 4
β’ ((Fun
(πΊβπ΄) β§ β β (V β {0}))
β (β‘(πΊβπ΄) β β) β (β‘(πΊβπ΄) β (V β {0}))) |
52 | 45, 50, 51 | sylancl 587 |
. . 3
β’ (π΄ β (π β© π
) β (β‘(πΊβπ΄) β β) β (β‘(πΊβπ΄) β (V β {0}))) |
53 | | fvex 6860 |
. . . . 5
β’ (πΊβπ΄) β V |
54 | | 0nn0 12435 |
. . . . 5
β’ 0 β
β0 |
55 | | suppimacnv 8110 |
. . . . 5
β’ (((πΊβπ΄) β V β§ 0 β
β0) β ((πΊβπ΄) supp 0) = (β‘(πΊβπ΄) β (V β {0}))) |
56 | 53, 54, 55 | mp2an 691 |
. . . 4
β’ ((πΊβπ΄) supp 0) = (β‘(πΊβπ΄) β (V β {0})) |
57 | | 0ne1 12231 |
. . . . . . . . 9
β’ 0 β
1 |
58 | | difprsn1 4765 |
. . . . . . . . 9
β’ (0 β 1
β ({0, 1} β {0}) = {1}) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . 8
β’ ({0, 1}
β {0}) = {1} |
60 | 59 | eqcomi 2746 |
. . . . . . 7
β’ {1} =
({0, 1} β {0}) |
61 | 60 | ffs2 31687 |
. . . . . 6
β’ ((β
β V β§ 0 β β0 β§ (πΊβπ΄):ββΆ{0, 1}) β ((πΊβπ΄) supp 0) = (β‘(πΊβπ΄) β {1})) |
62 | 14, 54, 61 | mp3an12 1452 |
. . . . 5
β’ ((πΊβπ΄):ββΆ{0, 1} β ((πΊβπ΄) supp 0) = (β‘(πΊβπ΄) β {1})) |
63 | 44, 62 | syl 17 |
. . . 4
β’ (π΄ β (π β© π
) β ((πΊβπ΄) supp 0) = (β‘(πΊβπ΄) β {1})) |
64 | 56, 63 | eqtr3id 2791 |
. . 3
β’ (π΄ β (π β© π
) β (β‘(πΊβπ΄) β (V β {0})) = (β‘(πΊβπ΄) β {1})) |
65 | 52, 64 | sseqtrd 3989 |
. 2
β’ (π΄ β (π β© π
) β (β‘(πΊβπ΄) β β) β (β‘(πΊβπ΄) β {1})) |
66 | | ssfi 9124 |
. 2
β’ (((β‘(πΊβπ΄) β {1}) β Fin β§ (β‘(πΊβπ΄) β β) β (β‘(πΊβπ΄) β {1})) β (β‘(πΊβπ΄) β β) β
Fin) |
67 | 36, 65, 66 | syl2anc 585 |
1
β’ (π΄ β (π β© π
) β (β‘(πΊβπ΄) β β) β
Fin) |