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 ⊢ φ → M ∈ ℕ
dvdsgcdidd.2 ⊢ φ → N ∈ ℤ
dvdsgcdidd.3 ⊢ φ → M ∥ N
Assertion dvdsgcdidd ⊢ φ → M gcd N = M

Proof

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