Metamath Proof Explorer


Theorem eulerpartlemd

Description: Lemma for eulerpart : D is the set of distinct part. of N . (Contributed by Thierry Arnoux, 11-Aug-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 }
Assertion eulerpartlemd
|- ( A e. D <-> ( A e. P /\ ( A " NN ) C_ { 0 , 1 } ) )

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