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

Metamath Proof Explorer

Theorem gcdeq

Description: A is equal to its gcd with B if and only if A divides B . (Contributed by Mario Carneiro, 23-Feb-2014) (Proof shortened by AV, 8-Aug-2021)

		Ref	Expression
	Assertion	gcdeq	$⊢ (A \in ℕ \land B \in ℕ) \to (A \gcd B = A \leftrightarrow A ∥ B)$

Proof

Step	Hyp	Ref	Expression
1		nnz	$⊢ B \in ℕ \to B \in ℤ$
2		gcdzeq	$⊢ (A \in ℕ \land B \in ℤ) \to (A \gcd B = A \leftrightarrow A ∥ B)$
3	1 2	sylan2	$⊢ (A \in ℕ \land B \in ℕ) \to (A \gcd B = A \leftrightarrow A ∥ B)$