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 e. NN /\ B e. NN ) -> ( ( A gcd B ) = A <-> A || B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nnz | |- ( B e. NN -> B e. ZZ ) |
|
| 2 | gcdzeq | |- ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) = A <-> A || B ) ) |
|
| 3 | 1 2 | sylan2 | |- ( ( A e. NN /\ B e. NN ) -> ( ( A gcd B ) = A <-> A || B ) ) |