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 \in ℤ \land N \in ℤ \land N \neq 0) \to M \gcd N \in ℕ$

Step	Hyp	Ref	Expression
1		neneq	$⊢ N \neq 0 \to \neg N = 0$
2	1	intnand	$⊢ N \neq 0 \to \neg (M = 0 \land N = 0)$
3	2	anim2i	$⊢ ((M \in ℤ \land N \in ℤ) \land N \neq 0) \to ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0))$
4	3	3impa	$⊢ (M \in ℤ \land N \in ℤ \land N \neq 0) \to ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0))$
5		gcdn0cl	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N \in ℕ$
6	4 5	syl	$⊢ (M \in ℤ \land N \in ℤ \land N \neq 0) \to M \gcd N \in ℕ$

Metamath Proof Explorer