# Metamath Proof Explorer

## Theorem dvdsgcdb

Description: Biconditional form of dvdsgcd . (Contributed by Scott Fenton, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion dvdsgcdb ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({K}\parallel {M}\wedge {K}\parallel {N}\right)↔{K}\parallel \left({M}\mathrm{gcd}{N}\right)\right)$

### Proof

Step Hyp Ref Expression
1 dvdsgcd ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({K}\parallel {M}\wedge {K}\parallel {N}\right)\to {K}\parallel \left({M}\mathrm{gcd}{N}\right)\right)$
2 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)$
3 2 simpld ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\mathrm{gcd}{N}\right)\parallel {M}$
4 3 3adant1 ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\mathrm{gcd}{N}\right)\parallel {M}$
5 simp1 ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to {K}\in ℤ$
6 gcdcl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\mathrm{gcd}{N}\in {ℕ}_{0}$
7 6 nn0zd ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\mathrm{gcd}{N}\in ℤ$
8 7 3adant1 ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\mathrm{gcd}{N}\in ℤ$
9 simp2 ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\in ℤ$
10 dvdstr ${⊢}\left({K}\in ℤ\wedge {M}\mathrm{gcd}{N}\in ℤ\wedge {M}\in ℤ\right)\to \left(\left({K}\parallel \left({M}\mathrm{gcd}{N}\right)\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {M}\right)\to {K}\parallel {M}\right)$
11 5 8 9 10 syl3anc ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({K}\parallel \left({M}\mathrm{gcd}{N}\right)\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {M}\right)\to {K}\parallel {M}\right)$
12 4 11 mpan2d ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\parallel \left({M}\mathrm{gcd}{N}\right)\to {K}\parallel {M}\right)$
13 2 simprd ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\mathrm{gcd}{N}\right)\parallel {N}$
14 13 3adant1 ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\mathrm{gcd}{N}\right)\parallel {N}$
15 dvdstr ${⊢}\left({K}\in ℤ\wedge {M}\mathrm{gcd}{N}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({K}\parallel \left({M}\mathrm{gcd}{N}\right)\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)\to {K}\parallel {N}\right)$
16 8 15 syld3an2 ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({K}\parallel \left({M}\mathrm{gcd}{N}\right)\wedge \left({M}\mathrm{gcd}{N}\right)\parallel {N}\right)\to {K}\parallel {N}\right)$
17 14 16 mpan2d ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\parallel \left({M}\mathrm{gcd}{N}\right)\to {K}\parallel {N}\right)$
18 12 17 jcad ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\parallel \left({M}\mathrm{gcd}{N}\right)\to \left({K}\parallel {M}\wedge {K}\parallel {N}\right)\right)$
19 1 18 impbid ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({K}\parallel {M}\wedge {K}\parallel {N}\right)↔{K}\parallel \left({M}\mathrm{gcd}{N}\right)\right)$