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 | |
|
gcdle1d.n | |
||
Assertion | gcdle1d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gcdle1d.m | |
|
2 | gcdle1d.n | |
|
3 | 1 | nnzd | |
4 | gcddvds | |
|
5 | 3 2 4 | syl2anc | |
6 | 5 | simpld | |
7 | 3 2 | gcdcld | |
8 | 7 | nn0zd | |
9 | dvdsle | |
|
10 | 8 1 9 | syl2anc | |
11 | 6 10 | mpd | |