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	$⊢ φ \to M \in ℕ$
		gcdle1d.n	$⊢ φ \to N \in ℤ$
	Assertion	gcdle1d	$⊢ φ \to M \gcd N \leq M$

Proof

Step	Hyp	Ref	Expression
1		gcdle1d.m	$⊢ φ \to M \in ℕ$
2		gcdle1d.n	$⊢ φ \to N \in ℤ$
3	1	nnzd	$⊢ φ \to M \in ℤ$
4		gcddvds	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
5	3 2 4	syl2anc	$⊢ φ \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
6	5	simpld	$⊢ φ \to (M \gcd N) ∥ M$
7	3 2	gcdcld	$⊢ φ \to M \gcd N \in ℕ_{0}$
8	7	nn0zd	$⊢ φ \to M \gcd N \in ℤ$
9		dvdsle	$⊢ (M \gcd N \in ℤ \land M \in ℕ) \to ((M \gcd N) ∥ M \to M \gcd N \leq M)$
10	8 1 9	syl2anc	$⊢ φ \to ((M \gcd N) ∥ M \to M \gcd N \leq M)$
11	6 10	mpd	$⊢ φ \to M \gcd N \leq M$