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	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) = 𝐴 ↔ 𝐴 ∥ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nnz	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
2		gcdzeq	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) = 𝐴 ↔ 𝐴 ∥ 𝐵 ) )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) = 𝐴 ↔ 𝐴 ∥ 𝐵 ) )