Theorem gcdnncli

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

	Ref	Expression
Hypotheses	gcdnncli.1	⊢ 𝑀 ∈ ℕ
	gcdnncli.2	⊢ 𝑁 ∈ ℕ
Assertion	gcdnncli	⊢ ( 𝑀 gcd 𝑁 ) ∈ ℕ

Proof

Step	Hyp	Ref	Expression
1		gcdnncli.1	⊢ 𝑀 ∈ ℕ
2		gcdnncli.2	⊢ 𝑁 ∈ ℕ
3		gcdnncl	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ )
4	1 2 3	mp2an	⊢ ( 𝑀 gcd 𝑁 ) ∈ ℕ