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 φM
gcdle1d.n φN
Assertion gcdle1d φMgcdNM

Proof

Step Hyp Ref Expression
1 gcdle1d.m φM
2 gcdle1d.n φN
3 1 nnzd φM
4 gcddvds MNMgcdNMMgcdNN
5 3 2 4 syl2anc φMgcdNMMgcdNN
6 5 simpld φMgcdNM
7 3 2 gcdcld φMgcdN0
8 7 nn0zd φMgcdN
9 dvdsle MgcdNMMgcdNMMgcdNM
10 8 1 9 syl2anc φMgcdNMMgcdNM
11 6 10 mpd φMgcdNM