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

Metamath Proof Explorer

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 )