# 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 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)$

### Proof

Step Hyp Ref Expression
1 0z ${⊢}0\in ℤ$
2 dvds0 ${⊢}0\in ℤ\to 0\parallel 0$
3 1 2 ax-mp ${⊢}0\parallel 0$
4 breq2 ${⊢}{M}=0\to \left(0\parallel {M}↔0\parallel 0\right)$
5 breq2 ${⊢}{N}=0\to \left(0\parallel {N}↔0\parallel 0\right)$
6 4 5 bi2anan9 ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\left(0\parallel {M}\wedge 0\parallel {N}\right)↔\left(0\parallel 0\wedge 0\parallel 0\right)\right)$
7 anidm ${⊢}\left(0\parallel 0\wedge 0\parallel 0\right)↔0\parallel 0$
8 6 7 syl6bb ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\left(0\parallel {M}\wedge 0\parallel {N}\right)↔0\parallel 0\right)$
9 3 8 mpbiri ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(0\parallel {M}\wedge 0\parallel {N}\right)$
10 oveq12 ${⊢}\left({M}=0\wedge {N}=0\right)\to {M}\mathrm{gcd}{N}=0\mathrm{gcd}0$
11 gcd0val ${⊢}0\mathrm{gcd}0=0$
12 10 11 syl6eq ${⊢}\left({M}=0\wedge {N}=0\right)\to {M}\mathrm{gcd}{N}=0$
13 12 breq1d ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}↔0\parallel {M}\right)$
14 12 breq1d ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\left({M}\mathrm{gcd}{N}\right)\parallel {N}↔0\parallel {N}\right)$
15 13 14 anbi12d ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)↔\left(0\parallel {M}\wedge 0\parallel {N}\right)\right)$
16 9 15 mpbird ${⊢}\left({M}=0\wedge {N}=0\right)\to \left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)$
17 16 adantl ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({M}=0\wedge {N}=0\right)\right)\to \left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)$
18 eqid ${⊢}\left\{{n}\in ℤ|\forall {z}\in \left\{{M},{N}\right\}\phantom{\rule{.4em}{0ex}}{n}\parallel {z}\right\}=\left\{{n}\in ℤ|\forall {z}\in \left\{{M},{N}\right\}\phantom{\rule{.4em}{0ex}}{n}\parallel {z}\right\}$
19 eqid ${⊢}\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\}=\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\}$
20 18 19 gcdcllem3 ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left(sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\in ℕ\wedge \left(sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\parallel {M}\wedge sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\parallel {N}\right)\wedge \left(\left({K}\in ℤ\wedge {K}\parallel {M}\wedge {K}\parallel {N}\right)\to {K}\le sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\right)\right)$
21 20 simp2d ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left(sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\parallel {M}\wedge sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\parallel {N}\right)$
22 gcdn0val ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to {M}\mathrm{gcd}{N}=sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)$
23 22 breq1d ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}↔sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\parallel {M}\right)$
24 22 breq1d ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left(\left({M}\mathrm{gcd}{N}\right)\parallel {N}↔sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\parallel {N}\right)$
25 23 24 anbi12d ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left(\left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)↔\left(sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\parallel {M}\wedge sup\left(\left\{{n}\in ℤ|\left({n}\parallel {M}\wedge {n}\parallel {N}\right)\right\},ℝ,<\right)\parallel {N}\right)\right)$
26 21 25 mpbird ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to \left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)$
27 17 26 pm2.61dan ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({M}\mathrm{gcd}{N}\right)\parallel {M}\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)$