Theorem gcdnncli

Description: Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024)

	Ref	Expression
Hypotheses	gcdnncli.1	$$⊢M\in \mathbb{N}$$
	gcdnncli.2	$$⊢N\in \mathbb{N}$$
Assertion	gcdnncli	$$⊢M\gcd N\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		gcdnncli.1	$$⊢M\in \mathbb{N}$$
2		gcdnncli.2	$$⊢N\in \mathbb{N}$$
3		gcdnncl	$$⊢\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)\to M\gcd N\in \mathbb{N}$$
4	1 2 3	mp2an	$$⊢M\gcd N\in \mathbb{N}$$