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 :ℂ\times \mathbb{N}⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$$⊢\left(x\in ℂ\wedge n\in \mathbb{N}\right)\to \left(1\dots n\right)\in \mathrm{Fin}$$
2		dvdsssfz1	$$⊢n\in \mathbb{N}\to \left\{p\in \mathbb{N}|p\parallel n\right\}\subseteq \left(1\dots n\right)$$
3	2	adantl	$$⊢\left(x\in ℂ\wedge n\in \mathbb{N}\right)\to \left\{p\in \mathbb{N}|p\parallel n\right\}\subseteq \left(1\dots n\right)$$
4	1 3	ssfid	$$⊢\left(x\in ℂ\wedge n\in \mathbb{N}\right)\to \left\{p\in \mathbb{N}|p\parallel n\right\}\in \mathrm{Fin}$$
5		elrabi	$$⊢k\in \left\{p\in \mathbb{N}|p\parallel n\right\}\to k\in \mathbb{N}$$
6	5	nncnd	$$⊢k\in \left\{p\in \mathbb{N}|p\parallel n\right\}\to k\in ℂ$$
7		simpl	$$⊢\left(x\in ℂ\wedge n\in \mathbb{N}\right)\to x\in ℂ$$
8		cxpcl	$$⊢\left(k\in ℂ\wedge x\in ℂ\right)\to k^x\in ℂ$$
9	6 7 8	syl2anr	$$⊢\left(\left(x\in ℂ\wedge n\in \mathbb{N}\right)\wedge k\in \left\{p\in \mathbb{N}|p\parallel n\right\}\right)\to k^x\in ℂ$$
10	4 9	fsumcl	$$⊢\left(x\in ℂ\wedge n\in \mathbb{N}\right)\to \sum _{k\in \left\{p\in \mathbb{N}|p\parallel n\right\}}{k}^x\in ℂ$$
11	10	rgen2	$$⊢\forall x\in ℂ\forall n\in \mathbb{N}\sum _{k\in \left\{p\in \mathbb{N}|p\parallel n\right\}}{k}^x\in ℂ$$
12		df-sgm	$$⊢\sigma =\left(x\in ℂ,n\in \mathbb{N}⟼\sum _{k\in \left\{p\in \mathbb{N}|p\parallel n\right\}}{k}^x\right)$$
13	12	fmpo	$$⊢\forall x\in ℂ\forall n\in \mathbb{N}\sum _{k\in \left\{p\in \mathbb{N}|p\parallel n\right\}}{k}^x\in ℂ\leftrightarrow \sigma :ℂ\times \mathbb{N}⟶ℂ$$
14	11 13	mpbi	$$⊢\sigma :ℂ\times \mathbb{N}⟶ℂ$$