gcdcl

Description: Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	gcdcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℕ_{0}$

Step	Hyp	Ref	Expression
1		oveq12	$⊢ (M = 0 \land N = 0) \to M \gcd N = 0 \gcd 0$
2		gcd0val	$⊢ 0 \gcd 0 = 0$
3	1 2	eqtrdi	$⊢ (M = 0 \land N = 0) \to M \gcd N = 0$
4		0nn0	$⊢ 0 \in ℕ_{0}$
5	3 4	eqeltrdi	$⊢ (M = 0 \land N = 0) \to M \gcd N \in ℕ_{0}$
6	5	adantl	$⊢ ((M \in ℤ \land N \in ℤ) \land (M = 0 \land N = 0)) \to M \gcd N \in ℕ_{0}$
7		gcdn0cl	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N \in ℕ$
8	7	nnnn0d	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N \in ℕ_{0}$
9	6 8	pm2.61dan	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℕ_{0}$

Metamath Proof Explorer