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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 σ 𝐵 ) ∈ ℂ )

Proof

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