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