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 
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || N ) <-> K || ( M gcd N ) ) )

Proof

Step Hyp Ref Expression
1 dvdsgcd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || N ) -> K || ( M gcd N ) ) )
2 gcddvds 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
3 2 simpld 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) || M )
4 3 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) || M )
5 simp1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> K e. ZZ )
6 gcdcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )
7 6 nn0zd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. ZZ )
8 7 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. ZZ )
9 simp2 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> M e. ZZ )
10 dvdstr 
 |-  ( ( K e. ZZ /\ ( M gcd N ) e. ZZ /\ M e. ZZ ) -> ( ( K || ( M gcd N ) /\ ( M gcd N ) || M ) -> K || M ) )
11 5 8 9 10 syl3anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || ( M gcd N ) /\ ( M gcd N ) || M ) -> K || M ) )
12 4 11 mpan2d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || ( M gcd N ) -> K || M ) )
13 2 simprd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) || N )
14 13 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) || N )
15 dvdstr 
 |-  ( ( K e. ZZ /\ ( M gcd N ) e. ZZ /\ N e. ZZ ) -> ( ( K || ( M gcd N ) /\ ( M gcd N ) || N ) -> K || N ) )
16 8 15 syld3an2 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || ( M gcd N ) /\ ( M gcd N ) || N ) -> K || N ) )
17 14 16 mpan2d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || ( M gcd N ) -> K || N ) )
18 12 17 jcad 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || ( M gcd N ) -> ( K || M /\ K || N ) ) )
19 1 18 impbid 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || N ) <-> K || ( M gcd N ) ) )