# Metamath Proof Explorer

## Theorem dvdsgcd

Description: An integer which divides each of two others also divides their gcd. (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 30-May-2014)

Ref Expression
Assertion dvdsgcd
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || N ) -> K || ( M gcd N ) ) )

### Proof

Step Hyp Ref Expression
1 bezout
|-  ( ( M e. ZZ /\ N e. ZZ ) -> E. x e. ZZ E. y e. ZZ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) )
|-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> E. x e. ZZ E. y e. ZZ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) )
3 dvds2ln
|-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) ) -> ( ( K || M /\ K || N ) -> K || ( ( x x. M ) + ( y x. N ) ) ) )
4 3 3impia
|-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) ) -> K || ( ( x x. M ) + ( y x. N ) ) )
5 4 3coml
|-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> K || ( ( x x. M ) + ( y x. N ) ) )
6 simp3l
|-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> x e. ZZ )
7 simp12
|-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> M e. ZZ )
8 zcn
|-  ( x e. ZZ -> x e. CC )
9 zcn
|-  ( M e. ZZ -> M e. CC )
10 mulcom
|-  ( ( x e. CC /\ M e. CC ) -> ( x x. M ) = ( M x. x ) )
11 8 9 10 syl2an
|-  ( ( x e. ZZ /\ M e. ZZ ) -> ( x x. M ) = ( M x. x ) )
12 6 7 11 syl2anc
|-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x x. M ) = ( M x. x ) )
13 simp3r
|-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> y e. ZZ )
14 simp13
|-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> N e. ZZ )
15 zcn
|-  ( y e. ZZ -> y e. CC )
16 zcn
|-  ( N e. ZZ -> N e. CC )
17 mulcom
|-  ( ( y e. CC /\ N e. CC ) -> ( y x. N ) = ( N x. y ) )
18 15 16 17 syl2an
|-  ( ( y e. ZZ /\ N e. ZZ ) -> ( y x. N ) = ( N x. y ) )
19 13 14 18 syl2anc
|-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( y x. N ) = ( N x. y ) )
20 12 19 oveq12d
|-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x x. M ) + ( y x. N ) ) = ( ( M x. x ) + ( N x. y ) ) )
21 5 20 breqtrd
|-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> K || ( ( M x. x ) + ( N x. y ) ) )
22 breq2
|-  ( ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) -> ( K || ( M gcd N ) <-> K || ( ( M x. x ) + ( N x. y ) ) ) )
23 21 22 syl5ibrcom
|-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) -> K || ( M gcd N ) ) )
24 23 3expia
|-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) ) -> ( ( x e. ZZ /\ y e. ZZ ) -> ( ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) -> K || ( M gcd N ) ) ) )
25 24 rexlimdvv
|-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K || M /\ K || N ) ) -> ( E. x e. ZZ E. y e. ZZ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) -> K || ( M gcd N ) ) )
26 25 ex
|-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || N ) -> ( E. x e. ZZ E. y e. ZZ ( M gcd N ) = ( ( M x. x ) + ( N x. y ) ) -> K || ( M gcd N ) ) ) )
27 2 26 mpid
|-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || N ) -> K || ( M gcd N ) ) )