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

Metamath Proof Explorer

Theorem gcdmultipled

Description: The greatest common divisor of a nonnegative integer M and a multiple of it is M itself. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses gcdmultipled.1 ⊢ φ → M ∈ ℕ 0
gcdmultipled.2 ⊢ φ → N ∈ ℤ
Assertion gcdmultipled ⊢ φ → M gcd N ⋅ M = M

Proof

Step Hyp Ref Expression
1 gcdmultipled.1 ⊢ φ → M ∈ ℕ 0
2 gcdmultipled.2 ⊢ φ → N ∈ ℤ
3 1 nn0zd ⊢ φ → M ∈ ℤ
4 0zd ⊢ φ → 0 ∈ ℤ
5 gcdaddm ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ 0 ∈ ℤ → M gcd 0 = M gcd 0 + N ⋅ M
6 2 3 4 5 syl3anc ⊢ φ → M gcd 0 = M gcd 0 + N ⋅ M
7 nn0gcdid0 ⊢ M ∈ ℕ 0 → M gcd 0 = M
8 1 7 syl ⊢ φ → M gcd 0 = M
9 2 3 zmulcld ⊢ φ → N ⋅ M ∈ ℤ
10 9 zcnd ⊢ φ → N ⋅ M ∈ ℂ
11 10 addlidd ⊢ φ → 0 + N ⋅ M = N ⋅ M
12 11 oveq2d ⊢ φ → M gcd 0 + N ⋅ M = M gcd N ⋅ M
13 6 8 12 3eqtr3rd ⊢ φ → M gcd N ⋅ M = M