Metamath Proof Explorer


Theorem gcdn0gt0

Description: The gcd of two integers is positive (nonzero) iff they are not both zero. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion gcdn0gt0 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ↔ 0 < ( 𝑀 gcd 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 gcdcl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ0 )
2 0re 0 ∈ ℝ
3 nn0re ( ( 𝑀 gcd 𝑁 ) ∈ ℕ0 → ( 𝑀 gcd 𝑁 ) ∈ ℝ )
4 nn0ge0 ( ( 𝑀 gcd 𝑁 ) ∈ ℕ0 → 0 ≤ ( 𝑀 gcd 𝑁 ) )
5 leltne ( ( 0 ∈ ℝ ∧ ( 𝑀 gcd 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝑀 gcd 𝑁 ) ) → ( 0 < ( 𝑀 gcd 𝑁 ) ↔ ( 𝑀 gcd 𝑁 ) ≠ 0 ) )
6 2 3 4 5 mp3an2i ( ( 𝑀 gcd 𝑁 ) ∈ ℕ0 → ( 0 < ( 𝑀 gcd 𝑁 ) ↔ ( 𝑀 gcd 𝑁 ) ≠ 0 ) )
7 1 6 syl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 < ( 𝑀 gcd 𝑁 ) ↔ ( 𝑀 gcd 𝑁 ) ≠ 0 ) )
8 gcdeq0 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) = 0 ↔ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) )
9 8 necon3abid ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ≠ 0 ↔ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) )
10 7 9 bitr2d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ↔ 0 < ( 𝑀 gcd 𝑁 ) ) )