Step | Hyp | Ref
| Expression |
1 | | elmapi 8794 |
. . . . . . . . . 10
β’ (π β (β0
βm π½)
β π:π½βΆβ0) |
2 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β (β0
βm π½) β§
π β π
) β π:π½βΆβ0) |
3 | | c0ex 11156 |
. . . . . . . . . . 11
β’ 0 β
V |
4 | 3 | fconst 6733 |
. . . . . . . . . 10
β’ ((β
β π½) Γ
{0}):(β β π½)βΆ{0} |
5 | 4 | a1i 11 |
. . . . . . . . 9
β’ ((π β (β0
βm π½) β§
π β π
) β ((β β π½) Γ {0}):(β β π½)βΆ{0}) |
6 | | disjdif 4436 |
. . . . . . . . . 10
β’ (π½ β© (β β π½)) = β
|
7 | 6 | a1i 11 |
. . . . . . . . 9
β’ ((π β (β0
βm π½) β§
π β π
) β (π½ β© (β β π½)) = β
) |
8 | | fun 6709 |
. . . . . . . . 9
β’ (((π:π½βΆβ0 β§ ((β
β π½) Γ
{0}):(β β π½)βΆ{0}) β§ (π½ β© (β β π½)) = β
) β (π βͺ ((β β π½) Γ {0})):(π½ βͺ (β β π½))βΆ(β0 βͺ
{0})) |
9 | 2, 5, 7, 8 | syl21anc 837 |
. . . . . . . 8
β’ ((π β (β0
βm π½) β§
π β π
) β (π βͺ ((β β π½) Γ {0})):(π½ βͺ (β β π½))βΆ(β0 βͺ
{0})) |
10 | | eulerpart.j |
. . . . . . . . . . 11
β’ π½ = {π§ β β β£ Β¬ 2 β₯ π§} |
11 | | ssrab2 4042 |
. . . . . . . . . . 11
β’ {π§ β β β£ Β¬ 2
β₯ π§} β
β |
12 | 10, 11 | eqsstri 3983 |
. . . . . . . . . 10
β’ π½ β
β |
13 | | undif 4446 |
. . . . . . . . . 10
β’ (π½ β β β (π½ βͺ (β β π½)) = β) |
14 | 12, 13 | mpbi 229 |
. . . . . . . . 9
β’ (π½ βͺ (β β π½)) = β |
15 | | 0nn0 12435 |
. . . . . . . . . . 11
β’ 0 β
β0 |
16 | | snssi 4773 |
. . . . . . . . . . 11
β’ (0 β
β0 β {0} β β0) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . 10
β’ {0}
β β0 |
18 | | ssequn2 4148 |
. . . . . . . . . 10
β’ ({0}
β β0 β (β0 βͺ {0}) =
β0) |
19 | 17, 18 | mpbi 229 |
. . . . . . . . 9
β’
(β0 βͺ {0}) = β0 |
20 | 14, 19 | feq23i 6667 |
. . . . . . . 8
β’ ((π βͺ ((β β π½) Γ {0})):(π½ βͺ (β β π½))βΆ(β0
βͺ {0}) β (π βͺ
((β β π½)
Γ {0})):ββΆβ0) |
21 | 9, 20 | sylib 217 |
. . . . . . 7
β’ ((π β (β0
βm π½) β§
π β π
) β (π βͺ ((β β π½) Γ
{0})):ββΆβ0) |
22 | | nn0ex 12426 |
. . . . . . . 8
β’
β0 β V |
23 | | nnex 12166 |
. . . . . . . 8
β’ β
β V |
24 | 22, 23 | elmap 8816 |
. . . . . . 7
β’ ((π βͺ ((β β π½) Γ {0})) β
(β0 βm β) β (π βͺ ((β β π½) Γ
{0})):ββΆβ0) |
25 | 21, 24 | sylibr 233 |
. . . . . 6
β’ ((π β (β0
βm π½) β§
π β π
) β (π βͺ ((β β π½) Γ {0})) β (β0
βm β)) |
26 | | cnvun 6100 |
. . . . . . . . 9
β’ β‘(π βͺ ((β β π½) Γ {0})) = (β‘π βͺ β‘((β β π½) Γ {0})) |
27 | 26 | imaeq1i 6015 |
. . . . . . . 8
β’ (β‘(π βͺ ((β β π½) Γ {0})) β β) = ((β‘π βͺ β‘((β β π½) Γ {0})) β
β) |
28 | | imaundir 6108 |
. . . . . . . 8
β’ ((β‘π βͺ β‘((β β π½) Γ {0})) β β) = ((β‘π β β) βͺ (β‘((β β π½) Γ {0}) β
β)) |
29 | 27, 28 | eqtri 2765 |
. . . . . . 7
β’ (β‘(π βͺ ((β β π½) Γ {0})) β β) = ((β‘π β β) βͺ (β‘((β β π½) Γ {0}) β
β)) |
30 | | vex 3452 |
. . . . . . . . . . 11
β’ π β V |
31 | | cnveq 5834 |
. . . . . . . . . . . . 13
β’ (π = π β β‘π = β‘π) |
32 | 31 | imaeq1d 6017 |
. . . . . . . . . . . 12
β’ (π = π β (β‘π β β) = (β‘π β β)) |
33 | 32 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (π = π β ((β‘π β β) β Fin β (β‘π β β) β
Fin)) |
34 | | eulerpart.r |
. . . . . . . . . . 11
β’ π
= {π β£ (β‘π β β) β
Fin} |
35 | 30, 33, 34 | elab2 3639 |
. . . . . . . . . 10
β’ (π β π
β (β‘π β β) β
Fin) |
36 | 35 | biimpi 215 |
. . . . . . . . 9
β’ (π β π
β (β‘π β β) β
Fin) |
37 | 36 | adantl 483 |
. . . . . . . 8
β’ ((π β (β0
βm π½) β§
π β π
) β (β‘π β β) β
Fin) |
38 | | cnvxp 6114 |
. . . . . . . . . . . . . 14
β’ β‘((β β π½) Γ {0}) = ({0} Γ (β
β π½)) |
39 | 38 | dmeqi 5865 |
. . . . . . . . . . . . 13
β’ dom β‘((β β π½) Γ {0}) = dom ({0} Γ (β
β π½)) |
40 | | 2nn 12233 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
41 | | 2z 12542 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β€ |
42 | | iddvds 16159 |
. . . . . . . . . . . . . . . . 17
β’ (2 β
β€ β 2 β₯ 2) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ 2 β₯
2 |
44 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = 2 β (2 β₯ π§ β 2 β₯
2)) |
45 | 44 | notbid 318 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = 2 β (Β¬ 2 β₯
π§ β Β¬ 2 β₯
2)) |
46 | 45, 10 | elrab2 3653 |
. . . . . . . . . . . . . . . . 17
β’ (2 β
π½ β (2 β β
β§ Β¬ 2 β₯ 2)) |
47 | 46 | simprbi 498 |
. . . . . . . . . . . . . . . 16
β’ (2 β
π½ β Β¬ 2 β₯
2) |
48 | 43, 47 | mt2 199 |
. . . . . . . . . . . . . . 15
β’ Β¬ 2
β π½ |
49 | | eldif 3925 |
. . . . . . . . . . . . . . 15
β’ (2 β
(β β π½) β
(2 β β β§ Β¬ 2 β π½)) |
50 | 40, 48, 49 | mpbir2an 710 |
. . . . . . . . . . . . . 14
β’ 2 β
(β β π½) |
51 | | ne0i 4299 |
. . . . . . . . . . . . . 14
β’ (2 β
(β β π½) β
(β β π½) β
β
) |
52 | | dmxp 5889 |
. . . . . . . . . . . . . 14
β’ ((β
β π½) β β
β dom ({0} Γ (β β π½)) = {0}) |
53 | 50, 51, 52 | mp2b 10 |
. . . . . . . . . . . . 13
β’ dom ({0}
Γ (β β π½)) = {0} |
54 | 39, 53 | eqtri 2765 |
. . . . . . . . . . . 12
β’ dom β‘((β β π½) Γ {0}) = {0} |
55 | 54 | ineq1i 4173 |
. . . . . . . . . . 11
β’ (dom
β‘((β β π½) Γ {0}) β© β) = ({0} β©
β) |
56 | | incom 4166 |
. . . . . . . . . . 11
β’ (β
β© {0}) = ({0} β© β) |
57 | | 0nnn 12196 |
. . . . . . . . . . . 12
β’ Β¬ 0
β β |
58 | | disjsn 4677 |
. . . . . . . . . . . 12
β’ ((β
β© {0}) = β
β Β¬ 0 β β) |
59 | 57, 58 | mpbir 230 |
. . . . . . . . . . 11
β’ (β
β© {0}) = β
|
60 | 55, 56, 59 | 3eqtr2i 2771 |
. . . . . . . . . 10
β’ (dom
β‘((β β π½) Γ {0}) β© β) =
β
|
61 | | imadisj 6037 |
. . . . . . . . . 10
β’ ((β‘((β β π½) Γ {0}) β β) = β
β (dom β‘((β β π½) Γ {0}) β© β) =
β
) |
62 | 60, 61 | mpbir 230 |
. . . . . . . . 9
β’ (β‘((β β π½) Γ {0}) β β) =
β
|
63 | | 0fin 9122 |
. . . . . . . . 9
β’ β
β Fin |
64 | 62, 63 | eqeltri 2834 |
. . . . . . . 8
β’ (β‘((β β π½) Γ {0}) β β) β
Fin |
65 | | unfi 9123 |
. . . . . . . 8
β’ (((β‘π β β) β Fin β§ (β‘((β β π½) Γ {0}) β β) β Fin)
β ((β‘π β β) βͺ (β‘((β β π½) Γ {0}) β β)) β
Fin) |
66 | 37, 64, 65 | sylancl 587 |
. . . . . . 7
β’ ((π β (β0
βm π½) β§
π β π
) β ((β‘π β β) βͺ (β‘((β β π½) Γ {0}) β β)) β
Fin) |
67 | 29, 66 | eqeltrid 2842 |
. . . . . 6
β’ ((π β (β0
βm π½) β§
π β π
) β (β‘(π βͺ ((β β π½) Γ {0})) β β) β
Fin) |
68 | | cnvimass 6038 |
. . . . . . . . 9
β’ (β‘π β β) β dom π |
69 | 68, 2 | fssdm 6693 |
. . . . . . . 8
β’ ((π β (β0
βm π½) β§
π β π
) β (β‘π β β) β π½) |
70 | | 0ss 4361 |
. . . . . . . . . 10
β’ β
β π½ |
71 | 62, 70 | eqsstri 3983 |
. . . . . . . . 9
β’ (β‘((β β π½) Γ {0}) β β) β
π½ |
72 | 71 | a1i 11 |
. . . . . . . 8
β’ ((π β (β0
βm π½) β§
π β π
) β (β‘((β β π½) Γ {0}) β β) β
π½) |
73 | 69, 72 | unssd 4151 |
. . . . . . 7
β’ ((π β (β0
βm π½) β§
π β π
) β ((β‘π β β) βͺ (β‘((β β π½) Γ {0}) β β)) β
π½) |
74 | 29, 73 | eqsstrid 3997 |
. . . . . 6
β’ ((π β (β0
βm π½) β§
π β π
) β (β‘(π βͺ ((β β π½) Γ {0})) β β) β
π½) |
75 | | eulerpart.p |
. . . . . . 7
β’ π = {π β (β0
βm β) β£ ((β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π)} |
76 | | eulerpart.o |
. . . . . . 7
β’ π = {π β π β£ βπ β (β‘π β β) Β¬ 2 β₯ π} |
77 | | eulerpart.d |
. . . . . . 7
β’ π· = {π β π β£ βπ β β (πβπ) β€ 1} |
78 | | eulerpart.f |
. . . . . . 7
β’ πΉ = (π₯ β π½, π¦ β β0 β¦
((2βπ¦) Β· π₯)) |
79 | | eulerpart.h |
. . . . . . 7
β’ π» = {π β ((π« β0 β©
Fin) βm π½)
β£ (π supp β
)
β Fin} |
80 | | eulerpart.m |
. . . . . . 7
β’ π = (π β π» β¦ {β¨π₯, π¦β© β£ (π₯ β π½ β§ π¦ β (πβπ₯))}) |
81 | | eulerpart.t |
. . . . . . 7
β’ π = {π β (β0
βm β) β£ (β‘π β β) β π½} |
82 | 75, 76, 77, 10, 78, 79, 80, 34, 81 | eulerpartlemt0 33009 |
. . . . . 6
β’ ((π βͺ ((β β π½) Γ {0})) β (π β© π
) β ((π βͺ ((β β π½) Γ {0})) β (β0
βm β) β§ (β‘(π βͺ ((β β π½) Γ {0})) β β) β Fin
β§ (β‘(π βͺ ((β β π½) Γ {0})) β β) β
π½)) |
83 | 25, 67, 74, 82 | syl3anbrc 1344 |
. . . . 5
β’ ((π β (β0
βm π½) β§
π β π
) β (π βͺ ((β β π½) Γ {0})) β (π β© π
)) |
84 | | resundir 5957 |
. . . . . 6
β’ ((π βͺ ((β β π½) Γ {0})) βΎ π½) = ((π βΎ π½) βͺ (((β β π½) Γ {0}) βΎ π½)) |
85 | | ffn 6673 |
. . . . . . . 8
β’ (π:π½βΆβ0 β π Fn π½) |
86 | | fnresdm 6625 |
. . . . . . . . 9
β’ (π Fn π½ β (π βΎ π½) = π) |
87 | | disjdifr 4437 |
. . . . . . . . . . 11
β’ ((β
β π½) β© π½) = β
|
88 | | fnconstg 6735 |
. . . . . . . . . . . 12
β’ (0 β
β0 β ((β β π½) Γ {0}) Fn (β β π½)) |
89 | | fnresdisj 6626 |
. . . . . . . . . . . 12
β’
(((β β π½) Γ {0}) Fn (β β π½) β (((β β
π½) β© π½) = β
β (((β β π½) Γ {0}) βΎ π½) = β
)) |
90 | 15, 88, 89 | mp2b 10 |
. . . . . . . . . . 11
β’
(((β β π½) β© π½) = β
β (((β β π½) Γ {0}) βΎ π½) = β
) |
91 | 87, 90 | mpbi 229 |
. . . . . . . . . 10
β’
(((β β π½) Γ {0}) βΎ π½) = β
|
92 | 91 | a1i 11 |
. . . . . . . . 9
β’ (π Fn π½ β (((β β π½) Γ {0}) βΎ π½) = β
) |
93 | 86, 92 | uneq12d 4129 |
. . . . . . . 8
β’ (π Fn π½ β ((π βΎ π½) βͺ (((β β π½) Γ {0}) βΎ π½)) = (π βͺ β
)) |
94 | 2, 85, 93 | 3syl 18 |
. . . . . . 7
β’ ((π β (β0
βm π½) β§
π β π
) β ((π βΎ π½) βͺ (((β β π½) Γ {0}) βΎ π½)) = (π βͺ β
)) |
95 | | un0 4355 |
. . . . . . 7
β’ (π βͺ β
) = π |
96 | 94, 95 | eqtrdi 2793 |
. . . . . 6
β’ ((π β (β0
βm π½) β§
π β π
) β ((π βΎ π½) βͺ (((β β π½) Γ {0}) βΎ π½)) = π) |
97 | 84, 96 | eqtr2id 2790 |
. . . . 5
β’ ((π β (β0
βm π½) β§
π β π
) β π = ((π βͺ ((β β π½) Γ {0})) βΎ π½)) |
98 | | reseq1 5936 |
. . . . . 6
β’ (π = (π βͺ ((β β π½) Γ {0})) β (π βΎ π½) = ((π βͺ ((β β π½) Γ {0})) βΎ π½)) |
99 | 98 | rspceeqv 3600 |
. . . . 5
β’ (((π βͺ ((β β π½) Γ {0})) β (π β© π
) β§ π = ((π βͺ ((β β π½) Γ {0})) βΎ π½)) β βπ β (π β© π
)π = (π βΎ π½)) |
100 | 83, 97, 99 | syl2anc 585 |
. . . 4
β’ ((π β (β0
βm π½) β§
π β π
) β βπ β (π β© π
)π = (π βΎ π½)) |
101 | | simpr 486 |
. . . . . . 7
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β π = (π βΎ π½)) |
102 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β π β (π β© π
)) |
103 | 75, 76, 77, 10, 78, 79, 80, 34, 81 | eulerpartlemt0 33009 |
. . . . . . . . . . . 12
β’ (π β (π β© π
) β (π β (β0
βm β) β§ (β‘π β β) β Fin β§ (β‘π β β) β π½)) |
104 | 102, 103 | sylib 217 |
. . . . . . . . . . 11
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β (π β (β0
βm β) β§ (β‘π β β) β Fin β§ (β‘π β β) β π½)) |
105 | 104 | simp1d 1143 |
. . . . . . . . . 10
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β π β (β0
βm β)) |
106 | 22, 23 | elmap 8816 |
. . . . . . . . . 10
β’ (π β (β0
βm β) β π:ββΆβ0) |
107 | 105, 106 | sylib 217 |
. . . . . . . . 9
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β π:ββΆβ0) |
108 | | fssres 6713 |
. . . . . . . . 9
β’ ((π:ββΆβ0 β§
π½ β β) β
(π βΎ π½):π½βΆβ0) |
109 | 107, 12, 108 | sylancl 587 |
. . . . . . . 8
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β (π βΎ π½):π½βΆβ0) |
110 | 10, 23 | rabex2 5296 |
. . . . . . . . 9
β’ π½ β V |
111 | 22, 110 | elmap 8816 |
. . . . . . . 8
β’ ((π βΎ π½) β (β0
βm π½)
β (π βΎ π½):π½βΆβ0) |
112 | 109, 111 | sylibr 233 |
. . . . . . 7
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β (π βΎ π½) β (β0
βm π½)) |
113 | 101, 112 | eqeltrd 2838 |
. . . . . 6
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β π β (β0
βm π½)) |
114 | | ffun 6676 |
. . . . . . . . . 10
β’ (π:ββΆβ0 β
Fun π) |
115 | | respreima 7021 |
. . . . . . . . . 10
β’ (Fun
π β (β‘(π βΎ π½) β β) = ((β‘π β β) β© π½)) |
116 | 107, 114,
115 | 3syl 18 |
. . . . . . . . 9
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β (β‘(π βΎ π½) β β) = ((β‘π β β) β© π½)) |
117 | 104 | simp2d 1144 |
. . . . . . . . . 10
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β (β‘π β β) β
Fin) |
118 | | infi 9219 |
. . . . . . . . . 10
β’ ((β‘π β β) β Fin β ((β‘π β β) β© π½) β Fin) |
119 | 117, 118 | syl 17 |
. . . . . . . . 9
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β ((β‘π β β) β© π½) β Fin) |
120 | 116, 119 | eqeltrd 2838 |
. . . . . . . 8
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β (β‘(π βΎ π½) β β) β
Fin) |
121 | | vex 3452 |
. . . . . . . . . 10
β’ π β V |
122 | 121 | resex 5990 |
. . . . . . . . 9
β’ (π βΎ π½) β V |
123 | | cnveq 5834 |
. . . . . . . . . . 11
β’ (π = (π βΎ π½) β β‘π = β‘(π βΎ π½)) |
124 | 123 | imaeq1d 6017 |
. . . . . . . . . 10
β’ (π = (π βΎ π½) β (β‘π β β) = (β‘(π βΎ π½) β β)) |
125 | 124 | eleq1d 2823 |
. . . . . . . . 9
β’ (π = (π βΎ π½) β ((β‘π β β) β Fin β (β‘(π βΎ π½) β β) β
Fin)) |
126 | 122, 125,
34 | elab2 3639 |
. . . . . . . 8
β’ ((π βΎ π½) β π
β (β‘(π βΎ π½) β β) β
Fin) |
127 | 120, 126 | sylibr 233 |
. . . . . . 7
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β (π βΎ π½) β π
) |
128 | 101, 127 | eqeltrd 2838 |
. . . . . 6
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β π β π
) |
129 | 113, 128 | jca 513 |
. . . . 5
β’ ((π β (π β© π
) β§ π = (π βΎ π½)) β (π β (β0
βm π½) β§
π β π
)) |
130 | 129 | rexlimiva 3145 |
. . . 4
β’
(βπ β
(π β© π
)π = (π βΎ π½) β (π β (β0
βm π½) β§
π β π
)) |
131 | 100, 130 | impbii 208 |
. . 3
β’ ((π β (β0
βm π½) β§
π β π
) β βπ β (π β© π
)π = (π βΎ π½)) |
132 | 131 | abbii 2807 |
. 2
β’ {π β£ (π β (β0
βm π½) β§
π β π
)} = {π β£ βπ β (π β© π
)π = (π βΎ π½)} |
133 | | df-in 3922 |
. 2
β’
((β0 βm π½) β© π
) = {π β£ (π β (β0
βm π½) β§
π β π
)} |
134 | | eqid 2737 |
. . 3
β’ (π β (π β© π
) β¦ (π βΎ π½)) = (π β (π β© π
) β¦ (π βΎ π½)) |
135 | 134 | rnmpt 5915 |
. 2
β’ ran
(π β (π β© π
) β¦ (π βΎ π½)) = {π β£ βπ β (π β© π
)π = (π βΎ π½)} |
136 | 132, 133,
135 | 3eqtr4i 2775 |
1
β’
((β0 βm π½) β© π
) = ran (π β (π β© π
) β¦ (π βΎ π½)) |