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 |
|
cnvimass |
|- ( `' ( G ` A ) " NN ) C_ dom ( G ` A ) |
13 |
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 ) |
14 |
|
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 ) ) |
15 |
13 14
|
ax-mp |
|- G : ( T i^i R ) --> ( ( { 0 , 1 } ^m NN ) i^i R ) |
16 |
15
|
ffvelcdmi |
|- ( A e. ( T i^i R ) -> ( G ` A ) e. ( ( { 0 , 1 } ^m NN ) i^i R ) ) |
17 |
|
elin |
|- ( ( G ` A ) e. ( ( { 0 , 1 } ^m NN ) i^i R ) <-> ( ( G ` A ) e. ( { 0 , 1 } ^m NN ) /\ ( G ` A ) e. R ) ) |
18 |
16 17
|
sylib |
|- ( A e. ( T i^i R ) -> ( ( G ` A ) e. ( { 0 , 1 } ^m NN ) /\ ( G ` A ) e. R ) ) |
19 |
18
|
simpld |
|- ( A e. ( T i^i R ) -> ( G ` A ) e. ( { 0 , 1 } ^m NN ) ) |
20 |
|
elmapi |
|- ( ( G ` A ) e. ( { 0 , 1 } ^m NN ) -> ( G ` A ) : NN --> { 0 , 1 } ) |
21 |
|
fdm |
|- ( ( G ` A ) : NN --> { 0 , 1 } -> dom ( G ` A ) = NN ) |
22 |
19 20 21
|
3syl |
|- ( A e. ( T i^i R ) -> dom ( G ` A ) = NN ) |
23 |
12 22
|
sseqtrid |
|- ( A e. ( T i^i R ) -> ( `' ( G ` A ) " NN ) C_ NN ) |
24 |
23
|
sselda |
|- ( ( A e. ( T i^i R ) /\ k e. ( `' ( G ` A ) " NN ) ) -> k e. NN ) |
25 |
1 2 3 4 5 6 7 8 9 10
|
eulerpartlemgvv |
|- ( ( A e. ( T i^i R ) /\ k e. NN ) -> ( ( G ` A ) ` k ) = if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) ) |
26 |
25
|
oveq1d |
|- ( ( A e. ( T i^i R ) /\ k e. NN ) -> ( ( ( G ` A ) ` k ) x. k ) = ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) ) |
27 |
24 26
|
syldan |
|- ( ( A e. ( T i^i R ) /\ k e. ( `' ( G ` A ) " NN ) ) -> ( ( ( G ` A ) ` k ) x. k ) = ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) ) |
28 |
27
|
sumeq2dv |
|- ( A e. ( T i^i R ) -> sum_ k e. ( `' ( G ` A ) " NN ) ( ( ( G ` A ) ` k ) x. k ) = sum_ k e. ( `' ( G ` A ) " NN ) ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) ) |
29 |
|
eqeq2 |
|- ( m = k -> ( ( ( 2 ^ n ) x. t ) = m <-> ( ( 2 ^ n ) x. t ) = k ) ) |
30 |
29
|
2rexbidv |
|- ( m = k -> ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m <-> E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k ) ) |
31 |
30
|
elrab |
|- ( k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } <-> ( k e. NN /\ E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k ) ) |
32 |
31
|
simprbi |
|- ( k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } -> E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k ) |
33 |
32
|
iftrued |
|- ( k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } -> if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) = 1 ) |
34 |
33
|
oveq1d |
|- ( k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } -> ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) = ( 1 x. k ) ) |
35 |
|
elrabi |
|- ( k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } -> k e. NN ) |
36 |
35
|
nncnd |
|- ( k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } -> k e. CC ) |
37 |
36
|
mullidd |
|- ( k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } -> ( 1 x. k ) = k ) |
38 |
34 37
|
eqtrd |
|- ( k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } -> ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) = k ) |
39 |
38
|
sumeq2i |
|- sum_ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) = sum_ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } k |
40 |
|
id |
|- ( k = ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) -> k = ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) ) |
41 |
1 2 3 4 5 6 7 8 9 10
|
eulerpartlemgf |
|- ( A e. ( T i^i R ) -> ( `' ( G ` A ) " NN ) e. Fin ) |
42 |
35
|
adantl |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> k e. NN ) |
43 |
42 25
|
syldan |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> ( ( G ` A ) ` k ) = if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) ) |
44 |
32
|
adantl |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k ) |
45 |
44
|
iftrued |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) = 1 ) |
46 |
43 45
|
eqtrd |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> ( ( G ` A ) ` k ) = 1 ) |
47 |
|
1nn |
|- 1 e. NN |
48 |
46 47
|
eqeltrdi |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> ( ( G ` A ) ` k ) e. NN ) |
49 |
|
ffn |
|- ( ( G ` A ) : NN --> { 0 , 1 } -> ( G ` A ) Fn NN ) |
50 |
|
elpreima |
|- ( ( G ` A ) Fn NN -> ( k e. ( `' ( G ` A ) " NN ) <-> ( k e. NN /\ ( ( G ` A ) ` k ) e. NN ) ) ) |
51 |
19 20 49 50
|
4syl |
|- ( A e. ( T i^i R ) -> ( k e. ( `' ( G ` A ) " NN ) <-> ( k e. NN /\ ( ( G ` A ) ` k ) e. NN ) ) ) |
52 |
51
|
adantr |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> ( k e. ( `' ( G ` A ) " NN ) <-> ( k e. NN /\ ( ( G ` A ) ` k ) e. NN ) ) ) |
53 |
42 48 52
|
mpbir2and |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> k e. ( `' ( G ` A ) " NN ) ) |
54 |
53
|
ex |
|- ( A e. ( T i^i R ) -> ( k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } -> k e. ( `' ( G ` A ) " NN ) ) ) |
55 |
54
|
ssrdv |
|- ( A e. ( T i^i R ) -> { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } C_ ( `' ( G ` A ) " NN ) ) |
56 |
|
ssfi |
|- ( ( ( `' ( G ` A ) " NN ) e. Fin /\ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } C_ ( `' ( G ` A ) " NN ) ) -> { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } e. Fin ) |
57 |
41 55 56
|
syl2anc |
|- ( A e. ( T i^i R ) -> { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } e. Fin ) |
58 |
|
cnvexg |
|- ( A e. ( T i^i R ) -> `' A e. _V ) |
59 |
|
imaexg |
|- ( `' A e. _V -> ( `' A " NN ) e. _V ) |
60 |
|
inex1g |
|- ( ( `' A " NN ) e. _V -> ( ( `' A " NN ) i^i J ) e. _V ) |
61 |
58 59 60
|
3syl |
|- ( A e. ( T i^i R ) -> ( ( `' A " NN ) i^i J ) e. _V ) |
62 |
|
vsnex |
|- { t } e. _V |
63 |
|
fvex |
|- ( bits ` ( A ` t ) ) e. _V |
64 |
62 63
|
xpex |
|- ( { t } X. ( bits ` ( A ` t ) ) ) e. _V |
65 |
64
|
rgenw |
|- A. t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) e. _V |
66 |
|
iunexg |
|- ( ( ( ( `' A " NN ) i^i J ) e. _V /\ A. t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) e. _V ) -> U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) e. _V ) |
67 |
61 65 66
|
sylancl |
|- ( A e. ( T i^i R ) -> U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) e. _V ) |
68 |
|
eqid |
|- U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) = U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) |
69 |
1 2 3 4 5 6 7 8 9 10 68
|
eulerpartlemgh |
|- ( A e. ( T i^i R ) -> ( F |` U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ) : U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) -1-1-onto-> { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) |
70 |
|
f1oeng |
|- ( ( U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) e. _V /\ ( F |` U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ) : U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) -1-1-onto-> { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ~~ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) |
71 |
67 69 70
|
syl2anc |
|- ( A e. ( T i^i R ) -> U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ~~ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) |
72 |
|
enfii |
|- ( ( { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } e. Fin /\ U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ~~ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) e. Fin ) |
73 |
57 71 72
|
syl2anc |
|- ( A e. ( T i^i R ) -> U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) e. Fin ) |
74 |
|
fvres |
|- ( w e. U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) -> ( ( F |` U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ) ` w ) = ( F ` w ) ) |
75 |
74
|
adantl |
|- ( ( A e. ( T i^i R ) /\ w e. U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ) -> ( ( F |` U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ) ` w ) = ( F ` w ) ) |
76 |
|
inss2 |
|- ( ( `' A " NN ) i^i J ) C_ J |
77 |
|
simpr |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> t e. ( ( `' A " NN ) i^i J ) ) |
78 |
76 77
|
sselid |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> t e. J ) |
79 |
78
|
snssd |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> { t } C_ J ) |
80 |
|
bitsss |
|- ( bits ` ( A ` t ) ) C_ NN0 |
81 |
|
xpss12 |
|- ( ( { t } C_ J /\ ( bits ` ( A ` t ) ) C_ NN0 ) -> ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) ) |
82 |
79 80 81
|
sylancl |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) ) |
83 |
82
|
ralrimiva |
|- ( A e. ( T i^i R ) -> A. t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) ) |
84 |
|
iunss |
|- ( U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) <-> A. t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) ) |
85 |
83 84
|
sylibr |
|- ( A e. ( T i^i R ) -> U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) ) |
86 |
85
|
sselda |
|- ( ( A e. ( T i^i R ) /\ w e. U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ) -> w e. ( J X. NN0 ) ) |
87 |
4 5
|
oddpwdcv |
|- ( w e. ( J X. NN0 ) -> ( F ` w ) = ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) ) |
88 |
86 87
|
syl |
|- ( ( A e. ( T i^i R ) /\ w e. U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ) -> ( F ` w ) = ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) ) |
89 |
75 88
|
eqtrd |
|- ( ( A e. ( T i^i R ) /\ w e. U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ) -> ( ( F |` U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ) ` w ) = ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) ) |
90 |
42
|
nncnd |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> k e. CC ) |
91 |
40 73 69 89 90
|
fsumf1o |
|- ( A e. ( T i^i R ) -> sum_ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } k = sum_ w e. U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) ) |
92 |
39 91
|
eqtrid |
|- ( A e. ( T i^i R ) -> sum_ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) = sum_ w e. U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) ) |
93 |
|
ax-1cn |
|- 1 e. CC |
94 |
|
0cn |
|- 0 e. CC |
95 |
93 94
|
ifcli |
|- if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) e. CC |
96 |
95
|
a1i |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) e. CC ) |
97 |
|
ssrab2 |
|- { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } C_ NN |
98 |
|
simpr |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) |
99 |
97 98
|
sselid |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> k e. NN ) |
100 |
99
|
nncnd |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> k e. CC ) |
101 |
96 100
|
mulcld |
|- ( ( A e. ( T i^i R ) /\ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) -> ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) e. CC ) |
102 |
|
simpr |
|- ( ( A e. ( T i^i R ) /\ k e. ( ( `' ( G ` A ) " NN ) \ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) ) -> k e. ( ( `' ( G ` A ) " NN ) \ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) ) |
103 |
102
|
eldifbd |
|- ( ( A e. ( T i^i R ) /\ k e. ( ( `' ( G ` A ) " NN ) \ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) ) -> -. k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) |
104 |
23
|
ssdifssd |
|- ( A e. ( T i^i R ) -> ( ( `' ( G ` A ) " NN ) \ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) C_ NN ) |
105 |
104
|
sselda |
|- ( ( A e. ( T i^i R ) /\ k e. ( ( `' ( G ` A ) " NN ) \ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) ) -> k e. NN ) |
106 |
31
|
notbii |
|- ( -. k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } <-> -. ( k e. NN /\ E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k ) ) |
107 |
|
imnan |
|- ( ( k e. NN -> -. E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k ) <-> -. ( k e. NN /\ E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k ) ) |
108 |
106 107
|
sylbb2 |
|- ( -. k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } -> ( k e. NN -> -. E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k ) ) |
109 |
103 105 108
|
sylc |
|- ( ( A e. ( T i^i R ) /\ k e. ( ( `' ( G ` A ) " NN ) \ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) ) -> -. E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k ) |
110 |
109
|
iffalsed |
|- ( ( A e. ( T i^i R ) /\ k e. ( ( `' ( G ` A ) " NN ) \ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) ) -> if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) = 0 ) |
111 |
110
|
oveq1d |
|- ( ( A e. ( T i^i R ) /\ k e. ( ( `' ( G ` A ) " NN ) \ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) ) -> ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) = ( 0 x. k ) ) |
112 |
|
nnsscn |
|- NN C_ CC |
113 |
104 112
|
sstrdi |
|- ( A e. ( T i^i R ) -> ( ( `' ( G ` A ) " NN ) \ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) C_ CC ) |
114 |
113
|
sselda |
|- ( ( A e. ( T i^i R ) /\ k e. ( ( `' ( G ` A ) " NN ) \ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) ) -> k e. CC ) |
115 |
114
|
mul02d |
|- ( ( A e. ( T i^i R ) /\ k e. ( ( `' ( G ` A ) " NN ) \ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) ) -> ( 0 x. k ) = 0 ) |
116 |
111 115
|
eqtrd |
|- ( ( A e. ( T i^i R ) /\ k e. ( ( `' ( G ` A ) " NN ) \ { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) ) -> ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) = 0 ) |
117 |
55 101 116 41
|
fsumss |
|- ( A e. ( T i^i R ) -> sum_ k e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) = sum_ k e. ( `' ( G ` A ) " NN ) ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) ) |
118 |
92 117
|
eqtr3d |
|- ( A e. ( T i^i R ) -> sum_ w e. U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) = sum_ k e. ( `' ( G ` A ) " NN ) ( if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) x. k ) ) |
119 |
1 2 3 4 5 6 7 8 9
|
eulerpartlemt0 |
|- ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) ) |
120 |
119
|
simp1bi |
|- ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) ) |
121 |
|
elmapi |
|- ( A e. ( NN0 ^m NN ) -> A : NN --> NN0 ) |
122 |
120 121
|
syl |
|- ( A e. ( T i^i R ) -> A : NN --> NN0 ) |
123 |
122
|
adantr |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> A : NN --> NN0 ) |
124 |
|
cnvimass |
|- ( `' A " NN ) C_ dom A |
125 |
124 122
|
fssdm |
|- ( A e. ( T i^i R ) -> ( `' A " NN ) C_ NN ) |
126 |
125
|
adantr |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( `' A " NN ) C_ NN ) |
127 |
|
inss1 |
|- ( ( `' A " NN ) i^i J ) C_ ( `' A " NN ) |
128 |
127 77
|
sselid |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> t e. ( `' A " NN ) ) |
129 |
126 128
|
sseldd |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> t e. NN ) |
130 |
123 129
|
ffvelcdmd |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( A ` t ) e. NN0 ) |
131 |
|
bitsfi |
|- ( ( A ` t ) e. NN0 -> ( bits ` ( A ` t ) ) e. Fin ) |
132 |
130 131
|
syl |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( bits ` ( A ` t ) ) e. Fin ) |
133 |
129
|
nncnd |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> t e. CC ) |
134 |
|
2cnd |
|- ( ( A e. ( T i^i R ) /\ ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( bits ` ( A ` t ) ) ) ) -> 2 e. CC ) |
135 |
|
simprr |
|- ( ( A e. ( T i^i R ) /\ ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( bits ` ( A ` t ) ) ) ) -> n e. ( bits ` ( A ` t ) ) ) |
136 |
80 135
|
sselid |
|- ( ( A e. ( T i^i R ) /\ ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( bits ` ( A ` t ) ) ) ) -> n e. NN0 ) |
137 |
134 136
|
expcld |
|- ( ( A e. ( T i^i R ) /\ ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( 2 ^ n ) e. CC ) |
138 |
137
|
anassrs |
|- ( ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) /\ n e. ( bits ` ( A ` t ) ) ) -> ( 2 ^ n ) e. CC ) |
139 |
132 133 138
|
fsummulc1 |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( sum_ n e. ( bits ` ( A ` t ) ) ( 2 ^ n ) x. t ) = sum_ n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) ) |
140 |
139
|
sumeq2dv |
|- ( A e. ( T i^i R ) -> sum_ t e. ( ( `' A " NN ) i^i J ) ( sum_ n e. ( bits ` ( A ` t ) ) ( 2 ^ n ) x. t ) = sum_ t e. ( ( `' A " NN ) i^i J ) sum_ n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) ) |
141 |
|
bitsinv1 |
|- ( ( A ` t ) e. NN0 -> sum_ n e. ( bits ` ( A ` t ) ) ( 2 ^ n ) = ( A ` t ) ) |
142 |
141
|
oveq1d |
|- ( ( A ` t ) e. NN0 -> ( sum_ n e. ( bits ` ( A ` t ) ) ( 2 ^ n ) x. t ) = ( ( A ` t ) x. t ) ) |
143 |
130 142
|
syl |
|- ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( sum_ n e. ( bits ` ( A ` t ) ) ( 2 ^ n ) x. t ) = ( ( A ` t ) x. t ) ) |
144 |
143
|
sumeq2dv |
|- ( A e. ( T i^i R ) -> sum_ t e. ( ( `' A " NN ) i^i J ) ( sum_ n e. ( bits ` ( A ` t ) ) ( 2 ^ n ) x. t ) = sum_ t e. ( ( `' A " NN ) i^i J ) ( ( A ` t ) x. t ) ) |
145 |
|
vex |
|- t e. _V |
146 |
|
vex |
|- n e. _V |
147 |
145 146
|
op2ndd |
|- ( w = <. t , n >. -> ( 2nd ` w ) = n ) |
148 |
147
|
oveq2d |
|- ( w = <. t , n >. -> ( 2 ^ ( 2nd ` w ) ) = ( 2 ^ n ) ) |
149 |
145 146
|
op1std |
|- ( w = <. t , n >. -> ( 1st ` w ) = t ) |
150 |
148 149
|
oveq12d |
|- ( w = <. t , n >. -> ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) = ( ( 2 ^ n ) x. t ) ) |
151 |
|
inss2 |
|- ( T i^i R ) C_ R |
152 |
151
|
sseli |
|- ( A e. ( T i^i R ) -> A e. R ) |
153 |
|
cnveq |
|- ( f = A -> `' f = `' A ) |
154 |
153
|
imaeq1d |
|- ( f = A -> ( `' f " NN ) = ( `' A " NN ) ) |
155 |
154
|
eleq1d |
|- ( f = A -> ( ( `' f " NN ) e. Fin <-> ( `' A " NN ) e. Fin ) ) |
156 |
155 8
|
elab2g |
|- ( A e. ( T i^i R ) -> ( A e. R <-> ( `' A " NN ) e. Fin ) ) |
157 |
152 156
|
mpbid |
|- ( A e. ( T i^i R ) -> ( `' A " NN ) e. Fin ) |
158 |
|
ssfi |
|- ( ( ( `' A " NN ) e. Fin /\ ( ( `' A " NN ) i^i J ) C_ ( `' A " NN ) ) -> ( ( `' A " NN ) i^i J ) e. Fin ) |
159 |
157 127 158
|
sylancl |
|- ( A e. ( T i^i R ) -> ( ( `' A " NN ) i^i J ) e. Fin ) |
160 |
133
|
adantrr |
|- ( ( A e. ( T i^i R ) /\ ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( bits ` ( A ` t ) ) ) ) -> t e. CC ) |
161 |
137 160
|
mulcld |
|- ( ( A e. ( T i^i R ) /\ ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( ( 2 ^ n ) x. t ) e. CC ) |
162 |
150 159 132 161
|
fsum2d |
|- ( A e. ( T i^i R ) -> sum_ t e. ( ( `' A " NN ) i^i J ) sum_ n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = sum_ w e. U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) ) |
163 |
140 144 162
|
3eqtr3d |
|- ( A e. ( T i^i R ) -> sum_ t e. ( ( `' A " NN ) i^i J ) ( ( A ` t ) x. t ) = sum_ w e. U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) ) |
164 |
|
inss1 |
|- ( T i^i R ) C_ T |
165 |
164
|
sseli |
|- ( A e. ( T i^i R ) -> A e. T ) |
166 |
154
|
sseq1d |
|- ( f = A -> ( ( `' f " NN ) C_ J <-> ( `' A " NN ) C_ J ) ) |
167 |
166 9
|
elrab2 |
|- ( A e. T <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) C_ J ) ) |
168 |
167
|
simprbi |
|- ( A e. T -> ( `' A " NN ) C_ J ) |
169 |
165 168
|
syl |
|- ( A e. ( T i^i R ) -> ( `' A " NN ) C_ J ) |
170 |
|
dfss2 |
|- ( ( `' A " NN ) C_ J <-> ( ( `' A " NN ) i^i J ) = ( `' A " NN ) ) |
171 |
169 170
|
sylib |
|- ( A e. ( T i^i R ) -> ( ( `' A " NN ) i^i J ) = ( `' A " NN ) ) |
172 |
171
|
sumeq1d |
|- ( A e. ( T i^i R ) -> sum_ t e. ( ( `' A " NN ) i^i J ) ( ( A ` t ) x. t ) = sum_ t e. ( `' A " NN ) ( ( A ` t ) x. t ) ) |
173 |
163 172
|
eqtr3d |
|- ( A e. ( T i^i R ) -> sum_ w e. U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) = sum_ t e. ( `' A " NN ) ( ( A ` t ) x. t ) ) |
174 |
28 118 173
|
3eqtr2d |
|- ( A e. ( T i^i R ) -> sum_ k e. ( `' ( G ` A ) " NN ) ( ( ( G ` A ) ` k ) x. k ) = sum_ t e. ( `' A " NN ) ( ( A ` t ) x. t ) ) |
175 |
|
fveq2 |
|- ( k = t -> ( A ` k ) = ( A ` t ) ) |
176 |
|
id |
|- ( k = t -> k = t ) |
177 |
175 176
|
oveq12d |
|- ( k = t -> ( ( A ` k ) x. k ) = ( ( A ` t ) x. t ) ) |
178 |
177
|
cbvsumv |
|- sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) = sum_ t e. ( `' A " NN ) ( ( A ` t ) x. t ) |
179 |
174 178
|
eqtr4di |
|- ( A e. ( T i^i R ) -> sum_ k e. ( `' ( G ` A ) " NN ) ( ( ( G ` A ) ` k ) x. k ) = sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) ) |
180 |
|
0nn0 |
|- 0 e. NN0 |
181 |
|
1nn0 |
|- 1 e. NN0 |
182 |
|
prssi |
|- ( ( 0 e. NN0 /\ 1 e. NN0 ) -> { 0 , 1 } C_ NN0 ) |
183 |
180 181 182
|
mp2an |
|- { 0 , 1 } C_ NN0 |
184 |
|
fss |
|- ( ( ( G ` A ) : NN --> { 0 , 1 } /\ { 0 , 1 } C_ NN0 ) -> ( G ` A ) : NN --> NN0 ) |
185 |
183 184
|
mpan2 |
|- ( ( G ` A ) : NN --> { 0 , 1 } -> ( G ` A ) : NN --> NN0 ) |
186 |
|
nn0ex |
|- NN0 e. _V |
187 |
|
nnex |
|- NN e. _V |
188 |
186 187
|
elmap |
|- ( ( G ` A ) e. ( NN0 ^m NN ) <-> ( G ` A ) : NN --> NN0 ) |
189 |
188
|
biimpri |
|- ( ( G ` A ) : NN --> NN0 -> ( G ` A ) e. ( NN0 ^m NN ) ) |
190 |
20 185 189
|
3syl |
|- ( ( G ` A ) e. ( { 0 , 1 } ^m NN ) -> ( G ` A ) e. ( NN0 ^m NN ) ) |
191 |
190
|
anim1i |
|- ( ( ( G ` A ) e. ( { 0 , 1 } ^m NN ) /\ ( G ` A ) e. R ) -> ( ( G ` A ) e. ( NN0 ^m NN ) /\ ( G ` A ) e. R ) ) |
192 |
|
elin |
|- ( ( G ` A ) e. ( ( NN0 ^m NN ) i^i R ) <-> ( ( G ` A ) e. ( NN0 ^m NN ) /\ ( G ` A ) e. R ) ) |
193 |
191 17 192
|
3imtr4i |
|- ( ( G ` A ) e. ( ( { 0 , 1 } ^m NN ) i^i R ) -> ( G ` A ) e. ( ( NN0 ^m NN ) i^i R ) ) |
194 |
8 11
|
eulerpartlemsv2 |
|- ( ( G ` A ) e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` ( G ` A ) ) = sum_ k e. ( `' ( G ` A ) " NN ) ( ( ( G ` A ) ` k ) x. k ) ) |
195 |
16 193 194
|
3syl |
|- ( A e. ( T i^i R ) -> ( S ` ( G ` A ) ) = sum_ k e. ( `' ( G ` A ) " NN ) ( ( ( G ` A ) ` k ) x. k ) ) |
196 |
120 152
|
elind |
|- ( A e. ( T i^i R ) -> A e. ( ( NN0 ^m NN ) i^i R ) ) |
197 |
8 11
|
eulerpartlemsv2 |
|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) ) |
198 |
196 197
|
syl |
|- ( A e. ( T i^i R ) -> ( S ` A ) = sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) ) |
199 |
179 195 198
|
3eqtr4d |
|- ( A e. ( T i^i R ) -> ( S ` ( G ` A ) ) = ( S ` A ) ) |