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