This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gcdmultiple

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 ∈ ℕ ∧ N ∈ ℕ → M gcd M ⋅ N = M

Proof

Step Hyp Ref Expression
1 nnz ⊢ N ∈ ℕ → N ∈ ℤ
2 gcdmultiplez ⊢ M ∈ ℕ ∧ N ∈ ℤ → M gcd M ⋅ N = M
3 1 2 sylan2 ⊢ M ∈ ℕ ∧ N ∈ ℕ → M gcd M ⋅ N = M