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