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