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 𝑁 ) ∈ ℕ ) |
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 𝑁 ) ∈ ℕ ) |