Metamath Proof Explorer

Theorem muinv

Description: The MΓΆbius inversion formula. If G ( n ) = sum_ k || n F ( k ) for every n e. NN , then F ( n ) = sum_ k || n mmu ( k ) G ( n / k ) = sum_ k || n mmu ( n / k ) G ( k ) , i.e. the MΓΆbius function is the Dirichlet convolution inverse of the constant function 1 . Theorem 2.9 in ApostolNT p. 32. (Contributed by Mario Carneiro, 2-Jul-2015)

Ref Expression
Hypotheses muinv.1 ⊒ ( πœ‘ β†’ 𝐹 : β„• ⟢ β„‚ )
muinv.2 ⊒ ( πœ‘ β†’ 𝐺 = ( 𝑛 ∈ β„• ↦ Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑛 } ( 𝐹 β€˜ π‘˜ ) ) )
Assertion muinv ( πœ‘ β†’ 𝐹 = ( π‘š ∈ β„• ↦ Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐺 β€˜ ( π‘š / 𝑗 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 muinv.1 ⊒ ( πœ‘ β†’ 𝐹 : β„• ⟢ β„‚ )
2 muinv.2 ⊒ ( πœ‘ β†’ 𝐺 = ( 𝑛 ∈ β„• ↦ Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑛 } ( 𝐹 β€˜ π‘˜ ) ) )
3 1 feqmptd ⊒ ( πœ‘ β†’ 𝐹 = ( π‘š ∈ β„• ↦ ( 𝐹 β€˜ π‘š ) ) )
4 2 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ 𝐺 = ( 𝑛 ∈ β„• ↦ Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑛 } ( 𝐹 β€˜ π‘˜ ) ) )
5 4 fveq1d ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( 𝐺 β€˜ ( π‘š / 𝑗 ) ) = ( ( 𝑛 ∈ β„• ↦ Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑛 } ( 𝐹 β€˜ π‘˜ ) ) β€˜ ( π‘š / 𝑗 ) ) )
6 breq1 ⊒ ( π‘₯ = 𝑗 β†’ ( π‘₯ βˆ₯ π‘š ↔ 𝑗 βˆ₯ π‘š ) )
7 6 elrab ⊒ ( 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ↔ ( 𝑗 ∈ β„• ∧ 𝑗 βˆ₯ π‘š ) )
8 7 simprbi ⊒ ( 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } β†’ 𝑗 βˆ₯ π‘š )
9 8 adantl ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ 𝑗 βˆ₯ π‘š )
10 elrabi ⊒ ( 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } β†’ 𝑗 ∈ β„• )
11 10 adantl ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ 𝑗 ∈ β„• )
12 11 nnzd ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ 𝑗 ∈ β„€ )
13 11 nnne0d ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ 𝑗 β‰  0 )
14 nnz ⊒ ( π‘š ∈ β„• β†’ π‘š ∈ β„€ )
15 14 ad2antlr ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ π‘š ∈ β„€ )
16 dvdsval2 ⊒ ( ( 𝑗 ∈ β„€ ∧ 𝑗 β‰  0 ∧ π‘š ∈ β„€ ) β†’ ( 𝑗 βˆ₯ π‘š ↔ ( π‘š / 𝑗 ) ∈ β„€ ) )
17 12 13 15 16 syl3anc ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( 𝑗 βˆ₯ π‘š ↔ ( π‘š / 𝑗 ) ∈ β„€ ) )
18 9 17 mpbid ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( π‘š / 𝑗 ) ∈ β„€ )
19 nnre ⊒ ( π‘š ∈ β„• β†’ π‘š ∈ ℝ )
20 nngt0 ⊒ ( π‘š ∈ β„• β†’ 0 < π‘š )
21 19 20 jca ⊒ ( π‘š ∈ β„• β†’ ( π‘š ∈ ℝ ∧ 0 < π‘š ) )
22 21 ad2antlr ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( π‘š ∈ ℝ ∧ 0 < π‘š ) )
23 nnre ⊒ ( 𝑗 ∈ β„• β†’ 𝑗 ∈ ℝ )
24 nngt0 ⊒ ( 𝑗 ∈ β„• β†’ 0 < 𝑗 )
25 23 24 jca ⊒ ( 𝑗 ∈ β„• β†’ ( 𝑗 ∈ ℝ ∧ 0 < 𝑗 ) )
26 11 25 syl ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( 𝑗 ∈ ℝ ∧ 0 < 𝑗 ) )
27 divgt0 ⊒ ( ( ( π‘š ∈ ℝ ∧ 0 < π‘š ) ∧ ( 𝑗 ∈ ℝ ∧ 0 < 𝑗 ) ) β†’ 0 < ( π‘š / 𝑗 ) )
28 22 26 27 syl2anc ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ 0 < ( π‘š / 𝑗 ) )
29 elnnz ⊒ ( ( π‘š / 𝑗 ) ∈ β„• ↔ ( ( π‘š / 𝑗 ) ∈ β„€ ∧ 0 < ( π‘š / 𝑗 ) ) )
30 18 28 29 sylanbrc ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( π‘š / 𝑗 ) ∈ β„• )
31 breq2 ⊒ ( 𝑛 = ( π‘š / 𝑗 ) β†’ ( π‘₯ βˆ₯ 𝑛 ↔ π‘₯ βˆ₯ ( π‘š / 𝑗 ) ) )
32 31 rabbidv ⊒ ( 𝑛 = ( π‘š / 𝑗 ) β†’ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑛 } = { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } )
33 32 sumeq1d ⊒ ( 𝑛 = ( π‘š / 𝑗 ) β†’ Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑛 } ( 𝐹 β€˜ π‘˜ ) = Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ( 𝐹 β€˜ π‘˜ ) )
34 eqid ⊒ ( 𝑛 ∈ β„• ↦ Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑛 } ( 𝐹 β€˜ π‘˜ ) ) = ( 𝑛 ∈ β„• ↦ Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑛 } ( 𝐹 β€˜ π‘˜ ) )
35 sumex ⊒ Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ( 𝐹 β€˜ π‘˜ ) ∈ V
36 33 34 35 fvmpt ⊒ ( ( π‘š / 𝑗 ) ∈ β„• β†’ ( ( 𝑛 ∈ β„• ↦ Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑛 } ( 𝐹 β€˜ π‘˜ ) ) β€˜ ( π‘š / 𝑗 ) ) = Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ( 𝐹 β€˜ π‘˜ ) )
37 30 36 syl ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( ( 𝑛 ∈ β„• ↦ Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ 𝑛 } ( 𝐹 β€˜ π‘˜ ) ) β€˜ ( π‘š / 𝑗 ) ) = Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ( 𝐹 β€˜ π‘˜ ) )
38 5 37 eqtrd ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( 𝐺 β€˜ ( π‘š / 𝑗 ) ) = Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ( 𝐹 β€˜ π‘˜ ) )
39 38 oveq2d ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐺 β€˜ ( π‘š / 𝑗 ) ) ) = ( ( ΞΌ β€˜ 𝑗 ) Β· Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ( 𝐹 β€˜ π‘˜ ) ) )
40 fzfid ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( 1 ... ( π‘š / 𝑗 ) ) ∈ Fin )
41 dvdsssfz1 ⊒ ( ( π‘š / 𝑗 ) ∈ β„• β†’ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } βŠ† ( 1 ... ( π‘š / 𝑗 ) ) )
42 30 41 syl ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } βŠ† ( 1 ... ( π‘š / 𝑗 ) ) )
43 40 42 ssfid ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ∈ Fin )
44 mucl ⊒ ( 𝑗 ∈ β„• β†’ ( ΞΌ β€˜ 𝑗 ) ∈ β„€ )
45 11 44 syl ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( ΞΌ β€˜ 𝑗 ) ∈ β„€ )
46 45 zcnd ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( ΞΌ β€˜ 𝑗 ) ∈ β„‚ )
47 1 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ 𝐹 : β„• ⟢ β„‚ )
48 elrabi ⊒ ( π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } β†’ π‘˜ ∈ β„• )
49 ffvelcdm ⊒ ( ( 𝐹 : β„• ⟢ β„‚ ∧ π‘˜ ∈ β„• ) β†’ ( 𝐹 β€˜ π‘˜ ) ∈ β„‚ )
50 47 48 49 syl2an ⊒ ( ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ) β†’ ( 𝐹 β€˜ π‘˜ ) ∈ β„‚ )
51 43 46 50 fsummulc2 ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( ( ΞΌ β€˜ 𝑗 ) Β· Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ( 𝐹 β€˜ π‘˜ ) ) = Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐹 β€˜ π‘˜ ) ) )
52 39 51 eqtrd ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐺 β€˜ ( π‘š / 𝑗 ) ) ) = Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐹 β€˜ π‘˜ ) ) )
53 52 sumeq2dv ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐺 β€˜ ( π‘š / 𝑗 ) ) ) = Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐹 β€˜ π‘˜ ) ) )
54 simpr ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ π‘š ∈ β„• )
55 46 adantrr ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ ( 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ) ) β†’ ( ΞΌ β€˜ 𝑗 ) ∈ β„‚ )
56 50 anasss ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ ( 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ) ) β†’ ( 𝐹 β€˜ π‘˜ ) ∈ β„‚ )
57 55 56 mulcld ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ ( 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ) ) β†’ ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐹 β€˜ π‘˜ ) ) ∈ β„‚ )
58 54 57 fsumdvdsdiag ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / 𝑗 ) } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐹 β€˜ π‘˜ ) ) = Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐹 β€˜ π‘˜ ) ) )
59 ssrab2 ⊒ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } βŠ† β„•
60 dvdsdivcl ⊒ ( ( π‘š ∈ β„• ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( π‘š / π‘˜ ) ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } )
61 60 adantll ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( π‘š / π‘˜ ) ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } )
62 59 61 sselid ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( π‘š / π‘˜ ) ∈ β„• )
63 musum ⊒ ( ( π‘š / π‘˜ ) ∈ β„• β†’ Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ( ΞΌ β€˜ 𝑗 ) = if ( ( π‘š / π‘˜ ) = 1 , 1 , 0 ) )
64 62 63 syl ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ( ΞΌ β€˜ 𝑗 ) = if ( ( π‘š / π‘˜ ) = 1 , 1 , 0 ) )
65 64 oveq1d ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐹 β€˜ π‘˜ ) ) = ( if ( ( π‘š / π‘˜ ) = 1 , 1 , 0 ) Β· ( 𝐹 β€˜ π‘˜ ) ) )
66 fzfid ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( 1 ... ( π‘š / π‘˜ ) ) ∈ Fin )
67 dvdsssfz1 ⊒ ( ( π‘š / π‘˜ ) ∈ β„• β†’ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } βŠ† ( 1 ... ( π‘š / π‘˜ ) ) )
68 62 67 syl ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } βŠ† ( 1 ... ( π‘š / π‘˜ ) ) )
69 66 68 ssfid ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ∈ Fin )
70 1 adantr ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ 𝐹 : β„• ⟢ β„‚ )
71 elrabi ⊒ ( π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } β†’ π‘˜ ∈ β„• )
72 70 71 49 syl2an ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( 𝐹 β€˜ π‘˜ ) ∈ β„‚ )
73 ssrab2 ⊒ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } βŠ† β„•
74 simpr ⊒ ( ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ) β†’ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } )
75 73 74 sselid ⊒ ( ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ) β†’ 𝑗 ∈ β„• )
76 75 44 syl ⊒ ( ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ) β†’ ( ΞΌ β€˜ 𝑗 ) ∈ β„€ )
77 76 zcnd ⊒ ( ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) ∧ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ) β†’ ( ΞΌ β€˜ 𝑗 ) ∈ β„‚ )
78 69 72 77 fsummulc1 ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐹 β€˜ π‘˜ ) ) = Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐹 β€˜ π‘˜ ) ) )
79 ovif ⊒ ( if ( ( π‘š / π‘˜ ) = 1 , 1 , 0 ) Β· ( 𝐹 β€˜ π‘˜ ) ) = if ( ( π‘š / π‘˜ ) = 1 , ( 1 Β· ( 𝐹 β€˜ π‘˜ ) ) , ( 0 Β· ( 𝐹 β€˜ π‘˜ ) ) )
80 nncn ⊒ ( π‘š ∈ β„• β†’ π‘š ∈ β„‚ )
81 80 ad2antlr ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ π‘š ∈ β„‚ )
82 71 adantl ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ π‘˜ ∈ β„• )
83 82 nncnd ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ π‘˜ ∈ β„‚ )
84 1cnd ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ 1 ∈ β„‚ )
85 82 nnne0d ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ π‘˜ β‰  0 )
86 81 83 84 85 divmuld ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( ( π‘š / π‘˜ ) = 1 ↔ ( π‘˜ Β· 1 ) = π‘š ) )
87 83 mulridd ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( π‘˜ Β· 1 ) = π‘˜ )
88 87 eqeq1d ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( ( π‘˜ Β· 1 ) = π‘š ↔ π‘˜ = π‘š ) )
89 86 88 bitrd ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( ( π‘š / π‘˜ ) = 1 ↔ π‘˜ = π‘š ) )
90 72 mullidd ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( 1 Β· ( 𝐹 β€˜ π‘˜ ) ) = ( 𝐹 β€˜ π‘˜ ) )
91 72 mul02d ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( 0 Β· ( 𝐹 β€˜ π‘˜ ) ) = 0 )
92 89 90 91 ifbieq12d ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ if ( ( π‘š / π‘˜ ) = 1 , ( 1 Β· ( 𝐹 β€˜ π‘˜ ) ) , ( 0 Β· ( 𝐹 β€˜ π‘˜ ) ) ) = if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) )
93 79 92 eqtrid ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ ( if ( ( π‘š / π‘˜ ) = 1 , 1 , 0 ) Β· ( 𝐹 β€˜ π‘˜ ) ) = if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) )
94 65 78 93 3eqtr3d ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ) β†’ Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐹 β€˜ π‘˜ ) ) = if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) )
95 94 sumeq2dv ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐹 β€˜ π‘˜ ) ) = Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) )
96 breq1 ⊒ ( π‘₯ = π‘š β†’ ( π‘₯ βˆ₯ π‘š ↔ π‘š βˆ₯ π‘š ) )
97 54 nnzd ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ π‘š ∈ β„€ )
98 iddvds ⊒ ( π‘š ∈ β„€ β†’ π‘š βˆ₯ π‘š )
99 97 98 syl ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ π‘š βˆ₯ π‘š )
100 96 54 99 elrabd ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ π‘š ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } )
101 100 snssd ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ { π‘š } βŠ† { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } )
102 101 sselda ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘š } ) β†’ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } )
103 102 72 syldan ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘š } ) β†’ ( 𝐹 β€˜ π‘˜ ) ∈ β„‚ )
104 0cn ⊒ 0 ∈ β„‚
105 ifcl ⊒ ( ( ( 𝐹 β€˜ π‘˜ ) ∈ β„‚ ∧ 0 ∈ β„‚ ) β†’ if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) ∈ β„‚ )
106 103 104 105 sylancl ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ { π‘š } ) β†’ if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) ∈ β„‚ )
107 eldifsni ⊒ ( π‘˜ ∈ ( { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } βˆ– { π‘š } ) β†’ π‘˜ β‰  π‘š )
108 107 adantl ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ ( { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } βˆ– { π‘š } ) ) β†’ π‘˜ β‰  π‘š )
109 108 neneqd ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ ( { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } βˆ– { π‘š } ) ) β†’ Β¬ π‘˜ = π‘š )
110 109 iffalsed ⊒ ( ( ( πœ‘ ∧ π‘š ∈ β„• ) ∧ π‘˜ ∈ ( { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } βˆ– { π‘š } ) ) β†’ if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) = 0 )
111 fzfid ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ ( 1 ... π‘š ) ∈ Fin )
112 dvdsssfz1 ⊒ ( π‘š ∈ β„• β†’ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } βŠ† ( 1 ... π‘š ) )
113 112 adantl ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } βŠ† ( 1 ... π‘š ) )
114 111 113 ssfid ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ∈ Fin )
115 101 106 110 114 fsumss ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ Ξ£ π‘˜ ∈ { π‘š } if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) = Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) )
116 1 ffvelcdmda ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ ( 𝐹 β€˜ π‘š ) ∈ β„‚ )
117 iftrue ⊒ ( π‘˜ = π‘š β†’ if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) = ( 𝐹 β€˜ π‘˜ ) )
118 fveq2 ⊒ ( π‘˜ = π‘š β†’ ( 𝐹 β€˜ π‘˜ ) = ( 𝐹 β€˜ π‘š ) )
119 117 118 eqtrd ⊒ ( π‘˜ = π‘š β†’ if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) = ( 𝐹 β€˜ π‘š ) )
120 119 sumsn ⊒ ( ( π‘š ∈ β„• ∧ ( 𝐹 β€˜ π‘š ) ∈ β„‚ ) β†’ Ξ£ π‘˜ ∈ { π‘š } if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) = ( 𝐹 β€˜ π‘š ) )
121 54 116 120 syl2anc ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ Ξ£ π‘˜ ∈ { π‘š } if ( π‘˜ = π‘š , ( 𝐹 β€˜ π‘˜ ) , 0 ) = ( 𝐹 β€˜ π‘š ) )
122 95 115 121 3eqtr2d ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ Ξ£ π‘˜ ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ ( π‘š / π‘˜ ) } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐹 β€˜ π‘˜ ) ) = ( 𝐹 β€˜ π‘š ) )
123 53 58 122 3eqtrd ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐺 β€˜ ( π‘š / 𝑗 ) ) ) = ( 𝐹 β€˜ π‘š ) )
124 123 mpteq2dva ⊒ ( πœ‘ β†’ ( π‘š ∈ β„• ↦ Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐺 β€˜ ( π‘š / 𝑗 ) ) ) ) = ( π‘š ∈ β„• ↦ ( 𝐹 β€˜ π‘š ) ) )
125 3 124 eqtr4d ⊒ ( πœ‘ β†’ 𝐹 = ( π‘š ∈ β„• ↦ Ξ£ 𝑗 ∈ { π‘₯ ∈ β„• ∣ π‘₯ βˆ₯ π‘š } ( ( ΞΌ β€˜ 𝑗 ) Β· ( 𝐺 β€˜ ( π‘š / 𝑗 ) ) ) ) )