Metamath Proof Explorer

Theorem eulerpartlemsv2

Description: Lemma for eulerpart . Value of the sum of a finite partition A (Contributed by Thierry Arnoux, 19-Aug-2018)

Ref Expression
Hypotheses eulerpartlems.r 
|- R = { f | ( `' f " NN ) e. Fin }
eulerpartlems.s 
|- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
Assertion eulerpartlemsv2 
|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) )

Proof

Step Hyp Ref Expression
1 eulerpartlems.r 
 |-  R = { f | ( `' f " NN ) e. Fin }
2 eulerpartlems.s 
 |-  S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
3 1 2 eulerpartlemsv1 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. NN ( ( A ` k ) x. k ) )
4 cnvimass 
 |-  ( `' A " NN ) C_ dom A
5 1 2 eulerpartlemelr 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) )
6 5 simpld 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> A : NN --> NN0 )
7 4 6 fssdm 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( `' A " NN ) C_ NN )
8 6 adantr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( `' A " NN ) ) -> A : NN --> NN0 )
9 7 sselda 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( `' A " NN ) ) -> k e. NN )
10 8 9 ffvelrnd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( `' A " NN ) ) -> ( A ` k ) e. NN0 )
11 9 nnnn0d 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( `' A " NN ) ) -> k e. NN0 )
12 10 11 nn0mulcld 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( `' A " NN ) ) -> ( ( A ` k ) x. k ) e. NN0 )
13 12 nn0cnd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( `' A " NN ) ) -> ( ( A ` k ) x. k ) e. CC )
14 simpr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> k e. ( NN \ ( `' A " NN ) ) )
15 14 eldifad 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> k e. NN )
16 14 eldifbd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> -. k e. ( `' A " NN ) )
17 6 adantr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> A : NN --> NN0 )
18 ffn 
 |-  ( A : NN --> NN0 -> A Fn NN )
19 elpreima 
 |-  ( A Fn NN -> ( k e. ( `' A " NN ) <-> ( k e. NN /\ ( A ` k ) e. NN ) ) )
20 17 18 19 3syl 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( k e. ( `' A " NN ) <-> ( k e. NN /\ ( A ` k ) e. NN ) ) )
21 16 20 mtbid 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> -. ( k e. NN /\ ( A ` k ) e. NN ) )
22 imnan 
 |-  ( ( k e. NN -> -. ( A ` k ) e. NN ) <-> -. ( k e. NN /\ ( A ` k ) e. NN ) )
23 21 22 sylibr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( k e. NN -> -. ( A ` k ) e. NN ) )
24 15 23 mpd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> -. ( A ` k ) e. NN )
25 17 15 ffvelrnd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( A ` k ) e. NN0 )
26 elnn0 
 |-  ( ( A ` k ) e. NN0 <-> ( ( A ` k ) e. NN \/ ( A ` k ) = 0 ) )
27 25 26 sylib 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( ( A ` k ) e. NN \/ ( A ` k ) = 0 ) )
28 orel1 
 |-  ( -. ( A ` k ) e. NN -> ( ( ( A ` k ) e. NN \/ ( A ` k ) = 0 ) -> ( A ` k ) = 0 ) )
29 24 27 28 sylc 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( A ` k ) = 0 )
30 29 oveq1d 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( ( A ` k ) x. k ) = ( 0 x. k ) )
31 15 nncnd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> k e. CC )
32 31 mul02d 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( 0 x. k ) = 0 )
33 30 32 eqtrd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( `' A " NN ) ) ) -> ( ( A ` k ) x. k ) = 0 )
34 nnuz 
 |-  NN = ( ZZ>= ` 1 )
35 34 eqimssi 
 |-  NN C_ ( ZZ>= ` 1 )
36 35 a1i 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> NN C_ ( ZZ>= ` 1 ) )
37 7 13 33 36 sumss 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) = sum_ k e. NN ( ( A ` k ) x. k ) )
38 3 37 eqtr4d 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. ( `' A " NN ) ( ( A ` k ) x. k ) )