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 ) ) )
2 1 3adant1 
 |-  ( ( 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 ) ) )