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

Metamath Proof Explorer

Theorem gcdle1d

Description: The greatest common divisor of a positive integer and another integer is less than or equal to the positive integer. (Contributed by SN, 25-Aug-2024)

Ref Expression
Hypotheses gcdle1d.m ⊢ φ → M ∈ ℕ
gcdle1d.n ⊢ φ → N ∈ ℤ
Assertion gcdle1d ⊢ φ → M gcd N ≤ M

Proof

Step Hyp Ref Expression
1 gcdle1d.m ⊢ φ → M ∈ ℕ
2 gcdle1d.n ⊢ φ → N ∈ ℤ
3 1 nnzd ⊢ φ → M ∈ ℤ
4 gcddvds ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N ∥ M ∧ M gcd N ∥ N
5 3 2 4 syl2anc ⊢ φ → M gcd N ∥ M ∧ M gcd N ∥ N
6 5 simpld ⊢ φ → M gcd N ∥ M
7 3 2 gcdcld ⊢ φ → M gcd N ∈ ℕ 0
8 7 nn0zd ⊢ φ → M gcd N ∈ ℤ
9 dvdsle ⊢ M gcd N ∈ ℤ ∧ M ∈ ℕ → M gcd N ∥ M → M gcd N ≤ M
10 8 1 9 syl2anc ⊢ φ → M gcd N ∥ M → M gcd N ≤ M
11 6 10 mpd ⊢ φ → M gcd N ≤ M