Theorem sgmcl

Description: Closure of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	sgmcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		sgmf	⊢ σ : ( ℂ × ℕ ) ⟶ ℂ
2	1	fovcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) ∈ ℂ )