Metamath Proof Explorer

Theorem gcdnncli

Description: Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024)

Ref Expression
Hypotheses gcdnncli.1 
|- M e. NN
gcdnncli.2 
|- N e. NN
Assertion gcdnncli 
|- ( M gcd N ) e. NN

Proof

Step Hyp Ref Expression
1 gcdnncli.1 
 |-  M e. NN
2 gcdnncli.2 
 |-  N e. NN
3 gcdnncl 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) e. NN )
4 1 2 3 mp2an 
 |-  ( M gcd N ) e. NN