Metamath Proof Explorer

Theorem eulerpartlemr

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 13-Nov-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 ) ) ) ) ) )
Assertion eulerpartlemr 
|- O = ( ( T i^i R ) i^i P )

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 elin 
 |-  ( h e. ( T i^i R ) <-> ( h e. T /\ h e. R ) )
12 11 anbi1i 
 |-  ( ( h e. ( T i^i R ) /\ h e. P ) <-> ( ( h e. T /\ h e. R ) /\ h e. P ) )
13 elin 
 |-  ( h e. ( ( T i^i R ) i^i P ) <-> ( h e. ( T i^i R ) /\ h e. P ) )
14 1 2 3 eulerpartlemo 
 |-  ( h e. O <-> ( h e. P /\ A. n e. ( `' h " NN ) -. 2 || n ) )
15 cnveq 
 |-  ( f = h -> `' f = `' h )
16 15 imaeq1d 
 |-  ( f = h -> ( `' f " NN ) = ( `' h " NN ) )
17 16 eleq1d 
 |-  ( f = h -> ( ( `' f " NN ) e. Fin <-> ( `' h " NN ) e. Fin ) )
18 fveq1 
 |-  ( f = h -> ( f ` k ) = ( h ` k ) )
19 18 oveq1d 
 |-  ( f = h -> ( ( f ` k ) x. k ) = ( ( h ` k ) x. k ) )
20 19 sumeq2sdv 
 |-  ( f = h -> sum_ k e. NN ( ( f ` k ) x. k ) = sum_ k e. NN ( ( h ` k ) x. k ) )
21 20 eqeq1d 
 |-  ( f = h -> ( sum_ k e. NN ( ( f ` k ) x. k ) = N <-> sum_ k e. NN ( ( h ` k ) x. k ) = N ) )
22 17 21 anbi12d 
 |-  ( f = h -> ( ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) <-> ( ( `' h " NN ) e. Fin /\ sum_ k e. NN ( ( h ` k ) x. k ) = N ) ) )
23 22 1 elrab2 
 |-  ( h e. P <-> ( h e. ( NN0 ^m NN ) /\ ( ( `' h " NN ) e. Fin /\ sum_ k e. NN ( ( h ` k ) x. k ) = N ) ) )
24 23 simplbi 
 |-  ( h e. P -> h e. ( NN0 ^m NN ) )
25 cnvimass 
 |-  ( `' h " NN ) C_ dom h
26 nn0ex 
 |-  NN0 e. _V
27 nnex 
 |-  NN e. _V
28 26 27 elmap 
 |-  ( h e. ( NN0 ^m NN ) <-> h : NN --> NN0 )
29 fdm 
 |-  ( h : NN --> NN0 -> dom h = NN )
30 28 29 sylbi 
 |-  ( h e. ( NN0 ^m NN ) -> dom h = NN )
31 25 30 sseqtrid 
 |-  ( h e. ( NN0 ^m NN ) -> ( `' h " NN ) C_ NN )
32 24 31 syl 
 |-  ( h e. P -> ( `' h " NN ) C_ NN )
33 32 sselda 
 |-  ( ( h e. P /\ n e. ( `' h " NN ) ) -> n e. NN )
34 33 ralrimiva 
 |-  ( h e. P -> A. n e. ( `' h " NN ) n e. NN )
35 34 biantrurd 
 |-  ( h e. P -> ( A. n e. ( `' h " NN ) -. 2 || n <-> ( A. n e. ( `' h " NN ) n e. NN /\ A. n e. ( `' h " NN ) -. 2 || n ) ) )
36 24 biantrurd 
 |-  ( h e. P -> ( ( A. n e. ( `' h " NN ) n e. NN /\ A. n e. ( `' h " NN ) -. 2 || n ) <-> ( h e. ( NN0 ^m NN ) /\ ( A. n e. ( `' h " NN ) n e. NN /\ A. n e. ( `' h " NN ) -. 2 || n ) ) ) )
37 23 simprbi 
 |-  ( h e. P -> ( ( `' h " NN ) e. Fin /\ sum_ k e. NN ( ( h ` k ) x. k ) = N ) )
38 37 simpld 
 |-  ( h e. P -> ( `' h " NN ) e. Fin )
39 38 biantrud 
 |-  ( h e. P -> ( ( h e. ( NN0 ^m NN ) /\ ( A. n e. ( `' h " NN ) n e. NN /\ A. n e. ( `' h " NN ) -. 2 || n ) ) <-> ( ( h e. ( NN0 ^m NN ) /\ ( A. n e. ( `' h " NN ) n e. NN /\ A. n e. ( `' h " NN ) -. 2 || n ) ) /\ ( `' h " NN ) e. Fin ) ) )
40 35 36 39 3bitrd 
 |-  ( h e. P -> ( A. n e. ( `' h " NN ) -. 2 || n <-> ( ( h e. ( NN0 ^m NN ) /\ ( A. n e. ( `' h " NN ) n e. NN /\ A. n e. ( `' h " NN ) -. 2 || n ) ) /\ ( `' h " NN ) e. Fin ) ) )
41 dfss3 
 |-  ( ( `' h " NN ) C_ J <-> A. n e. ( `' h " NN ) n e. J )
42 breq2 
 |-  ( z = n -> ( 2 || z <-> 2 || n ) )
43 42 notbid 
 |-  ( z = n -> ( -. 2 || z <-> -. 2 || n ) )
44 43 4 elrab2 
 |-  ( n e. J <-> ( n e. NN /\ -. 2 || n ) )
45 44 ralbii 
 |-  ( A. n e. ( `' h " NN ) n e. J <-> A. n e. ( `' h " NN ) ( n e. NN /\ -. 2 || n ) )
46 r19.26 
 |-  ( A. n e. ( `' h " NN ) ( n e. NN /\ -. 2 || n ) <-> ( A. n e. ( `' h " NN ) n e. NN /\ A. n e. ( `' h " NN ) -. 2 || n ) )
47 41 45 46 3bitri 
 |-  ( ( `' h " NN ) C_ J <-> ( A. n e. ( `' h " NN ) n e. NN /\ A. n e. ( `' h " NN ) -. 2 || n ) )
48 47 anbi2i 
 |-  ( ( h e. ( NN0 ^m NN ) /\ ( `' h " NN ) C_ J ) <-> ( h e. ( NN0 ^m NN ) /\ ( A. n e. ( `' h " NN ) n e. NN /\ A. n e. ( `' h " NN ) -. 2 || n ) ) )
49 48 anbi1i 
 |-  ( ( ( h e. ( NN0 ^m NN ) /\ ( `' h " NN ) C_ J ) /\ ( `' h " NN ) e. Fin ) <-> ( ( h e. ( NN0 ^m NN ) /\ ( A. n e. ( `' h " NN ) n e. NN /\ A. n e. ( `' h " NN ) -. 2 || n ) ) /\ ( `' h " NN ) e. Fin ) )
50 40 49 bitr4di 
 |-  ( h e. P -> ( A. n e. ( `' h " NN ) -. 2 || n <-> ( ( h e. ( NN0 ^m NN ) /\ ( `' h " NN ) C_ J ) /\ ( `' h " NN ) e. Fin ) ) )
51 16 sseq1d 
 |-  ( f = h -> ( ( `' f " NN ) C_ J <-> ( `' h " NN ) C_ J ) )
52 51 9 elrab2 
 |-  ( h e. T <-> ( h e. ( NN0 ^m NN ) /\ ( `' h " NN ) C_ J ) )
53 vex 
 |-  h e. _V
54 53 17 8 elab2 
 |-  ( h e. R <-> ( `' h " NN ) e. Fin )
55 52 54 anbi12i 
 |-  ( ( h e. T /\ h e. R ) <-> ( ( h e. ( NN0 ^m NN ) /\ ( `' h " NN ) C_ J ) /\ ( `' h " NN ) e. Fin ) )
56 50 55 bitr4di 
 |-  ( h e. P -> ( A. n e. ( `' h " NN ) -. 2 || n <-> ( h e. T /\ h e. R ) ) )
57 56 pm5.32i 
 |-  ( ( h e. P /\ A. n e. ( `' h " NN ) -. 2 || n ) <-> ( h e. P /\ ( h e. T /\ h e. R ) ) )
58 ancom 
 |-  ( ( h e. P /\ ( h e. T /\ h e. R ) ) <-> ( ( h e. T /\ h e. R ) /\ h e. P ) )
59 14 57 58 3bitri 
 |-  ( h e. O <-> ( ( h e. T /\ h e. R ) /\ h e. P ) )
60 12 13 59 3bitr4ri 
 |-  ( h e. O <-> h e. ( ( T i^i R ) i^i P ) )
61 60 eqriv 
 |-  O = ( ( T i^i R ) i^i P )