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