Metamath Proof Explorer


Theorem gcd2n0cl

Description: Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021)

Ref Expression
Assertion gcd2n0cl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 neneq ( 𝑁 ≠ 0 → ¬ 𝑁 = 0 )
2 1 intnand ( 𝑁 ≠ 0 → ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) )
3 2 anim2i ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) )
4 3 3impa ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) )
5 gcdn0cl ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ )
6 4 5 syl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ )