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 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
gcdmultipled.2 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
Assertion gcdmultipled ( 𝜑 → ( 𝑀 gcd ( 𝑁 · 𝑀 ) ) = 𝑀 )

Proof

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