This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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