Metamath Proof Explorer


Theorem gcddvds

Description: The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion gcddvds M N M gcd N M M gcd N N

Proof

Step Hyp Ref Expression
1 0z 0
2 dvds0 0 0 0
3 1 2 ax-mp 0 0
4 breq2 M = 0 0 M 0 0
5 breq2 N = 0 0 N 0 0
6 4 5 bi2anan9 M = 0 N = 0 0 M 0 N 0 0 0 0
7 anidm 0 0 0 0 0 0
8 6 7 bitrdi M = 0 N = 0 0 M 0 N 0 0
9 3 8 mpbiri M = 0 N = 0 0 M 0 N
10 oveq12 M = 0 N = 0 M gcd N = 0 gcd 0
11 gcd0val 0 gcd 0 = 0
12 10 11 eqtrdi M = 0 N = 0 M gcd N = 0
13 12 breq1d M = 0 N = 0 M gcd N M 0 M
14 12 breq1d M = 0 N = 0 M gcd N N 0 N
15 13 14 anbi12d M = 0 N = 0 M gcd N M M gcd N N 0 M 0 N
16 9 15 mpbird M = 0 N = 0 M gcd N M M gcd N N
17 16 adantl M N M = 0 N = 0 M gcd N M M gcd N N
18 eqid n | z M N n z = n | z M N n z
19 eqid n | n M n N = n | n M n N
20 18 19 gcdcllem3 M N ¬ M = 0 N = 0 sup n | n M n N < sup n | n M n N < M sup n | n M n N < N K K M K N K sup n | n M n N <
21 20 simp2d M N ¬ M = 0 N = 0 sup n | n M n N < M sup n | n M n N < N
22 gcdn0val M N ¬ M = 0 N = 0 M gcd N = sup n | n M n N <
23 22 breq1d M N ¬ M = 0 N = 0 M gcd N M sup n | n M n N < M
24 22 breq1d M N ¬ M = 0 N = 0 M gcd N N sup n | n M n N < N
25 23 24 anbi12d M N ¬ M = 0 N = 0 M gcd N M M gcd N N sup n | n M n N < M sup n | n M n N < N
26 21 25 mpbird M N ¬ M = 0 N = 0 M gcd N M M gcd N N
27 17 26 pm2.61dan M N M gcd N M M gcd N N