Metamath Proof Explorer

Theorem eulerpart

Description: Euler's theorem on partitions, also known as a special case of Glaisher's theorem. Let P be the set of all partitions of N , represented as multisets of positive integers, which is to say functions from NN to NN0 where the value of the function represents the number of repetitions of an individual element, and the sum of all the elements with repetition equals N . Then the set O of all partitions that only consist of odd numbers and the set D of all partitions which have no repeated elements have the same cardinality. This is Metamath 100 proof #45. (Contributed by Thierry Arnoux, 14-Aug-2018) (Revised by Thierry Arnoux, 1-Sep-2019)

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 }
Assertion eulerpart 
|- ( # ` O ) = ( # ` D )

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 eqid 
 |-  { z e. NN | -. 2 || z } = { z e. NN | -. 2 || z }
5 oveq2 
 |-  ( a = x -> ( ( 2 ^ b ) x. a ) = ( ( 2 ^ b ) x. x ) )
6 oveq2 
 |-  ( b = y -> ( 2 ^ b ) = ( 2 ^ y ) )
7 6 oveq1d 
 |-  ( b = y -> ( ( 2 ^ b ) x. x ) = ( ( 2 ^ y ) x. x ) )
8 5 7 cbvmpov 
 |-  ( a e. { z e. NN | -. 2 || z } , b e. NN0 |-> ( ( 2 ^ b ) x. a ) ) = ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
9 oveq1 
 |-  ( r = m -> ( r supp (/) ) = ( m supp (/) ) )
10 9 eleq1d 
 |-  ( r = m -> ( ( r supp (/) ) e. Fin <-> ( m supp (/) ) e. Fin ) )
11 10 cbvrabv 
 |-  { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } = { m e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( m supp (/) ) e. Fin }
12 11 eqcomi 
 |-  { m e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( m supp (/) ) e. Fin } = { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin }
13 fveq1 
 |-  ( t = r -> ( t ` a ) = ( r ` a ) )
14 13 eleq2d 
 |-  ( t = r -> ( b e. ( t ` a ) <-> b e. ( r ` a ) ) )
15 14 anbi2d 
 |-  ( t = r -> ( ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) <-> ( a e. { z e. NN | -. 2 || z } /\ b e. ( r ` a ) ) ) )
16 15 opabbidv 
 |-  ( t = r -> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) } = { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( r ` a ) ) } )
17 16 cbvmptv 
 |-  ( t e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) } ) = ( r e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( r ` a ) ) } )
18 oveq1 
 |-  ( m = s -> ( m supp (/) ) = ( s supp (/) ) )
19 18 eleq1d 
 |-  ( m = s -> ( ( m supp (/) ) e. Fin <-> ( s supp (/) ) e. Fin ) )
20 19 cbvrabv 
 |-  { m e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( m supp (/) ) e. Fin } = { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin }
21 20 eqcomi 
 |-  { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } = { m e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( m supp (/) ) e. Fin }
22 simpl 
 |-  ( ( a = x /\ b = y ) -> a = x )
23 22 eleq1d 
 |-  ( ( a = x /\ b = y ) -> ( a e. { z e. NN | -. 2 || z } <-> x e. { z e. NN | -. 2 || z } ) )
24 simpr 
 |-  ( ( a = x /\ b = y ) -> b = y )
25 22 fveq2d 
 |-  ( ( a = x /\ b = y ) -> ( r ` a ) = ( r ` x ) )
26 24 25 eleq12d 
 |-  ( ( a = x /\ b = y ) -> ( b e. ( r ` a ) <-> y e. ( r ` x ) ) )
27 23 26 anbi12d 
 |-  ( ( a = x /\ b = y ) -> ( ( a e. { z e. NN | -. 2 || z } /\ b e. ( r ` a ) ) <-> ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) ) )
28 27 cbvopabv 
 |-  { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( r ` a ) ) } = { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) }
29 21 28 mpteq12i 
 |-  ( r e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( r ` a ) ) } ) = ( r e. { m e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( m supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } )
30 17 29 eqtri 
 |-  ( t e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) } ) = ( r e. { m e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( m supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } )
31 cnveq 
 |-  ( h = f -> `' h = `' f )
32 31 imaeq1d 
 |-  ( h = f -> ( `' h " NN ) = ( `' f " NN ) )
33 32 eleq1d 
 |-  ( h = f -> ( ( `' h " NN ) e. Fin <-> ( `' f " NN ) e. Fin ) )
34 33 cbvabv 
 |-  { h | ( `' h " NN ) e. Fin } = { f | ( `' f " NN ) e. Fin }
35 32 sseq1d 
 |-  ( h = f -> ( ( `' h " NN ) C_ { z e. NN | -. 2 || z } <-> ( `' f " NN ) C_ { z e. NN | -. 2 || z } ) )
36 35 cbvrabv 
 |-  { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ { z e. NN | -. 2 || z } }
37 reseq1 
 |-  ( o = q -> ( o |` { z e. NN | -. 2 || z } ) = ( q |` { z e. NN | -. 2 || z } ) )
38 37 coeq2d 
 |-  ( o = q -> ( bits o. ( o |` { z e. NN | -. 2 || z } ) ) = ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) )
39 38 fveq2d 
 |-  ( o = q -> ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( o |` { z e. NN | -. 2 || z } ) ) ) = ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) )
40 39 imaeq2d 
 |-  ( o = q -> ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( o |` { z e. NN | -. 2 || z } ) ) ) ) = ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) ) )
41 40 fveq2d 
 |-  ( o = q -> ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( o |` { z e. NN | -. 2 || z } ) ) ) ) ) = ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) ) ) )
42 41 cbvmptv 
 |-  ( o e. ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) |-> ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( o |` { z e. NN | -. 2 || z } ) ) ) ) ) ) = ( q e. ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) |-> ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) ) ) )
43 8 eqcomi 
 |-  ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) = ( a e. { z e. NN | -. 2 || z } , b e. NN0 |-> ( ( 2 ^ b ) x. a ) )
44 43 imaeq1i 
 |-  ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) ) = ( ( a e. { z e. NN | -. 2 || z } , b e. NN0 |-> ( ( 2 ^ b ) x. a ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) )
45 eqid 
 |-  { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } = { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) }
46 11 45 mpteq12i 
 |-  ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) = ( r e. { m e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( m supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } )
47 fveq1 
 |-  ( r = t -> ( r ` a ) = ( t ` a ) )
48 47 eleq2d 
 |-  ( r = t -> ( b e. ( r ` a ) <-> b e. ( t ` a ) ) )
49 48 anbi2d 
 |-  ( r = t -> ( ( a e. { z e. NN | -. 2 || z } /\ b e. ( r ` a ) ) <-> ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) ) )
50 49 opabbidv 
 |-  ( r = t -> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( r ` a ) ) } = { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) } )
51 50 cbvmptv 
 |-  ( r e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( r ` a ) ) } ) = ( t e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) } )
52 46 29 51 3eqtr2i 
 |-  ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) = ( t e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) } )
53 52 fveq1i 
 |-  ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) = ( ( t e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) )
54 53 imaeq2i 
 |-  ( ( a e. { z e. NN | -. 2 || z } , b e. NN0 |-> ( ( 2 ^ b ) x. a ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) ) = ( ( a e. { z e. NN | -. 2 || z } , b e. NN0 |-> ( ( 2 ^ b ) x. a ) ) " ( ( t e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) )
55 44 54 eqtri 
 |-  ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) ) = ( ( a e. { z e. NN | -. 2 || z } , b e. NN0 |-> ( ( 2 ^ b ) x. a ) ) " ( ( t e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) )
56 55 fveq2i 
 |-  ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) ) ) = ( ( _Ind ` NN ) ` ( ( a e. { z e. NN | -. 2 || z } , b e. NN0 |-> ( ( 2 ^ b ) x. a ) ) " ( ( t e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) ) )
57 56 mpteq2i 
 |-  ( q e. ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) |-> ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) ) ) ) = ( q e. ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) |-> ( ( _Ind ` NN ) ` ( ( a e. { z e. NN | -. 2 || z } , b e. NN0 |-> ( ( 2 ^ b ) x. a ) ) " ( ( t e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) ) ) )
58 42 57 eqtri 
 |-  ( o e. ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) |-> ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( o |` { z e. NN | -. 2 || z } ) ) ) ) ) ) = ( q e. ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) |-> ( ( _Ind ` NN ) ` ( ( a e. { z e. NN | -. 2 || z } , b e. NN0 |-> ( ( 2 ^ b ) x. a ) ) " ( ( t e. { s e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( s supp (/) ) e. Fin } |-> { <. a , b >. | ( a e. { z e. NN | -. 2 || z } /\ b e. ( t ` a ) ) } ) ` ( bits o. ( q |` { z e. NN | -. 2 || z } ) ) ) ) ) )
59 eqid 
 |-  ( f e. ( ( NN0 ^m NN ) i^i { h | ( `' h " NN ) e. Fin } ) |-> sum_ k e. NN ( ( f ` k ) x. k ) ) = ( f e. ( ( NN0 ^m NN ) i^i { h | ( `' h " NN ) e. Fin } ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
60 1 2 3 4 8 12 30 34 36 58 59 eulerpartlemn 
 |-  ( ( o e. ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) |-> ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( o |` { z e. NN | -. 2 || z } ) ) ) ) ) ) |` O ) : O -1-1-onto-> D
61 ovex 
 |-  ( NN0 ^m NN ) e. _V
62 61 rabex 
 |-  { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } e. _V
63 62 inex1 
 |-  ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) e. _V
64 63 mptex 
 |-  ( o e. ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) |-> ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( o |` { z e. NN | -. 2 || z } ) ) ) ) ) ) e. _V
65 64 resex 
 |-  ( ( o e. ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) |-> ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( o |` { z e. NN | -. 2 || z } ) ) ) ) ) ) |` O ) e. _V
66 f1oeq1 
 |-  ( g = ( ( o e. ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) |-> ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( o |` { z e. NN | -. 2 || z } ) ) ) ) ) ) |` O ) -> ( g : O -1-1-onto-> D <-> ( ( o e. ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) |-> ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( o |` { z e. NN | -. 2 || z } ) ) ) ) ) ) |` O ) : O -1-1-onto-> D ) )
67 65 66 spcev 
 |-  ( ( ( o e. ( { h e. ( NN0 ^m NN ) | ( `' h " NN ) C_ { z e. NN | -. 2 || z } } i^i { h | ( `' h " NN ) e. Fin } ) |-> ( ( _Ind ` NN ) ` ( ( x e. { z e. NN | -. 2 || z } , y e. NN0 |-> ( ( 2 ^ y ) x. x ) ) " ( ( r e. { r e. ( ( ~P NN0 i^i Fin ) ^m { z e. NN | -. 2 || z } ) | ( r supp (/) ) e. Fin } |-> { <. x , y >. | ( x e. { z e. NN | -. 2 || z } /\ y e. ( r ` x ) ) } ) ` ( bits o. ( o |` { z e. NN | -. 2 || z } ) ) ) ) ) ) |` O ) : O -1-1-onto-> D -> E. g g : O -1-1-onto-> D )
68 bren 
 |-  ( O ~~ D <-> E. g g : O -1-1-onto-> D )
69 hasheni 
 |-  ( O ~~ D -> ( # ` O ) = ( # ` D ) )
70 68 69 sylbir 
 |-  ( E. g g : O -1-1-onto-> D -> ( # ` O ) = ( # ` D ) )
71 60 67 70 mp2b 
 |-  ( # ` O ) = ( # ` D )