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

Proof

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