Metamath Proof Explorer

Theorem eulerpartlemf

Description: Lemma for eulerpart : Odd partitions are zero for even numbers. (Contributed by Thierry Arnoux, 9-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 eulerpartlemf 
|- ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) -> ( A ` t ) = 0 )

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 eldif 
 |-  ( t e. ( NN \ J ) <-> ( t e. NN /\ -. t e. J ) )
11 breq2 
 |-  ( z = t -> ( 2 || z <-> 2 || t ) )
12 11 notbid 
 |-  ( z = t -> ( -. 2 || z <-> -. 2 || t ) )
13 12 4 elrab2 
 |-  ( t e. J <-> ( t e. NN /\ -. 2 || t ) )
14 13 simplbi2 
 |-  ( t e. NN -> ( -. 2 || t -> t e. J ) )
15 14 con1d 
 |-  ( t e. NN -> ( -. t e. J -> 2 || t ) )
16 15 imp 
 |-  ( ( t e. NN /\ -. t e. J ) -> 2 || t )
17 10 16 sylbi 
 |-  ( t e. ( NN \ J ) -> 2 || t )
18 17 adantl 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) -> 2 || t )
19 18 adantr 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) /\ ( A ` t ) e. NN ) -> 2 || t )
20 simpll 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) /\ ( A ` t ) e. NN ) -> A e. ( T i^i R ) )
21 eldifi 
 |-  ( t e. ( NN \ J ) -> t e. NN )
22 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 ) )
23 22 simp1bi 
 |-  ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) )
24 elmapi 
 |-  ( A e. ( NN0 ^m NN ) -> A : NN --> NN0 )
25 23 24 syl 
 |-  ( A e. ( T i^i R ) -> A : NN --> NN0 )
26 ffn 
 |-  ( A : NN --> NN0 -> A Fn NN )
27 elpreima 
 |-  ( A Fn NN -> ( t e. ( `' A " NN ) <-> ( t e. NN /\ ( A ` t ) e. NN ) ) )
28 25 26 27 3syl 
 |-  ( A e. ( T i^i R ) -> ( t e. ( `' A " NN ) <-> ( t e. NN /\ ( A ` t ) e. NN ) ) )
29 28 baibd 
 |-  ( ( A e. ( T i^i R ) /\ t e. NN ) -> ( t e. ( `' A " NN ) <-> ( A ` t ) e. NN ) )
30 21 29 sylan2 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) -> ( t e. ( `' A " NN ) <-> ( A ` t ) e. NN ) )
31 30 biimpar 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) /\ ( A ` t ) e. NN ) -> t e. ( `' A " NN ) )
32 22 simp3bi 
 |-  ( A e. ( T i^i R ) -> ( `' A " NN ) C_ J )
33 32 sselda 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( `' A " NN ) ) -> t e. J )
34 13 simprbi 
 |-  ( t e. J -> -. 2 || t )
35 33 34 syl 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( `' A " NN ) ) -> -. 2 || t )
36 20 31 35 syl2anc 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) /\ ( A ` t ) e. NN ) -> -. 2 || t )
37 19 36 pm2.65da 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) -> -. ( A ` t ) e. NN )
38 25 adantr 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) -> A : NN --> NN0 )
39 21 adantl 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) -> t e. NN )
40 38 39 ffvelcdmd 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) -> ( A ` t ) e. NN0 )
41 elnn0 
 |-  ( ( A ` t ) e. NN0 <-> ( ( A ` t ) e. NN \/ ( A ` t ) = 0 ) )
42 40 41 sylib 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) -> ( ( A ` t ) e. NN \/ ( A ` t ) = 0 ) )
43 orel1 
 |-  ( -. ( A ` t ) e. NN -> ( ( ( A ` t ) e. NN \/ ( A ` t ) = 0 ) -> ( A ` t ) = 0 ) )
44 37 42 43 sylc 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) -> ( A ` t ) = 0 )