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 )