Metamath Proof Explorer

Theorem eulerpartlemgs2

Description: Lemma for eulerpart : The G function also preserves partition sums. (Contributed by Thierry Arnoux, 10-Sep-2017)

Ref Expression
Hypotheses eulerpart.p 
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
eulerpart.o 
|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
eulerpart.d 
|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
eulerpart.j 
|- J = { z e. NN | -. 2 || z }
eulerpart.f 
|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
eulerpart.h 
|- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
eulerpart.m 
|- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
eulerpart.r 
|- R = { f | ( `' f " NN ) e. Fin }
eulerpart.t 
|- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
eulerpart.g 
|- G = ( o e. ( T i^i R ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
eulerpart.s 
|- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
Assertion eulerpartlemgs2 
|- ( A e. ( T i^i R ) -> ( S ` ( G ` A ) ) = ( S ` A ) )

Proof

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 19 20 syl 
 |-  ( A e. ( T i^i R ) -> ( G ` A ) : NN --> { 0 , 1 } )
50 ffn 
 |-  ( ( G ` A ) : NN --> { 0 , 1 } -> ( G ` A ) Fn NN )
51 elpreima 
 |-  ( ( G ` A ) Fn NN -> ( k e. ( `' ( G ` A ) " NN ) <-> ( k e. NN /\ ( ( G ` A ) ` k ) e. NN ) ) )
52 49 50 51 3syl 
 |-  ( A e. ( T i^i R ) -> ( k e. ( `' ( G ` A ) " NN ) <-> ( k e. NN /\ ( ( G ` A ) ` k ) e. NN ) ) )
53 52 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 ) ) )
54 42 48 53 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 ) )
55 54 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 ) ) )
56 55 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 ) )
57 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 )
58 41 56 57 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 )
59 cnvexg 
 |-  ( A e. ( T i^i R ) -> `' A e. _V )
60 imaexg 
 |-  ( `' A e. _V -> ( `' A " NN ) e. _V )
61 inex1g 
 |-  ( ( `' A " NN ) e. _V -> ( ( `' A " NN ) i^i J ) e. _V )
62 59 60 61 3syl 
 |-  ( A e. ( T i^i R ) -> ( ( `' A " NN ) i^i J ) e. _V )
63 vsnex 
 |-  { t } e. _V
64 fvex 
 |-  ( bits ` ( A ` t ) ) e. _V
65 63 64 xpex 
 |-  ( { t } X. ( bits ` ( A ` t ) ) ) e. _V
66 65 rgenw 
 |-  A. t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) e. _V
67 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 )
68 62 66 67 sylancl 
 |-  ( A e. ( T i^i R ) -> U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) e. _V )
69 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 ) ) )
70 1 2 3 4 5 6 7 8 9 10 69 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 } )
71 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 } )
72 68 70 71 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 } )
73 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 )
74 58 72 73 syl2anc 
 |-  ( A e. ( T i^i R ) -> U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) e. Fin )
75 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 ) )
76 75 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 ) )
77 inss2 
 |-  ( ( `' A " NN ) i^i J ) C_ J
78 simpr 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> t e. ( ( `' A " NN ) i^i J ) )
79 77 78 sselid 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> t e. J )
80 79 snssd 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> { t } C_ J )
81 bitsss 
 |-  ( bits ` ( A ` t ) ) C_ NN0
82 xpss12 
 |-  ( ( { t } C_ J /\ ( bits ` ( A ` t ) ) C_ NN0 ) -> ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) )
83 80 81 82 sylancl 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) )
84 83 ralrimiva 
 |-  ( A e. ( T i^i R ) -> A. t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) )
85 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 ) )
86 84 85 sylibr 
 |-  ( A e. ( T i^i R ) -> U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) )
87 86 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 ) )
88 4 5 oddpwdcv 
 |-  ( w e. ( J X. NN0 ) -> ( F ` w ) = ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) )
89 87 88 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 ) ) )
90 76 89 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 ) ) )
91 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 )
92 40 74 70 90 91 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 ) ) )
93 39 92 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 ) ) )
94 ax-1cn 
 |-  1 e. CC
95 0cn 
 |-  0 e. CC
96 94 95 ifcli 
 |-  if ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = k , 1 , 0 ) e. CC
97 96 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 )
98 ssrab2 
 |-  { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } C_ NN
99 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 } )
100 98 99 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 )
101 100 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 )
102 97 101 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 )
103 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 } ) )
104 103 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 } )
105 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 )
106 105 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 )
107 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 ) )
108 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 ) )
109 107 108 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 ) )
110 104 106 109 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 )
111 110 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 )
112 111 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 ) )
113 nnsscn 
 |-  NN C_ CC
114 105 113 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 )
115 114 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 )
116 115 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 )
117 112 116 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 )
118 56 102 117 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 ) )
119 93 118 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 ) )
120 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 ) )
121 120 simp1bi 
 |-  ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) )
122 elmapi 
 |-  ( A e. ( NN0 ^m NN ) -> A : NN --> NN0 )
123 121 122 syl 
 |-  ( A e. ( T i^i R ) -> A : NN --> NN0 )
124 123 adantr 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> A : NN --> NN0 )
125 cnvimass 
 |-  ( `' A " NN ) C_ dom A
126 125 123 fssdm 
 |-  ( A e. ( T i^i R ) -> ( `' A " NN ) C_ NN )
127 126 adantr 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( `' A " NN ) C_ NN )
128 inss1 
 |-  ( ( `' A " NN ) i^i J ) C_ ( `' A " NN )
129 128 78 sselid 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> t e. ( `' A " NN ) )
130 127 129 sseldd 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> t e. NN )
131 124 130 ffvelcdmd 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( A ` t ) e. NN0 )
132 bitsfi 
 |-  ( ( A ` t ) e. NN0 -> ( bits ` ( A ` t ) ) e. Fin )
133 131 132 syl 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> ( bits ` ( A ` t ) ) e. Fin )
134 130 nncnd 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) -> t e. CC )
135 2cnd 
 |-  ( ( A e. ( T i^i R ) /\ ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( bits ` ( A ` t ) ) ) ) -> 2 e. CC )
136 simprr 
 |-  ( ( A e. ( T i^i R ) /\ ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( bits ` ( A ` t ) ) ) ) -> n e. ( bits ` ( A ` t ) ) )
137 81 136 sselid 
 |-  ( ( A e. ( T i^i R ) /\ ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( bits ` ( A ` t ) ) ) ) -> n e. NN0 )
138 135 137 expcld 
 |-  ( ( A e. ( T i^i R ) /\ ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( 2 ^ n ) e. CC )
139 138 anassrs 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. ( ( `' A " NN ) i^i J ) ) /\ n e. ( bits ` ( A ` t ) ) ) -> ( 2 ^ n ) e. CC )
140 133 134 139 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 ) )
141 140 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 ) )
142 bitsinv1 
 |-  ( ( A ` t ) e. NN0 -> sum_ n e. ( bits ` ( A ` t ) ) ( 2 ^ n ) = ( A ` t ) )
143 142 oveq1d 
 |-  ( ( A ` t ) e. NN0 -> ( sum_ n e. ( bits ` ( A ` t ) ) ( 2 ^ n ) x. t ) = ( ( A ` t ) x. t ) )
144 131 143 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 ) )
145 144 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 ) )
146 vex 
 |-  t e. _V
147 vex 
 |-  n e. _V
148 146 147 op2ndd 
 |-  ( w = <. t , n >. -> ( 2nd ` w ) = n )
149 148 oveq2d 
 |-  ( w = <. t , n >. -> ( 2 ^ ( 2nd ` w ) ) = ( 2 ^ n ) )
150 146 147 op1std 
 |-  ( w = <. t , n >. -> ( 1st ` w ) = t )
151 149 150 oveq12d 
 |-  ( w = <. t , n >. -> ( ( 2 ^ ( 2nd ` w ) ) x. ( 1st ` w ) ) = ( ( 2 ^ n ) x. t ) )
152 inss2 
 |-  ( T i^i R ) C_ R
153 152 sseli 
 |-  ( A e. ( T i^i R ) -> A e. R )
154 cnveq 
 |-  ( f = A -> `' f = `' A )
155 154 imaeq1d 
 |-  ( f = A -> ( `' f " NN ) = ( `' A " NN ) )
156 155 eleq1d 
 |-  ( f = A -> ( ( `' f " NN ) e. Fin <-> ( `' A " NN ) e. Fin ) )
157 156 8 elab2g 
 |-  ( A e. ( T i^i R ) -> ( A e. R <-> ( `' A " NN ) e. Fin ) )
158 153 157 mpbid 
 |-  ( A e. ( T i^i R ) -> ( `' A " NN ) e. Fin )
159 ssfi 
 |-  ( ( ( `' A " NN ) e. Fin /\ ( ( `' A " NN ) i^i J ) C_ ( `' A " NN ) ) -> ( ( `' A " NN ) i^i J ) e. Fin )
160 158 128 159 sylancl 
 |-  ( A e. ( T i^i R ) -> ( ( `' A " NN ) i^i J ) e. Fin )
161 134 adantrr 
 |-  ( ( A e. ( T i^i R ) /\ ( t e. ( ( `' A " NN ) i^i J ) /\ n e. ( bits ` ( A ` t ) ) ) ) -> t e. CC )
162 138 161 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 )
163 151 160 133 162 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 ) ) )
164 141 145 163 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 ) ) )
165 inss1 
 |-  ( T i^i R ) C_ T
166 165 sseli 
 |-  ( A e. ( T i^i R ) -> A e. T )
167 155 sseq1d 
 |-  ( f = A -> ( ( `' f " NN ) C_ J <-> ( `' A " NN ) C_ J ) )
168 167 9 elrab2 
 |-  ( A e. T <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) C_ J ) )
169 168 simprbi 
 |-  ( A e. T -> ( `' A " NN ) C_ J )
170 166 169 syl 
 |-  ( A e. ( T i^i R ) -> ( `' A " NN ) C_ J )
171 dfss2 
 |-  ( ( `' A " NN ) C_ J <-> ( ( `' A " NN ) i^i J ) = ( `' A " NN ) )
172 170 171 sylib 
 |-  ( A e. ( T i^i R ) -> ( ( `' A " NN ) i^i J ) = ( `' A " NN ) )
173 172 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 ) )
174 164 173 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 ) )
175 28 119 174 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 ) )
176 fveq2 
 |-  ( k = t -> ( A ` k ) = ( A ` t ) )
177 id 
 |-  ( k = t -> k = t )
178 176 177 oveq12d 
 |-  ( k = t -> ( ( A ` k ) x. k ) = ( ( A ` t ) x. t ) )
179 178 cbvsumv 
 |-  sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) = sum_ t e. ( `' A " NN ) ( ( A ` t ) x. t )
180 175 179 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 ) )
181 0nn0 
 |-  0 e. NN0
182 1nn0 
 |-  1 e. NN0
183 prssi 
 |-  ( ( 0 e. NN0 /\ 1 e. NN0 ) -> { 0 , 1 } C_ NN0 )
184 181 182 183 mp2an 
 |-  { 0 , 1 } C_ NN0
185 fss 
 |-  ( ( ( G ` A ) : NN --> { 0 , 1 } /\ { 0 , 1 } C_ NN0 ) -> ( G ` A ) : NN --> NN0 )
186 184 185 mpan2 
 |-  ( ( G ` A ) : NN --> { 0 , 1 } -> ( G ` A ) : NN --> NN0 )
187 nn0ex 
 |-  NN0 e. _V
188 nnex 
 |-  NN e. _V
189 187 188 elmap 
 |-  ( ( G ` A ) e. ( NN0 ^m NN ) <-> ( G ` A ) : NN --> NN0 )
190 189 biimpri 
 |-  ( ( G ` A ) : NN --> NN0 -> ( G ` A ) e. ( NN0 ^m NN ) )
191 20 186 190 3syl 
 |-  ( ( G ` A ) e. ( { 0 , 1 } ^m NN ) -> ( G ` A ) e. ( NN0 ^m NN ) )
192 191 anim1i 
 |-  ( ( ( G ` A ) e. ( { 0 , 1 } ^m NN ) /\ ( G ` A ) e. R ) -> ( ( G ` A ) e. ( NN0 ^m NN ) /\ ( G ` A ) e. R ) )
193 elin 
 |-  ( ( G ` A ) e. ( ( NN0 ^m NN ) i^i R ) <-> ( ( G ` A ) e. ( NN0 ^m NN ) /\ ( G ` A ) e. R ) )
194 192 17 193 3imtr4i 
 |-  ( ( G ` A ) e. ( ( { 0 , 1 } ^m NN ) i^i R ) -> ( G ` A ) e. ( ( NN0 ^m NN ) i^i R ) )
195 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 ) )
196 16 194 195 3syl 
 |-  ( A e. ( T i^i R ) -> ( S ` ( G ` A ) ) = sum_ k e. ( `' ( G ` A ) " NN ) ( ( ( G ` A ) ` k ) x. k ) )
197 121 153 elind 
 |-  ( A e. ( T i^i R ) -> A e. ( ( NN0 ^m NN ) i^i R ) )
198 8 11 eulerpartlemsv2 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) )
199 197 198 syl 
 |-  ( A e. ( T i^i R ) -> ( S ` A ) = sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) )
200 180 196 199 3eqtr4d 
 |-  ( A e. ( T i^i R ) -> ( S ` ( G ` A ) ) = ( S ` A ) )