Metamath Proof Explorer

Theorem eulerpartlemsv3

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 eulerpartlemsv3 
|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. ( 1 ... ( S ` A ) ) ( ( 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 fzssuz 
 |-  ( 1 ... ( S ` A ) ) C_ ( ZZ>= ` 1 )
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 4 5 sseqtrri 
 |-  ( 1 ... ( S ` A ) ) C_ NN
7 6 a1i 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( 1 ... ( S ` A ) ) C_ NN )
8 1 2 eulerpartlemelr 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) )
9 8 simpld 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> A : NN --> NN0 )
10 9 adantr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> A : NN --> NN0 )
11 7 sselda 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> k e. NN )
12 10 11 ffvelcdmd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> ( A ` k ) e. NN0 )
13 12 nn0cnd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> ( A ` k ) e. CC )
14 11 nncnd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> k e. CC )
15 13 14 mulcld 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> ( ( A ` k ) x. k ) e. CC )
16 1 2 eulerpartlems 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ) -> ( A ` t ) = 0 )
17 16 ralrimiva 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> A. t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ( A ` t ) = 0 )
18 fveqeq2 
 |-  ( k = t -> ( ( A ` k ) = 0 <-> ( A ` t ) = 0 ) )
19 18 cbvralvw 
 |-  ( A. k e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ( A ` k ) = 0 <-> A. t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ( A ` t ) = 0 )
20 17 19 sylibr 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> A. k e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ( A ` k ) = 0 )
21 1 2 eulerpartlemsf 
 |-  S : ( ( NN0 ^m NN ) i^i R ) --> NN0
22 21 ffvelcdmi 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) e. NN0 )
23 nndiffz1 
 |-  ( ( S ` A ) e. NN0 -> ( NN \ ( 1 ... ( S ` A ) ) ) = ( ZZ>= ` ( ( S ` A ) + 1 ) ) )
24 22 23 syl 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( NN \ ( 1 ... ( S ` A ) ) ) = ( ZZ>= ` ( ( S ` A ) + 1 ) ) )
25 20 24 raleqtrrdv 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> A. k e. ( NN \ ( 1 ... ( S ` A ) ) ) ( A ` k ) = 0 )
26 25 r19.21bi 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( A ` k ) = 0 )
27 26 oveq1d 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( ( A ` k ) x. k ) = ( 0 x. k ) )
28 simpr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> k e. ( NN \ ( 1 ... ( S ` A ) ) ) )
29 28 eldifad 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> k e. NN )
30 29 nncnd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> k e. CC )
31 30 mul02d 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( 0 x. k ) = 0 )
32 27 31 eqtrd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( ( A ` k ) x. k ) = 0 )
33 5 eqimssi 
 |-  NN C_ ( ZZ>= ` 1 )
34 33 a1i 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> NN C_ ( ZZ>= ` 1 ) )
35 7 15 32 34 sumss 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) = sum_ k e. NN ( ( A ` k ) x. k ) )
36 3 35 eqtr4d 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) )