gcdnncl

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

		Ref	Expression
	Assertion	gcdnncl	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \in ℕ$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (M \in ℕ \land N \in ℕ) \to M \in ℕ$
2	1	nnzd	$⊢ (M \in ℕ \land N \in ℕ) \to M \in ℤ$
3		simpr	$⊢ (M \in ℕ \land N \in ℕ) \to N \in ℕ$
4	3	nnzd	$⊢ (M \in ℕ \land N \in ℕ) \to N \in ℤ$
5	3	nnne0d	$⊢ (M \in ℕ \land N \in ℕ) \to N \neq 0$
6	5	neneqd	$⊢ (M \in ℕ \land N \in ℕ) \to \neg N = 0$
7	6	intnand	$⊢ (M \in ℕ \land N \in ℕ) \to \neg (M = 0 \land N = 0)$
8		gcdn0cl	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N \in ℕ$
9	2 4 7 8	syl21anc	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \in ℕ$

Metamath Proof Explorer