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	$⊢ σ : ℂ \times ℕ ⟶ ℂ$

Proof

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