Metamath Proof Explorer

Theorem eulerpartlemt0

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 19-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 }
Assertion eulerpartlemt0 
|- ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )

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 cnveq 
 |-  ( f = A -> `' f = `' A )
11 10 imaeq1d 
 |-  ( f = A -> ( `' f " NN ) = ( `' A " NN ) )
12 11 sseq1d 
 |-  ( f = A -> ( ( `' f " NN ) C_ J <-> ( `' A " NN ) C_ J ) )
13 12 9 elrab2 
 |-  ( A e. T <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) C_ J ) )
14 11 eleq1d 
 |-  ( f = A -> ( ( `' f " NN ) e. Fin <-> ( `' A " NN ) e. Fin ) )
15 14 8 elab4g 
 |-  ( A e. R <-> ( A e. _V /\ ( `' A " NN ) e. Fin ) )
16 13 15 anbi12i 
 |-  ( ( A e. T /\ A e. R ) <-> ( ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) C_ J ) /\ ( A e. _V /\ ( `' A " NN ) e. Fin ) ) )
17 elin 
 |-  ( A e. ( T i^i R ) <-> ( A e. T /\ A e. R ) )
18 elex 
 |-  ( A e. ( NN0 ^m NN ) -> A e. _V )
19 18 pm4.71i 
 |-  ( A e. ( NN0 ^m NN ) <-> ( A e. ( NN0 ^m NN ) /\ A e. _V ) )
20 19 anbi1i 
 |-  ( ( A e. ( NN0 ^m NN ) /\ ( ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) ) <-> ( ( A e. ( NN0 ^m NN ) /\ A e. _V ) /\ ( ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) ) )
21 3anass 
 |-  ( ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) <-> ( A e. ( NN0 ^m NN ) /\ ( ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) ) )
22 an42 
 |-  ( ( ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) C_ J ) /\ ( A e. _V /\ ( `' A " NN ) e. Fin ) ) <-> ( ( A e. ( NN0 ^m NN ) /\ A e. _V ) /\ ( ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) ) )
23 20 21 22 3bitr4i 
 |-  ( ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) <-> ( ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) C_ J ) /\ ( A e. _V /\ ( `' A " NN ) e. Fin ) ) )
24 16 17 23 3bitr4i 
 |-  ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )