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

Proof

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