This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( 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 )