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	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(A\gcd B=A\leftrightarrow A\parallel B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnz	$$⊢B\in \mathbb{N}\to B\in \mathbb{Z}$$
2		gcdzeq	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{Z}\right)\to \left(A\gcd B=A\leftrightarrow A\parallel B\right)$$
3	1 2	sylan2	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(A\gcd B=A\leftrightarrow A\parallel B\right)$$