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	|- ( ph -> M e. ZZ )
	gcdle2d.n	|- ( ph -> N e. NN )
Assertion	gcdle2d	|- ( ph -> ( M gcd N ) <_ N )

Proof

Step	Hyp	Ref	Expression
1		gcdle2d.m	|- ( ph -> M e. ZZ )
2		gcdle2d.n	|- ( ph -> N e. NN )
3	2	nnzd	|- ( ph -> N e. ZZ )
4		gcddvds	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
5	1 3 4	syl2anc	|- ( ph -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
6	5	simprd	|- ( ph -> ( M gcd N ) || N )
7	1 3	gcdcld	|- ( ph -> ( M gcd N ) e. NN0 )
8	7	nn0zd	|- ( ph -> ( M gcd N ) e. ZZ )
9		dvdsle	|- ( ( ( M gcd N ) e. ZZ /\ N e. NN ) -> ( ( M gcd N ) || N -> ( M gcd N ) <_ N ) )
10	8 2 9	syl2anc	|- ( ph -> ( ( M gcd N ) || N -> ( M gcd N ) <_ N ) )
11	6 10	mpd	|- ( ph -> ( M gcd N ) <_ N )