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 𝐵 ) = 𝐴 ↔ 𝐴 ∥ 𝐵 ) )