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	$⊢ (M \in ℤ \land N \in ℤ) \to (M \gcd N = 0 \leftrightarrow (M = 0 \land N = 0))$

Step	Hyp	Ref	Expression
1		gcdn0cl	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N \in ℕ$
2	1	nnne0d	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N \neq 0$
3	2	ex	$⊢ (M \in ℤ \land N \in ℤ) \to (\neg (M = 0 \land N = 0) \to M \gcd N \neq 0)$
4	3	necon4bd	$⊢ (M \in ℤ \land N \in ℤ) \to (M \gcd N = 0 \to (M = 0 \land N = 0))$
5		oveq12	$⊢ (M = 0 \land N = 0) \to M \gcd N = 0 \gcd 0$
6		gcd0val	$⊢ 0 \gcd 0 = 0$
7	5 6	eqtrdi	$⊢ (M = 0 \land N = 0) \to M \gcd N = 0$
8	4 7	impbid1	$⊢ (M \in ℤ \land N \in ℤ) \to (M \gcd N = 0 \leftrightarrow (M = 0 \land N = 0))$

Metamath Proof Explorer