Theorem gcdeq0

Description: The gcd of two integers is zero iff they are both zero. (Contributed by Paul Chapman, 21-Mar-2011)

	Ref	Expression
Assertion	gcdeq0	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) = 0 ↔ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gcdn0cl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ )
2	1	nnne0d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) ≠ 0 )
3	2	ex	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd 𝑁 ) ≠ 0 ) )
4	3	necon4bd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) = 0 → ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) )
5		oveq12	⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd 𝑁 ) = ( 0 gcd 0 ) )
6		gcd0val	⊢ ( 0 gcd 0 ) = 0
7	5 6	eqtrdi	⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd 𝑁 ) = 0 )
8	4 7	impbid1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) = 0 ↔ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) )