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

Proof

Step Hyp Ref Expression
1 fzfid ⊢ x ∈ ℂ ∧ n ∈ ℕ → 1 … n ∈ Fin
2 dvdsssfz1 ⊢ n ∈ ℕ → p ∈ ℕ | p ∥ n ⊆ 1 … n
3 2 adantl ⊢ x ∈ ℂ ∧ n ∈ ℕ → p ∈ ℕ | p ∥ n ⊆ 1 … n
4 1 3 ssfid ⊢ x ∈ ℂ ∧ n ∈ ℕ → p ∈ ℕ | p ∥ n ∈ Fin
5 elrabi ⊢ k ∈ p ∈ ℕ | p ∥ n → k ∈ ℕ
6 5 nncnd ⊢ k ∈ p ∈ ℕ | p ∥ n → k ∈ ℂ
7 simpl ⊢ x ∈ ℂ ∧ n ∈ ℕ → x ∈ ℂ
8 cxpcl ⊢ k ∈ ℂ ∧ x ∈ ℂ → k x ∈ ℂ
9 6 7 8 syl2anr ⊢ x ∈ ℂ ∧ n ∈ ℕ ∧ k ∈ p ∈ ℕ | p ∥ n → k x ∈ ℂ
10 4 9 fsumcl ⊢ x ∈ ℂ ∧ n ∈ ℕ → ∑ k ∈ p ∈ ℕ | p ∥ n k x ∈ ℂ
11 10 rgen2 ⊢ ∀ x ∈ ℂ ∀ n ∈ ℕ ∑ k ∈ p ∈ ℕ | p ∥ n k x ∈ ℂ
12 df-sgm ⊢ σ = x ∈ ℂ , n ∈ ℕ ⟼ ∑ k ∈ p ∈ ℕ | p ∥ n k x
13 12 fmpo ⊢ ∀ x ∈ ℂ ∀ n ∈ ℕ ∑ k ∈ p ∈ ℕ | p ∥ n k x ∈ ℂ ↔ σ : ℂ × ℕ ⟶ ℂ
14 11 13 mpbi ⊢ σ : ℂ × ℕ ⟶ ℂ