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 ffvelrnd
 |-  ( ( 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 )