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

Metamath Proof Explorer

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