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 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
gcdle1d.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
Assertion gcdle1d ( 𝜑 → ( 𝑀 gcd 𝑁 ) ≤ 𝑀 )

Proof

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