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 ⊒ ( π‘š = 1 β†’ 𝐡 = 𝐢 )
musumsum.2 ⊒ ( πœ‘ β†’ 𝐴 ∈ Fin )
musumsum.3 ⊒ ( πœ‘ β†’ 𝐴 βŠ† β„• )
musumsum.4 ⊒ ( πœ‘ β†’ 1 ∈ 𝐴 )
musumsum.5 ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) β†’ 𝐡 ∈ β„‚ )
Assertion musumsum ( πœ‘ β†’ Ξ£ π‘š ∈ 𝐴 Ξ£ π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } ( ( ΞΌ β€˜ π‘˜ ) Β· 𝐡 ) = 𝐢 )

Proof

Step Hyp Ref Expression
1 musumsum.1 ⊒ ( π‘š = 1 β†’ 𝐡 = 𝐢 )
2 musumsum.2 ⊒ ( πœ‘ β†’ 𝐴 ∈ Fin )
3 musumsum.3 ⊒ ( πœ‘ β†’ 𝐴 βŠ† β„• )
4 musumsum.4 ⊒ ( πœ‘ β†’ 1 ∈ 𝐴 )
5 musumsum.5 ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) β†’ 𝐡 ∈ β„‚ )
6 3 sselda ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) β†’ π‘š ∈ β„• )
7 musum ⊒ ( π‘š ∈ β„• β†’ Ξ£ π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } ( ΞΌ β€˜ π‘˜ ) = if ( π‘š = 1 , 1 , 0 ) )
8 6 7 syl ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) β†’ Ξ£ π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } ( ΞΌ β€˜ π‘˜ ) = if ( π‘š = 1 , 1 , 0 ) )
9 8 oveq1d ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) β†’ ( Ξ£ π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } ( ΞΌ β€˜ π‘˜ ) Β· 𝐡 ) = ( if ( π‘š = 1 , 1 , 0 ) Β· 𝐡 ) )
10 fzfid ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) β†’ ( 1 ... π‘š ) ∈ Fin )
11 dvdsssfz1 ⊒ ( π‘š ∈ β„• β†’ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } βŠ† ( 1 ... π‘š ) )
12 6 11 syl ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) β†’ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } βŠ† ( 1 ... π‘š ) )
13 10 12 ssfid ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) β†’ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } ∈ Fin )
14 elrabi ⊒ ( π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } β†’ π‘˜ ∈ β„• )
15 mucl ⊒ ( π‘˜ ∈ β„• β†’ ( ΞΌ β€˜ π‘˜ ) ∈ β„€ )
16 14 15 syl ⊒ ( π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } β†’ ( ΞΌ β€˜ π‘˜ ) ∈ β„€ )
17 16 zcnd ⊒ ( π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } β†’ ( ΞΌ β€˜ π‘˜ ) ∈ β„‚ )
18 17 adantl ⊒ ( ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) ∧ π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } ) β†’ ( ΞΌ β€˜ π‘˜ ) ∈ β„‚ )
19 13 5 18 fsummulc1 ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) β†’ ( Ξ£ π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } ( ΞΌ β€˜ π‘˜ ) Β· 𝐡 ) = Ξ£ π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } ( ( ΞΌ β€˜ π‘˜ ) Β· 𝐡 ) )
20 ovif ⊒ ( if ( π‘š = 1 , 1 , 0 ) Β· 𝐡 ) = if ( π‘š = 1 , ( 1 Β· 𝐡 ) , ( 0 Β· 𝐡 ) )
21 velsn ⊒ ( π‘š ∈ { 1 } ↔ π‘š = 1 )
22 21 bicomi ⊒ ( π‘š = 1 ↔ π‘š ∈ { 1 } )
23 22 a1i ⊒ ( 𝐡 ∈ β„‚ β†’ ( π‘š = 1 ↔ π‘š ∈ { 1 } ) )
24 mullid ⊒ ( 𝐡 ∈ β„‚ β†’ ( 1 Β· 𝐡 ) = 𝐡 )
25 mul02 ⊒ ( 𝐡 ∈ β„‚ β†’ ( 0 Β· 𝐡 ) = 0 )
26 23 24 25 ifbieq12d ⊒ ( 𝐡 ∈ β„‚ β†’ if ( π‘š = 1 , ( 1 Β· 𝐡 ) , ( 0 Β· 𝐡 ) ) = if ( π‘š ∈ { 1 } , 𝐡 , 0 ) )
27 5 26 syl ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) β†’ if ( π‘š = 1 , ( 1 Β· 𝐡 ) , ( 0 Β· 𝐡 ) ) = if ( π‘š ∈ { 1 } , 𝐡 , 0 ) )
28 20 27 eqtrid ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) β†’ ( if ( π‘š = 1 , 1 , 0 ) Β· 𝐡 ) = if ( π‘š ∈ { 1 } , 𝐡 , 0 ) )
29 9 19 28 3eqtr3d ⊒ ( ( πœ‘ ∧ π‘š ∈ 𝐴 ) β†’ Ξ£ π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } ( ( ΞΌ β€˜ π‘˜ ) Β· 𝐡 ) = if ( π‘š ∈ { 1 } , 𝐡 , 0 ) )
30 29 sumeq2dv ⊒ ( πœ‘ β†’ Ξ£ π‘š ∈ 𝐴 Ξ£ π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } ( ( ΞΌ β€˜ π‘˜ ) Β· 𝐡 ) = Ξ£ π‘š ∈ 𝐴 if ( π‘š ∈ { 1 } , 𝐡 , 0 ) )
31 4 snssd ⊒ ( πœ‘ β†’ { 1 } βŠ† 𝐴 )
32 31 sselda ⊒ ( ( πœ‘ ∧ π‘š ∈ { 1 } ) β†’ π‘š ∈ 𝐴 )
33 32 5 syldan ⊒ ( ( πœ‘ ∧ π‘š ∈ { 1 } ) β†’ 𝐡 ∈ β„‚ )
34 33 ralrimiva ⊒ ( πœ‘ β†’ βˆ€ π‘š ∈ { 1 } 𝐡 ∈ β„‚ )
35 2 olcd ⊒ ( πœ‘ β†’ ( 𝐴 βŠ† ( β„€β‰₯ β€˜ 1 ) ∨ 𝐴 ∈ Fin ) )
36 sumss2 ⊒ ( ( ( { 1 } βŠ† 𝐴 ∧ βˆ€ π‘š ∈ { 1 } 𝐡 ∈ β„‚ ) ∧ ( 𝐴 βŠ† ( β„€β‰₯ β€˜ 1 ) ∨ 𝐴 ∈ Fin ) ) β†’ Ξ£ π‘š ∈ { 1 } 𝐡 = Ξ£ π‘š ∈ 𝐴 if ( π‘š ∈ { 1 } , 𝐡 , 0 ) )
37 31 34 35 36 syl21anc ⊒ ( πœ‘ β†’ Ξ£ π‘š ∈ { 1 } 𝐡 = Ξ£ π‘š ∈ 𝐴 if ( π‘š ∈ { 1 } , 𝐡 , 0 ) )
38 1 eleq1d ⊒ ( π‘š = 1 β†’ ( 𝐡 ∈ β„‚ ↔ 𝐢 ∈ β„‚ ) )
39 5 ralrimiva ⊒ ( πœ‘ β†’ βˆ€ π‘š ∈ 𝐴 𝐡 ∈ β„‚ )
40 38 39 4 rspcdva ⊒ ( πœ‘ β†’ 𝐢 ∈ β„‚ )
41 1 sumsn ⊒ ( ( 1 ∈ 𝐴 ∧ 𝐢 ∈ β„‚ ) β†’ Ξ£ π‘š ∈ { 1 } 𝐡 = 𝐢 )
42 4 40 41 syl2anc ⊒ ( πœ‘ β†’ Ξ£ π‘š ∈ { 1 } 𝐡 = 𝐢 )
43 30 37 42 3eqtr2d ⊒ ( πœ‘ β†’ Ξ£ π‘š ∈ 𝐴 Ξ£ π‘˜ ∈ { 𝑛 ∈ β„• ∣ 𝑛 βˆ₯ π‘š } ( ( ΞΌ β€˜ π‘˜ ) Β· 𝐡 ) = 𝐢 )