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

Metamath Proof Explorer

Theorem dvdsgcdidd

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

Ref Expression
Hypotheses dvdsgcdidd.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
dvdsgcdidd.2 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
dvdsgcdidd.3 ⊢ ( 𝜑 → 𝑀 ∥ 𝑁 )
Assertion dvdsgcdidd ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 𝑀 )

Proof

Step Hyp Ref Expression
1 dvdsgcdidd.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 dvdsgcdidd.2 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
3 dvdsgcdidd.3 ⊢ ( 𝜑 → 𝑀 ∥ 𝑁 )
4 2 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
5 1 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
6 1 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
7 4 5 6 divcan1d ⊢ ( 𝜑 → ( ( 𝑁 / 𝑀 ) · 𝑀 ) = 𝑁 )
8 7 oveq2d ⊢ ( 𝜑 → ( 𝑀 gcd ( ( 𝑁 / 𝑀 ) · 𝑀 ) ) = ( 𝑀 gcd 𝑁 ) )
9 1 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
10 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
11 dvdsval2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )
12 10 6 2 11 syl3anc ⊢ ( 𝜑 → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )
13 3 12 mpbid ⊢ ( 𝜑 → ( 𝑁 / 𝑀 ) ∈ ℤ )
14 9 13 gcdmultipled ⊢ ( 𝜑 → ( 𝑀 gcd ( ( 𝑁 / 𝑀 ) · 𝑀 ) ) = 𝑀 )
15 8 14 eqtr3d ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 𝑀 )