Step |
Hyp |
Ref |
Expression |
1 |
|
eulerpart.p |
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) } |
2 |
|
eulerpart.o |
|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n } |
3 |
|
eulerpart.d |
|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 } |
4 |
|
eulerpart.j |
|- J = { z e. NN | -. 2 || z } |
5 |
|
eulerpart.f |
|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) |
6 |
|
eulerpart.h |
|- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin } |
7 |
|
eulerpart.m |
|- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } ) |
8 |
|
eulerpart.r |
|- R = { f | ( `' f " NN ) e. Fin } |
9 |
|
eulerpart.t |
|- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J } |
10 |
|
eulerpart.g |
|- G = ( o e. ( T i^i R ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) |
11 |
|
eulerpart.s |
|- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) ) |
12 |
|
simpl |
|- ( ( o = q /\ k e. NN ) -> o = q ) |
13 |
12
|
fveq1d |
|- ( ( o = q /\ k e. NN ) -> ( o ` k ) = ( q ` k ) ) |
14 |
13
|
oveq1d |
|- ( ( o = q /\ k e. NN ) -> ( ( o ` k ) x. k ) = ( ( q ` k ) x. k ) ) |
15 |
14
|
sumeq2dv |
|- ( o = q -> sum_ k e. NN ( ( o ` k ) x. k ) = sum_ k e. NN ( ( q ` k ) x. k ) ) |
16 |
15
|
eqeq1d |
|- ( o = q -> ( sum_ k e. NN ( ( o ` k ) x. k ) = N <-> sum_ k e. NN ( ( q ` k ) x. k ) = N ) ) |
17 |
16
|
cbvrabv |
|- { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } = { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } |
18 |
17
|
a1i |
|- ( o = q -> { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } = { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) |
19 |
18
|
reseq2d |
|- ( o = q -> ( G |` { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } ) = ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) ) |
20 |
|
eqidd |
|- ( o = q -> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } = { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) |
21 |
19 18 20
|
f1oeq123d |
|- ( o = q -> ( ( G |` { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } ) : { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } <-> ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) : { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) ) |
22 |
21
|
imbi2d |
|- ( o = q -> ( ( T. -> ( G |` { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } ) : { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) <-> ( T. -> ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) : { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) ) ) |
23 |
1 2 3 4 5 6 7 8 9 10
|
eulerpartgbij |
|- G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) |
24 |
23
|
a1i |
|- ( T. -> G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) ) |
25 |
|
fveq2 |
|- ( q = o -> ( G ` q ) = ( G ` o ) ) |
26 |
|
reseq1 |
|- ( q = o -> ( q |` J ) = ( o |` J ) ) |
27 |
26
|
coeq2d |
|- ( q = o -> ( bits o. ( q |` J ) ) = ( bits o. ( o |` J ) ) ) |
28 |
27
|
fveq2d |
|- ( q = o -> ( M ` ( bits o. ( q |` J ) ) ) = ( M ` ( bits o. ( o |` J ) ) ) ) |
29 |
28
|
imaeq2d |
|- ( q = o -> ( F " ( M ` ( bits o. ( q |` J ) ) ) ) = ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) |
30 |
29
|
fveq2d |
|- ( q = o -> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( q |` J ) ) ) ) ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) |
31 |
25 30
|
eqeq12d |
|- ( q = o -> ( ( G ` q ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( q |` J ) ) ) ) ) <-> ( G ` o ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) ) |
32 |
1 2 3 4 5 6 7 8 9 10
|
eulerpartlemgv |
|- ( q e. ( T i^i R ) -> ( G ` q ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( q |` J ) ) ) ) ) ) |
33 |
31 32
|
vtoclga |
|- ( o e. ( T i^i R ) -> ( G ` o ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) |
34 |
33
|
3ad2ant2 |
|- ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> ( G ` o ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) |
35 |
|
simp3 |
|- ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) |
36 |
34 35
|
eqtr4d |
|- ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> ( G ` o ) = d ) |
37 |
36
|
fveq1d |
|- ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> ( ( G ` o ) ` k ) = ( d ` k ) ) |
38 |
37
|
oveq1d |
|- ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> ( ( ( G ` o ) ` k ) x. k ) = ( ( d ` k ) x. k ) ) |
39 |
38
|
sumeq2sdv |
|- ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> sum_ k e. NN ( ( ( G ` o ) ` k ) x. k ) = sum_ k e. NN ( ( d ` k ) x. k ) ) |
40 |
25
|
fveq2d |
|- ( q = o -> ( S ` ( G ` q ) ) = ( S ` ( G ` o ) ) ) |
41 |
|
fveq2 |
|- ( q = o -> ( S ` q ) = ( S ` o ) ) |
42 |
40 41
|
eqeq12d |
|- ( q = o -> ( ( S ` ( G ` q ) ) = ( S ` q ) <-> ( S ` ( G ` o ) ) = ( S ` o ) ) ) |
43 |
1 2 3 4 5 6 7 8 9 10 11
|
eulerpartlemgs2 |
|- ( q e. ( T i^i R ) -> ( S ` ( G ` q ) ) = ( S ` q ) ) |
44 |
42 43
|
vtoclga |
|- ( o e. ( T i^i R ) -> ( S ` ( G ` o ) ) = ( S ` o ) ) |
45 |
|
nn0ex |
|- NN0 e. _V |
46 |
|
0nn0 |
|- 0 e. NN0 |
47 |
|
1nn0 |
|- 1 e. NN0 |
48 |
|
prssi |
|- ( ( 0 e. NN0 /\ 1 e. NN0 ) -> { 0 , 1 } C_ NN0 ) |
49 |
46 47 48
|
mp2an |
|- { 0 , 1 } C_ NN0 |
50 |
|
mapss |
|- ( ( NN0 e. _V /\ { 0 , 1 } C_ NN0 ) -> ( { 0 , 1 } ^m NN ) C_ ( NN0 ^m NN ) ) |
51 |
45 49 50
|
mp2an |
|- ( { 0 , 1 } ^m NN ) C_ ( NN0 ^m NN ) |
52 |
|
ssrin |
|- ( ( { 0 , 1 } ^m NN ) C_ ( NN0 ^m NN ) -> ( ( { 0 , 1 } ^m NN ) i^i R ) C_ ( ( NN0 ^m NN ) i^i R ) ) |
53 |
51 52
|
ax-mp |
|- ( ( { 0 , 1 } ^m NN ) i^i R ) C_ ( ( NN0 ^m NN ) i^i R ) |
54 |
|
f1of |
|- ( G : ( T i^i R ) -1-1-onto-> ( ( { 0 , 1 } ^m NN ) i^i R ) -> G : ( T i^i R ) --> ( ( { 0 , 1 } ^m NN ) i^i R ) ) |
55 |
23 54
|
ax-mp |
|- G : ( T i^i R ) --> ( ( { 0 , 1 } ^m NN ) i^i R ) |
56 |
55
|
ffvelrni |
|- ( o e. ( T i^i R ) -> ( G ` o ) e. ( ( { 0 , 1 } ^m NN ) i^i R ) ) |
57 |
53 56
|
sselid |
|- ( o e. ( T i^i R ) -> ( G ` o ) e. ( ( NN0 ^m NN ) i^i R ) ) |
58 |
8 11
|
eulerpartlemsv1 |
|- ( ( G ` o ) e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` ( G ` o ) ) = sum_ k e. NN ( ( ( G ` o ) ` k ) x. k ) ) |
59 |
57 58
|
syl |
|- ( o e. ( T i^i R ) -> ( S ` ( G ` o ) ) = sum_ k e. NN ( ( ( G ` o ) ` k ) x. k ) ) |
60 |
1 2 3 4 5 6 7 8 9
|
eulerpartlemt0 |
|- ( o e. ( T i^i R ) <-> ( o e. ( NN0 ^m NN ) /\ ( `' o " NN ) e. Fin /\ ( `' o " NN ) C_ J ) ) |
61 |
60
|
simp1bi |
|- ( o e. ( T i^i R ) -> o e. ( NN0 ^m NN ) ) |
62 |
|
inss2 |
|- ( T i^i R ) C_ R |
63 |
62
|
sseli |
|- ( o e. ( T i^i R ) -> o e. R ) |
64 |
61 63
|
elind |
|- ( o e. ( T i^i R ) -> o e. ( ( NN0 ^m NN ) i^i R ) ) |
65 |
8 11
|
eulerpartlemsv1 |
|- ( o e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` o ) = sum_ k e. NN ( ( o ` k ) x. k ) ) |
66 |
64 65
|
syl |
|- ( o e. ( T i^i R ) -> ( S ` o ) = sum_ k e. NN ( ( o ` k ) x. k ) ) |
67 |
44 59 66
|
3eqtr3d |
|- ( o e. ( T i^i R ) -> sum_ k e. NN ( ( ( G ` o ) ` k ) x. k ) = sum_ k e. NN ( ( o ` k ) x. k ) ) |
68 |
67
|
3ad2ant2 |
|- ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> sum_ k e. NN ( ( ( G ` o ) ` k ) x. k ) = sum_ k e. NN ( ( o ` k ) x. k ) ) |
69 |
39 68
|
eqtr3d |
|- ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> sum_ k e. NN ( ( d ` k ) x. k ) = sum_ k e. NN ( ( o ` k ) x. k ) ) |
70 |
69
|
eqeq1d |
|- ( ( T. /\ o e. ( T i^i R ) /\ d = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) ) -> ( sum_ k e. NN ( ( d ` k ) x. k ) = N <-> sum_ k e. NN ( ( o ` k ) x. k ) = N ) ) |
71 |
10 24 70
|
f1oresrab |
|- ( T. -> ( G |` { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } ) : { o e. ( T i^i R ) | sum_ k e. NN ( ( o ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) |
72 |
22 71
|
chvarvv |
|- ( T. -> ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) : { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) |
73 |
|
cnveq |
|- ( g = q -> `' g = `' q ) |
74 |
73
|
imaeq1d |
|- ( g = q -> ( `' g " NN ) = ( `' q " NN ) ) |
75 |
74
|
raleqdv |
|- ( g = q -> ( A. n e. ( `' g " NN ) -. 2 || n <-> A. n e. ( `' q " NN ) -. 2 || n ) ) |
76 |
75
|
cbvrabv |
|- { g e. P | A. n e. ( `' g " NN ) -. 2 || n } = { q e. P | A. n e. ( `' q " NN ) -. 2 || n } |
77 |
|
nfrab1 |
|- F/_ q { q e. P | A. n e. ( `' q " NN ) -. 2 || n } |
78 |
|
nfrab1 |
|- F/_ q { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } |
79 |
|
df-3an |
|- ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) <-> ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) ) |
80 |
79
|
anbi1i |
|- ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) /\ A. n e. ( `' q " NN ) -. 2 || n ) <-> ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) /\ A. n e. ( `' q " NN ) -. 2 || n ) ) |
81 |
1
|
eulerpartleme |
|- ( q e. P <-> ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) ) |
82 |
81
|
anbi1i |
|- ( ( q e. P /\ A. n e. ( `' q " NN ) -. 2 || n ) <-> ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) /\ A. n e. ( `' q " NN ) -. 2 || n ) ) |
83 |
|
an32 |
|- ( ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ A. n e. ( `' q " NN ) -. 2 || n ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) <-> ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) /\ A. n e. ( `' q " NN ) -. 2 || n ) ) |
84 |
80 82 83
|
3bitr4i |
|- ( ( q e. P /\ A. n e. ( `' q " NN ) -. 2 || n ) <-> ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ A. n e. ( `' q " NN ) -. 2 || n ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) ) |
85 |
1 2 3 4 5 6 7 8 9
|
eulerpartlemt0 |
|- ( q e. ( T i^i R ) <-> ( q e. ( NN0 ^m NN ) /\ ( `' q " NN ) e. Fin /\ ( `' q " NN ) C_ J ) ) |
86 |
|
nnex |
|- NN e. _V |
87 |
45 86
|
elmap |
|- ( q e. ( NN0 ^m NN ) <-> q : NN --> NN0 ) |
88 |
87
|
3anbi1i |
|- ( ( q e. ( NN0 ^m NN ) /\ ( `' q " NN ) e. Fin /\ ( `' q " NN ) C_ J ) <-> ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ ( `' q " NN ) C_ J ) ) |
89 |
85 88
|
bitri |
|- ( q e. ( T i^i R ) <-> ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ ( `' q " NN ) C_ J ) ) |
90 |
|
df-3an |
|- ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin /\ ( `' q " NN ) C_ J ) <-> ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ ( `' q " NN ) C_ J ) ) |
91 |
|
dfss3 |
|- ( ( `' q " NN ) C_ J <-> A. n e. ( `' q " NN ) n e. J ) |
92 |
|
breq2 |
|- ( z = n -> ( 2 || z <-> 2 || n ) ) |
93 |
92
|
notbid |
|- ( z = n -> ( -. 2 || z <-> -. 2 || n ) ) |
94 |
93 4
|
elrab2 |
|- ( n e. J <-> ( n e. NN /\ -. 2 || n ) ) |
95 |
94
|
ralbii |
|- ( A. n e. ( `' q " NN ) n e. J <-> A. n e. ( `' q " NN ) ( n e. NN /\ -. 2 || n ) ) |
96 |
|
r19.26 |
|- ( A. n e. ( `' q " NN ) ( n e. NN /\ -. 2 || n ) <-> ( A. n e. ( `' q " NN ) n e. NN /\ A. n e. ( `' q " NN ) -. 2 || n ) ) |
97 |
91 95 96
|
3bitri |
|- ( ( `' q " NN ) C_ J <-> ( A. n e. ( `' q " NN ) n e. NN /\ A. n e. ( `' q " NN ) -. 2 || n ) ) |
98 |
|
cnvimass |
|- ( `' q " NN ) C_ dom q |
99 |
|
fdm |
|- ( q : NN --> NN0 -> dom q = NN ) |
100 |
98 99
|
sseqtrid |
|- ( q : NN --> NN0 -> ( `' q " NN ) C_ NN ) |
101 |
|
dfss3 |
|- ( ( `' q " NN ) C_ NN <-> A. n e. ( `' q " NN ) n e. NN ) |
102 |
100 101
|
sylib |
|- ( q : NN --> NN0 -> A. n e. ( `' q " NN ) n e. NN ) |
103 |
102
|
biantrurd |
|- ( q : NN --> NN0 -> ( A. n e. ( `' q " NN ) -. 2 || n <-> ( A. n e. ( `' q " NN ) n e. NN /\ A. n e. ( `' q " NN ) -. 2 || n ) ) ) |
104 |
97 103
|
bitr4id |
|- ( q : NN --> NN0 -> ( ( `' q " NN ) C_ J <-> A. n e. ( `' q " NN ) -. 2 || n ) ) |
105 |
104
|
adantr |
|- ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) -> ( ( `' q " NN ) C_ J <-> A. n e. ( `' q " NN ) -. 2 || n ) ) |
106 |
105
|
pm5.32i |
|- ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ ( `' q " NN ) C_ J ) <-> ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ A. n e. ( `' q " NN ) -. 2 || n ) ) |
107 |
89 90 106
|
3bitri |
|- ( q e. ( T i^i R ) <-> ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ A. n e. ( `' q " NN ) -. 2 || n ) ) |
108 |
107
|
anbi1i |
|- ( ( q e. ( T i^i R ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) <-> ( ( ( q : NN --> NN0 /\ ( `' q " NN ) e. Fin ) /\ A. n e. ( `' q " NN ) -. 2 || n ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) ) |
109 |
84 108
|
bitr4i |
|- ( ( q e. P /\ A. n e. ( `' q " NN ) -. 2 || n ) <-> ( q e. ( T i^i R ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) ) |
110 |
|
rabid |
|- ( q e. { q e. P | A. n e. ( `' q " NN ) -. 2 || n } <-> ( q e. P /\ A. n e. ( `' q " NN ) -. 2 || n ) ) |
111 |
|
rabid |
|- ( q e. { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } <-> ( q e. ( T i^i R ) /\ sum_ k e. NN ( ( q ` k ) x. k ) = N ) ) |
112 |
109 110 111
|
3bitr4i |
|- ( q e. { q e. P | A. n e. ( `' q " NN ) -. 2 || n } <-> q e. { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) |
113 |
77 78 112
|
eqri |
|- { q e. P | A. n e. ( `' q " NN ) -. 2 || n } = { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } |
114 |
2 76 113
|
3eqtri |
|- O = { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } |
115 |
114
|
reseq2i |
|- ( G |` O ) = ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) |
116 |
115
|
a1i |
|- ( T. -> ( G |` O ) = ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) ) |
117 |
114
|
a1i |
|- ( T. -> O = { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) |
118 |
|
nfcv |
|- F/_ d D |
119 |
|
nfrab1 |
|- F/_ d { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } |
120 |
|
fnima |
|- ( d Fn NN -> ( d " NN ) = ran d ) |
121 |
120
|
sseq1d |
|- ( d Fn NN -> ( ( d " NN ) C_ { 0 , 1 } <-> ran d C_ { 0 , 1 } ) ) |
122 |
121
|
anbi2d |
|- ( d Fn NN -> ( ( ran d C_ NN0 /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ran d C_ NN0 /\ ran d C_ { 0 , 1 } ) ) ) |
123 |
|
sstr |
|- ( ( ran d C_ { 0 , 1 } /\ { 0 , 1 } C_ NN0 ) -> ran d C_ NN0 ) |
124 |
49 123
|
mpan2 |
|- ( ran d C_ { 0 , 1 } -> ran d C_ NN0 ) |
125 |
124
|
pm4.71ri |
|- ( ran d C_ { 0 , 1 } <-> ( ran d C_ NN0 /\ ran d C_ { 0 , 1 } ) ) |
126 |
122 125
|
bitr4di |
|- ( d Fn NN -> ( ( ran d C_ NN0 /\ ( d " NN ) C_ { 0 , 1 } ) <-> ran d C_ { 0 , 1 } ) ) |
127 |
126
|
pm5.32i |
|- ( ( d Fn NN /\ ( ran d C_ NN0 /\ ( d " NN ) C_ { 0 , 1 } ) ) <-> ( d Fn NN /\ ran d C_ { 0 , 1 } ) ) |
128 |
|
anass |
|- ( ( ( d Fn NN /\ ran d C_ NN0 ) /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( d Fn NN /\ ( ran d C_ NN0 /\ ( d " NN ) C_ { 0 , 1 } ) ) ) |
129 |
|
df-f |
|- ( d : NN --> { 0 , 1 } <-> ( d Fn NN /\ ran d C_ { 0 , 1 } ) ) |
130 |
127 128 129
|
3bitr4ri |
|- ( d : NN --> { 0 , 1 } <-> ( ( d Fn NN /\ ran d C_ NN0 ) /\ ( d " NN ) C_ { 0 , 1 } ) ) |
131 |
|
prex |
|- { 0 , 1 } e. _V |
132 |
131 86
|
elmap |
|- ( d e. ( { 0 , 1 } ^m NN ) <-> d : NN --> { 0 , 1 } ) |
133 |
|
df-f |
|- ( d : NN --> NN0 <-> ( d Fn NN /\ ran d C_ NN0 ) ) |
134 |
133
|
anbi1i |
|- ( ( d : NN --> NN0 /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ( d Fn NN /\ ran d C_ NN0 ) /\ ( d " NN ) C_ { 0 , 1 } ) ) |
135 |
130 132 134
|
3bitr4i |
|- ( d e. ( { 0 , 1 } ^m NN ) <-> ( d : NN --> NN0 /\ ( d " NN ) C_ { 0 , 1 } ) ) |
136 |
|
vex |
|- d e. _V |
137 |
|
cnveq |
|- ( f = d -> `' f = `' d ) |
138 |
137
|
imaeq1d |
|- ( f = d -> ( `' f " NN ) = ( `' d " NN ) ) |
139 |
138
|
eleq1d |
|- ( f = d -> ( ( `' f " NN ) e. Fin <-> ( `' d " NN ) e. Fin ) ) |
140 |
136 139 8
|
elab2 |
|- ( d e. R <-> ( `' d " NN ) e. Fin ) |
141 |
135 140
|
anbi12i |
|- ( ( d e. ( { 0 , 1 } ^m NN ) /\ d e. R ) <-> ( ( d : NN --> NN0 /\ ( d " NN ) C_ { 0 , 1 } ) /\ ( `' d " NN ) e. Fin ) ) |
142 |
|
elin |
|- ( d e. ( ( { 0 , 1 } ^m NN ) i^i R ) <-> ( d e. ( { 0 , 1 } ^m NN ) /\ d e. R ) ) |
143 |
|
an32 |
|- ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ( d : NN --> NN0 /\ ( d " NN ) C_ { 0 , 1 } ) /\ ( `' d " NN ) e. Fin ) ) |
144 |
141 142 143
|
3bitr4i |
|- ( d e. ( ( { 0 , 1 } ^m NN ) i^i R ) <-> ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ ( d " NN ) C_ { 0 , 1 } ) ) |
145 |
144
|
anbi1i |
|- ( ( d e. ( ( { 0 , 1 } ^m NN ) i^i R ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) <-> ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ ( d " NN ) C_ { 0 , 1 } ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) ) |
146 |
1
|
eulerpartleme |
|- ( d e. P <-> ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) ) |
147 |
146
|
anbi1i |
|- ( ( d e. P /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) /\ ( d " NN ) C_ { 0 , 1 } ) ) |
148 |
|
df-3an |
|- ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) <-> ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) ) |
149 |
148
|
anbi1i |
|- ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) /\ ( d " NN ) C_ { 0 , 1 } ) ) |
150 |
|
an32 |
|- ( ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ ( d " NN ) C_ { 0 , 1 } ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) ) |
151 |
147 149 150
|
3bitri |
|- ( ( d e. P /\ ( d " NN ) C_ { 0 , 1 } ) <-> ( ( ( d : NN --> NN0 /\ ( `' d " NN ) e. Fin ) /\ ( d " NN ) C_ { 0 , 1 } ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) ) |
152 |
145 151
|
bitr4i |
|- ( ( d e. ( ( { 0 , 1 } ^m NN ) i^i R ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) <-> ( d e. P /\ ( d " NN ) C_ { 0 , 1 } ) ) |
153 |
|
rabid |
|- ( d e. { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } <-> ( d e. ( ( { 0 , 1 } ^m NN ) i^i R ) /\ sum_ k e. NN ( ( d ` k ) x. k ) = N ) ) |
154 |
1 2 3
|
eulerpartlemd |
|- ( d e. D <-> ( d e. P /\ ( d " NN ) C_ { 0 , 1 } ) ) |
155 |
152 153 154
|
3bitr4ri |
|- ( d e. D <-> d e. { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) |
156 |
118 119 155
|
eqri |
|- D = { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } |
157 |
156
|
a1i |
|- ( T. -> D = { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) |
158 |
116 117 157
|
f1oeq123d |
|- ( T. -> ( ( G |` O ) : O -1-1-onto-> D <-> ( G |` { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } ) : { q e. ( T i^i R ) | sum_ k e. NN ( ( q ` k ) x. k ) = N } -1-1-onto-> { d e. ( ( { 0 , 1 } ^m NN ) i^i R ) | sum_ k e. NN ( ( d ` k ) x. k ) = N } ) ) |
159 |
72 158
|
mpbird |
|- ( T. -> ( G |` O ) : O -1-1-onto-> D ) |
160 |
159
|
mptru |
|- ( G |` O ) : O -1-1-onto-> D |