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 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → ( 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 ⊢ σ : ( ℂ × ℕ ) ⟶ ℂ