Theorem sgmcl

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

	Ref	Expression
Assertion	sgmcl	$$⊢\left(A\in ℂ\wedge B\in \mathbb{N}\right)\to A\sigma B\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		sgmf	$$⊢\sigma :ℂ\times \mathbb{N}⟶ℂ$$
2	1	fovcl	$$⊢\left(A\in ℂ\wedge B\in \mathbb{N}\right)\to A\sigma B\in ℂ$$