Theorem gcd2n0cl

Description: Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021)

	Ref	Expression
Assertion	gcd2n0cl	|- ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M gcd N ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		neneq	|- ( N =/= 0 -> -. N = 0 )
2	1	intnand	|- ( N =/= 0 -> -. ( M = 0 /\ N = 0 ) )
3	2	anim2i	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ N =/= 0 ) -> ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) )
4	3	3impa	|- ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) )
5		gcdn0cl	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) e. NN )
6	4 5	syl	|- ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M gcd N ) e. NN )