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	⊢ σ : ( ℂ × ℕ ) ⟶ ℂ

Proof

Step	Hyp	Ref	Expression
1		fzfid	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ Fin )
2		dvdsssfz1	⊢ ( 𝑛 ∈ ℕ → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
3	2	adantl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
4	1 3	ssfid	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } ∈ Fin )
5		elrabi	⊢ ( 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } → 𝑘 ∈ ℕ )
6	5	nncnd	⊢ ( 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } → 𝑘 ∈ ℂ )
7		simpl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ ℂ )
8		cxpcl	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 ↑𝑐 𝑥 ) ∈ ℂ )
9	6 7 8	syl2anr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } ) → ( 𝑘 ↑𝑐 𝑥 ) ∈ ℂ )
10	4 9	fsumcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } ( 𝑘 ↑𝑐 𝑥 ) ∈ ℂ )
11	10	rgen2	⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑛 ∈ ℕ Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } ( 𝑘 ↑𝑐 𝑥 ) ∈ ℂ
12		df-sgm	⊢ σ = ( 𝑥 ∈ ℂ , 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } ( 𝑘 ↑𝑐 𝑥 ) )
13	12	fmpo	⊢ ( ∀ 𝑥 ∈ ℂ ∀ 𝑛 ∈ ℕ Σ 𝑘 ∈ { 𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝑛 } ( 𝑘 ↑𝑐 𝑥 ) ∈ ℂ ↔ σ : ( ℂ × ℕ ) ⟶ ℂ )
14	11 13	mpbi	⊢ σ : ( ℂ × ℕ ) ⟶ ℂ