Metamath Proof Explorer

Theorem musumsum

Description: Evaluate a collapsing sum over the Möbius function. (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses musumsum.1 
|- ( m = 1 -> B = C )
musumsum.2 
|- ( ph -> A e. Fin )
musumsum.3 
|- ( ph -> A C_ NN )
musumsum.4 
|- ( ph -> 1 e. A )
musumsum.5 
|- ( ( ph /\ m e. A ) -> B e. CC )
Assertion musumsum 
|- ( ph -> sum_ m e. A sum_ k e. { n e. NN | n || m } ( ( mmu ` k ) x. B ) = C )

Proof

Step Hyp Ref Expression
1 musumsum.1 
 |-  ( m = 1 -> B = C )
2 musumsum.2 
 |-  ( ph -> A e. Fin )
3 musumsum.3 
 |-  ( ph -> A C_ NN )
4 musumsum.4 
 |-  ( ph -> 1 e. A )
5 musumsum.5 
 |-  ( ( ph /\ m e. A ) -> B e. CC )
6 3 sselda 
 |-  ( ( ph /\ m e. A ) -> m e. NN )
7 musum 
 |-  ( m e. NN -> sum_ k e. { n e. NN | n || m } ( mmu ` k ) = if ( m = 1 , 1 , 0 ) )
8 6 7 syl 
 |-  ( ( ph /\ m e. A ) -> sum_ k e. { n e. NN | n || m } ( mmu ` k ) = if ( m = 1 , 1 , 0 ) )
9 8 oveq1d 
 |-  ( ( ph /\ m e. A ) -> ( sum_ k e. { n e. NN | n || m } ( mmu ` k ) x. B ) = ( if ( m = 1 , 1 , 0 ) x. B ) )
10 fzfid 
 |-  ( ( ph /\ m e. A ) -> ( 1 ... m ) e. Fin )
11 dvdsssfz1 
 |-  ( m e. NN -> { n e. NN | n || m } C_ ( 1 ... m ) )
12 6 11 syl 
 |-  ( ( ph /\ m e. A ) -> { n e. NN | n || m } C_ ( 1 ... m ) )
13 10 12 ssfid 
 |-  ( ( ph /\ m e. A ) -> { n e. NN | n || m } e. Fin )
14 elrabi 
 |-  ( k e. { n e. NN | n || m } -> k e. NN )
15 mucl 
 |-  ( k e. NN -> ( mmu ` k ) e. ZZ )
16 14 15 syl 
 |-  ( k e. { n e. NN | n || m } -> ( mmu ` k ) e. ZZ )
17 16 zcnd 
 |-  ( k e. { n e. NN | n || m } -> ( mmu ` k ) e. CC )
18 17 adantl 
 |-  ( ( ( ph /\ m e. A ) /\ k e. { n e. NN | n || m } ) -> ( mmu ` k ) e. CC )
19 13 5 18 fsummulc1 
 |-  ( ( ph /\ m e. A ) -> ( sum_ k e. { n e. NN | n || m } ( mmu ` k ) x. B ) = sum_ k e. { n e. NN | n || m } ( ( mmu ` k ) x. B ) )
20 ovif 
 |-  ( if ( m = 1 , 1 , 0 ) x. B ) = if ( m = 1 , ( 1 x. B ) , ( 0 x. B ) )
21 velsn 
 |-  ( m e. { 1 } <-> m = 1 )
22 21 bicomi 
 |-  ( m = 1 <-> m e. { 1 } )
23 22 a1i 
 |-  ( B e. CC -> ( m = 1 <-> m e. { 1 } ) )
24 mulid2 
 |-  ( B e. CC -> ( 1 x. B ) = B )
25 mul02 
 |-  ( B e. CC -> ( 0 x. B ) = 0 )
26 23 24 25 ifbieq12d 
 |-  ( B e. CC -> if ( m = 1 , ( 1 x. B ) , ( 0 x. B ) ) = if ( m e. { 1 } , B , 0 ) )
27 5 26 syl 
 |-  ( ( ph /\ m e. A ) -> if ( m = 1 , ( 1 x. B ) , ( 0 x. B ) ) = if ( m e. { 1 } , B , 0 ) )
28 20 27 syl5eq 
 |-  ( ( ph /\ m e. A ) -> ( if ( m = 1 , 1 , 0 ) x. B ) = if ( m e. { 1 } , B , 0 ) )
29 9 19 28 3eqtr3d 
 |-  ( ( ph /\ m e. A ) -> sum_ k e. { n e. NN | n || m } ( ( mmu ` k ) x. B ) = if ( m e. { 1 } , B , 0 ) )
30 29 sumeq2dv 
 |-  ( ph -> sum_ m e. A sum_ k e. { n e. NN | n || m } ( ( mmu ` k ) x. B ) = sum_ m e. A if ( m e. { 1 } , B , 0 ) )
31 4 snssd 
 |-  ( ph -> { 1 } C_ A )
32 31 sselda 
 |-  ( ( ph /\ m e. { 1 } ) -> m e. A )
33 32 5 syldan 
 |-  ( ( ph /\ m e. { 1 } ) -> B e. CC )
34 33 ralrimiva 
 |-  ( ph -> A. m e. { 1 } B e. CC )
35 2 olcd 
 |-  ( ph -> ( A C_ ( ZZ>= ` 1 ) \/ A e. Fin ) )
36 sumss2 
 |-  ( ( ( { 1 } C_ A /\ A. m e. { 1 } B e. CC ) /\ ( A C_ ( ZZ>= ` 1 ) \/ A e. Fin ) ) -> sum_ m e. { 1 } B = sum_ m e. A if ( m e. { 1 } , B , 0 ) )
37 31 34 35 36 syl21anc 
 |-  ( ph -> sum_ m e. { 1 } B = sum_ m e. A if ( m e. { 1 } , B , 0 ) )
38 1 eleq1d 
 |-  ( m = 1 -> ( B e. CC <-> C e. CC ) )
39 5 ralrimiva 
 |-  ( ph -> A. m e. A B e. CC )
40 38 39 4 rspcdva 
 |-  ( ph -> C e. CC )
41 1 sumsn 
 |-  ( ( 1 e. A /\ C e. CC ) -> sum_ m e. { 1 } B = C )
42 4 40 41 syl2anc 
 |-  ( ph -> sum_ m e. { 1 } B = C )
43 30 37 42 3eqtr2d 
 |-  ( ph -> sum_ m e. A sum_ k e. { n e. NN | n || m } ( ( mmu ` k ) x. B ) = C )