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	$$⊢\phi \to M\in \mathbb{Z}$$
	gcdle2d.n	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	gcdle2d	$$⊢\phi \to M\gcd N\le N$$

Proof

Step	Hyp	Ref	Expression
1		gcdle2d.m	$$⊢\phi \to M\in \mathbb{Z}$$
2		gcdle2d.n	$$⊢\phi \to N\in \mathbb{N}$$
3	2	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
4		gcddvds	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(\left(M\gcd N\right)\parallel M\wedge \left(M\gcd N\right)\parallel N\right)$$
5	1 3 4	syl2anc	$$⊢\phi \to \left(\left(M\gcd N\right)\parallel M\wedge \left(M\gcd N\right)\parallel N\right)$$
6	5	simprd	$$⊢\phi \to \left(M\gcd N\right)\parallel N$$
7	1 3	gcdcld	$$⊢\phi \to M\gcd N\in {\mathbb{N}}_0$$
8	7	nn0zd	$$⊢\phi \to M\gcd N\in \mathbb{Z}$$
9		dvdsle	$$⊢\left(M\gcd N\in \mathbb{Z}\wedge N\in \mathbb{N}\right)\to \left(\left(M\gcd N\right)\parallel N\to M\gcd N\le N\right)$$
10	8 2 9	syl2anc	$$⊢\phi \to \left(\left(M\gcd N\right)\parallel N\to M\gcd N\le N\right)$$
11	6 10	mpd	$$⊢\phi \to M\gcd N\le N$$