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 )