Metamath Proof Explorer


Theorem nndvdslegcd

Description: A positive integer which divides both positive operands of the gcd operator is bounded by it. (Contributed by AV, 9-Aug-2020)

Ref Expression
Assertion nndvdslegcd K M N K M K N K M gcd N

Proof

Step Hyp Ref Expression
1 nnz K K
2 nnz M M
3 nnz N N
4 1 2 3 3anim123i K M N K M N
5 nnne0 M M 0
6 5 neneqd M ¬ M = 0
7 6 3ad2ant2 K M N ¬ M = 0
8 7 intnanrd K M N ¬ M = 0 N = 0
9 dvdslegcd K M N ¬ M = 0 N = 0 K M K N K M gcd N
10 4 8 9 syl2anc K M N K M K N K M gcd N