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

Metamath Proof Explorer

Theorem gcdnncl

Description: Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020)

Ref Expression
Assertion gcdnncl 
|- ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) e. NN )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( M e. NN /\ N e. NN ) -> M e. NN )
2 1 nnzd 
 |-  ( ( M e. NN /\ N e. NN ) -> M e. ZZ )
3 simpr 
 |-  ( ( M e. NN /\ N e. NN ) -> N e. NN )
4 3 nnzd 
 |-  ( ( M e. NN /\ N e. NN ) -> N e. ZZ )
5 3 nnne0d 
 |-  ( ( M e. NN /\ N e. NN ) -> N =/= 0 )
6 5 neneqd 
 |-  ( ( M e. NN /\ N e. NN ) -> -. N = 0 )
7 6 intnand 
 |-  ( ( M e. NN /\ N e. NN ) -> -. ( M = 0 /\ N = 0 ) )
8 gcdn0cl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) e. NN )
9 2 4 7 8 syl21anc 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M gcd N ) e. NN )