This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sgmcl

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

		Ref	Expression
	Assertion	sgmcl	$⊢ (A \in ℂ \land B \in ℕ) \to A σ B \in ℂ$

Step	Hyp	Ref	Expression
1		sgmf	$⊢ σ : ℂ \times ℕ ⟶ ℂ$
2	1	fovcl	$⊢ (A \in ℂ \land B \in ℕ) \to A σ B \in ℂ$