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 |
|
fveq1 |
|- ( g = A -> ( g ` n ) = ( A ` n ) ) |
5 |
4
|
breq1d |
|- ( g = A -> ( ( g ` n ) <_ 1 <-> ( A ` n ) <_ 1 ) ) |
6 |
5
|
ralbidv |
|- ( g = A -> ( A. n e. NN ( g ` n ) <_ 1 <-> A. n e. NN ( A ` n ) <_ 1 ) ) |
7 |
6 3
|
elrab2 |
|- ( A e. D <-> ( A e. P /\ A. n e. NN ( A ` n ) <_ 1 ) ) |
8 |
|
2z |
|- 2 e. ZZ |
9 |
|
fzoval |
|- ( 2 e. ZZ -> ( 0 ..^ 2 ) = ( 0 ... ( 2 - 1 ) ) ) |
10 |
8 9
|
ax-mp |
|- ( 0 ..^ 2 ) = ( 0 ... ( 2 - 1 ) ) |
11 |
|
fzo0to2pr |
|- ( 0 ..^ 2 ) = { 0 , 1 } |
12 |
|
2m1e1 |
|- ( 2 - 1 ) = 1 |
13 |
12
|
oveq2i |
|- ( 0 ... ( 2 - 1 ) ) = ( 0 ... 1 ) |
14 |
10 11 13
|
3eqtr3i |
|- { 0 , 1 } = ( 0 ... 1 ) |
15 |
14
|
eleq2i |
|- ( ( A ` n ) e. { 0 , 1 } <-> ( A ` n ) e. ( 0 ... 1 ) ) |
16 |
1
|
eulerpartleme |
|- ( A e. P <-> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) ) |
17 |
16
|
simp1bi |
|- ( A e. P -> A : NN --> NN0 ) |
18 |
17
|
ffvelrnda |
|- ( ( A e. P /\ n e. NN ) -> ( A ` n ) e. NN0 ) |
19 |
|
1nn0 |
|- 1 e. NN0 |
20 |
|
elfz2nn0 |
|- ( ( A ` n ) e. ( 0 ... 1 ) <-> ( ( A ` n ) e. NN0 /\ 1 e. NN0 /\ ( A ` n ) <_ 1 ) ) |
21 |
|
df-3an |
|- ( ( ( A ` n ) e. NN0 /\ 1 e. NN0 /\ ( A ` n ) <_ 1 ) <-> ( ( ( A ` n ) e. NN0 /\ 1 e. NN0 ) /\ ( A ` n ) <_ 1 ) ) |
22 |
20 21
|
bitri |
|- ( ( A ` n ) e. ( 0 ... 1 ) <-> ( ( ( A ` n ) e. NN0 /\ 1 e. NN0 ) /\ ( A ` n ) <_ 1 ) ) |
23 |
22
|
baib |
|- ( ( ( A ` n ) e. NN0 /\ 1 e. NN0 ) -> ( ( A ` n ) e. ( 0 ... 1 ) <-> ( A ` n ) <_ 1 ) ) |
24 |
18 19 23
|
sylancl |
|- ( ( A e. P /\ n e. NN ) -> ( ( A ` n ) e. ( 0 ... 1 ) <-> ( A ` n ) <_ 1 ) ) |
25 |
15 24
|
bitr2id |
|- ( ( A e. P /\ n e. NN ) -> ( ( A ` n ) <_ 1 <-> ( A ` n ) e. { 0 , 1 } ) ) |
26 |
25
|
ralbidva |
|- ( A e. P -> ( A. n e. NN ( A ` n ) <_ 1 <-> A. n e. NN ( A ` n ) e. { 0 , 1 } ) ) |
27 |
17
|
ffund |
|- ( A e. P -> Fun A ) |
28 |
|
fdm |
|- ( A : NN --> NN0 -> dom A = NN ) |
29 |
|
eqimss2 |
|- ( dom A = NN -> NN C_ dom A ) |
30 |
17 28 29
|
3syl |
|- ( A e. P -> NN C_ dom A ) |
31 |
|
funimass4 |
|- ( ( Fun A /\ NN C_ dom A ) -> ( ( A " NN ) C_ { 0 , 1 } <-> A. n e. NN ( A ` n ) e. { 0 , 1 } ) ) |
32 |
27 30 31
|
syl2anc |
|- ( A e. P -> ( ( A " NN ) C_ { 0 , 1 } <-> A. n e. NN ( A ` n ) e. { 0 , 1 } ) ) |
33 |
26 32
|
bitr4d |
|- ( A e. P -> ( A. n e. NN ( A ` n ) <_ 1 <-> ( A " NN ) C_ { 0 , 1 } ) ) |
34 |
33
|
pm5.32i |
|- ( ( A e. P /\ A. n e. NN ( A ` n ) <_ 1 ) <-> ( A e. P /\ ( A " NN ) C_ { 0 , 1 } ) ) |
35 |
7 34
|
bitri |
|- ( A e. D <-> ( A e. P /\ ( A " NN ) C_ { 0 , 1 } ) ) |