Metamath Proof Explorer

Theorem eulerpartlemv

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 19-Aug-2018)

Ref Expression
Hypothesis eulerpart.p 
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
Assertion eulerpartlemv 
|- ( A e. P <-> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) = N ) )

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 1 eulerpartleme 
 |-  ( A e. P <-> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) )
3 cnvimass 
 |-  ( `' A " NN ) C_ dom A
4 fdm 
 |-  ( A : NN --> NN0 -> dom A = NN )
5 3 4 sseqtrid 
 |-  ( A : NN --> NN0 -> ( `' A " NN ) C_ NN )
6 simpl 
 |-  ( ( A : NN --> NN0 /\ k e. ( `' A " NN ) ) -> A : NN --> NN0 )
7 5 sselda 
 |-  ( ( A : NN --> NN0 /\ k e. ( `' A " NN ) ) -> k e. NN )
8 6 7 ffvelrnd 
 |-  ( ( A : NN --> NN0 /\ k e. ( `' A " NN ) ) -> ( A ` k ) e. NN0 )
9 7 nnnn0d 
 |-  ( ( A : NN --> NN0 /\ k e. ( `' A " NN ) ) -> k e. NN0 )
10 8 9 nn0mulcld 
 |-  ( ( A : NN --> NN0 /\ k e. ( `' A " NN ) ) -> ( ( A ` k ) x. k ) e. NN0 )
11 10 nn0cnd 
 |-  ( ( A : NN --> NN0 /\ k e. ( `' A " NN ) ) -> ( ( A ` k ) x. k ) e. CC )
12 simpr 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> k e. ( NN \ ( `' A " NN ) ) )
13 12 eldifad 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> k e. NN )
14 12 eldifbd 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> -. k e. ( `' A " NN ) )
15 simpl 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> A : NN --> NN0 )
16 ffn 
 |-  ( A : NN --> NN0 -> A Fn NN )
17 elpreima 
 |-  ( A Fn NN -> ( k e. ( `' A " NN ) <-> ( k e. NN /\ ( A ` k ) e. NN ) ) )
18 15 16 17 3syl 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( k e. ( `' A " NN ) <-> ( k e. NN /\ ( A ` k ) e. NN ) ) )
19 14 18 mtbid 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> -. ( k e. NN /\ ( A ` k ) e. NN ) )
20 imnan 
 |-  ( ( k e. NN -> -. ( A ` k ) e. NN ) <-> -. ( k e. NN /\ ( A ` k ) e. NN ) )
21 19 20 sylibr 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( k e. NN -> -. ( A ` k ) e. NN ) )
22 13 21 mpd 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> -. ( A ` k ) e. NN )
23 15 13 ffvelrnd 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( A ` k ) e. NN0 )
24 elnn0 
 |-  ( ( A ` k ) e. NN0 <-> ( ( A ` k ) e. NN \/ ( A ` k ) = 0 ) )
25 23 24 sylib 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( ( A ` k ) e. NN \/ ( A ` k ) = 0 ) )
26 orel1 
 |-  ( -. ( A ` k ) e. NN -> ( ( ( A ` k ) e. NN \/ ( A ` k ) = 0 ) -> ( A ` k ) = 0 ) )
27 22 25 26 sylc 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( A ` k ) = 0 )
28 27 oveq1d 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( ( A ` k ) x. k ) = ( 0 x. k ) )
29 13 nncnd 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> k e. CC )
30 29 mul02d 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( 0 x. k ) = 0 )
31 28 30 eqtrd 
 |-  ( ( A : NN --> NN0 /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( ( A ` k ) x. k ) = 0 )
32 nnuz 
 |-  NN = ( ZZ>= ` 1 )
33 32 eqimssi 
 |-  NN C_ ( ZZ>= ` 1 )
34 33 a1i 
 |-  ( A : NN --> NN0 -> NN C_ ( ZZ>= ` 1 ) )
35 5 11 31 34 sumss 
 |-  ( A : NN --> NN0 -> sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) = sum_ k e. NN ( ( A ` k ) x. k ) )
36 35 eqcomd 
 |-  ( A : NN --> NN0 -> sum_ k e. NN ( ( A ` k ) x. k ) = sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) )
37 36 adantr 
 |-  ( ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) -> sum_ k e. NN ( ( A ` k ) x. k ) = sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) )
38 37 eqeq1d 
 |-  ( ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) -> ( sum_ k e. NN ( ( A ` k ) x. k ) = N <-> sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) = N ) )
39 38 pm5.32i 
 |-  ( ( ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) <-> ( ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) /\ sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) = N ) )
40 df-3an 
 |-  ( ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) <-> ( ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) )
41 df-3an 
 |-  ( ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) = N ) <-> ( ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) /\ sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) = N ) )
42 39 40 41 3bitr4i 
 |-  ( ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) <-> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) = N ) )
43 2 42 bitri 
 |-  ( A e. P <-> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) = N ) )