Theorem gcdcld

Description: Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016)

	Ref	Expression
Hypotheses	gcdcld.1	$$⊢\phi \to M\in \mathbb{Z}$$
	gcdcld.2	$$⊢\phi \to N\in \mathbb{Z}$$
Assertion	gcdcld	$$⊢\phi \to M\gcd N\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		gcdcld.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		gcdcld.2	$$⊢\phi \to N\in \mathbb{Z}$$
3		gcdcl	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to M\gcd N\in {\mathbb{N}}_0$$
4	1 2 3	syl2anc	$$⊢\phi \to M\gcd N\in {\mathbb{N}}_0$$