Metamath Proof Explorer


Theorem sgmcl

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

Ref Expression
Assertion sgmcl
|- ( ( A e. CC /\ B e. NN ) -> ( A sigma B ) e. CC )

Proof

Step Hyp Ref Expression
1 sgmf
 |-  sigma : ( CC X. NN ) --> CC
2 1 fovcl
 |-  ( ( A e. CC /\ B e. NN ) -> ( A sigma B ) e. CC )