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 ⊢ M ∈ ℤ ∧ N ∈ ℤ → ¬ M = 0 ∧ N = 0 ↔ 0 < M gcd N

Proof

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