This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sgmf

Description: The divisor function is a function into the complex numbers. (Contributed by Mario Carneiro, 22-Sep-2014) (Revised by Mario Carneiro, 21-Jun-2015)

Ref Expression
Assertion sgmf 
|- sigma : ( CC X. NN ) --> CC

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( ( x e. CC /\ n e. NN ) -> ( 1 ... n ) e. Fin )
2 dvdsssfz1 
 |-  ( n e. NN -> { p e. NN | p || n } C_ ( 1 ... n ) )
3 2 adantl 
 |-  ( ( x e. CC /\ n e. NN ) -> { p e. NN | p || n } C_ ( 1 ... n ) )
4 1 3 ssfid 
 |-  ( ( x e. CC /\ n e. NN ) -> { p e. NN | p || n } e. Fin )
5 elrabi 
 |-  ( k e. { p e. NN | p || n } -> k e. NN )
6 5 nncnd 
 |-  ( k e. { p e. NN | p || n } -> k e. CC )
7 simpl 
 |-  ( ( x e. CC /\ n e. NN ) -> x e. CC )
8 cxpcl 
 |-  ( ( k e. CC /\ x e. CC ) -> ( k ^c x ) e. CC )
9 6 7 8 syl2anr 
 |-  ( ( ( x e. CC /\ n e. NN ) /\ k e. { p e. NN | p || n } ) -> ( k ^c x ) e. CC )
10 4 9 fsumcl 
 |-  ( ( x e. CC /\ n e. NN ) -> sum_ k e. { p e. NN | p || n } ( k ^c x ) e. CC )
11 10 rgen2 
 |-  A. x e. CC A. n e. NN sum_ k e. { p e. NN | p || n } ( k ^c x ) e. CC
12 df-sgm 
 |-  sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^c x ) )
13 12 fmpo 
 |-  ( A. x e. CC A. n e. NN sum_ k e. { p e. NN | p || n } ( k ^c x ) e. CC <-> sigma : ( CC X. NN ) --> CC )
14 11 13 mpbi 
 |-  sigma : ( CC X. NN ) --> CC