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

Metamath Proof Explorer

Theorem gcdle2d

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 gcdle2d.m ⊢ φ → M ∈ ℤ
gcdle2d.n ⊢ φ → N ∈ ℕ
Assertion gcdle2d ⊢ φ → M gcd N ≤ N

Proof

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