Description: The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by AV, 12-Jan-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | gcdmultiple | |- ( ( M e. NN /\ N e. NN ) -> ( M gcd ( M x. N ) ) = M ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nnz | |- ( N e. NN -> N e. ZZ ) |
|
| 2 | gcdmultiplez | |- ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. N ) ) = M ) |
|
| 3 | 1 2 | sylan2 | |- ( ( M e. NN /\ N e. NN ) -> ( M gcd ( M x. N ) ) = M ) |