Metamath Proof Explorer


Theorem gcdmultiplei

Description: The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024)

Ref Expression
Hypotheses gcdmultiplei.1
|- M e. NN
gcdmultiplei.2
|- N e. NN
Assertion gcdmultiplei
|- ( M gcd ( M x. N ) ) = M

Proof

Step Hyp Ref Expression
1 gcdmultiplei.1
 |-  M e. NN
2 gcdmultiplei.2
 |-  N e. NN
3 gcdmultiple
 |-  ( ( M e. NN /\ N e. NN ) -> ( M gcd ( M x. N ) ) = M )
4 1 2 3 mp2an
 |-  ( M gcd ( M x. N ) ) = M