Metamath Proof Explorer

Theorem coprmdvds2

Description: If an integer is divisible by two coprime integers, then it is divisible by their product. (Contributed by Mario Carneiro, 24-Feb-2014)

Ref Expression
Assertion coprmdvds2 
|- ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( M || K /\ N || K ) -> ( M x. N ) || K ) )

Proof

Step Hyp Ref Expression
1 divides 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N || K <-> E. x e. ZZ ( x x. N ) = K ) )
2 1 3adant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( N || K <-> E. x e. ZZ ( x x. N ) = K ) )
3 2 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( N || K <-> E. x e. ZZ ( x x. N ) = K ) )
4 simprr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( ( M gcd N ) = 1 /\ x e. ZZ ) ) -> x e. ZZ )
5 simpl2 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( ( M gcd N ) = 1 /\ x e. ZZ ) ) -> N e. ZZ )
6 zcn 
 |-  ( x e. ZZ -> x e. CC )
7 zcn 
 |-  ( N e. ZZ -> N e. CC )
8 mulcom 
 |-  ( ( x e. CC /\ N e. CC ) -> ( x x. N ) = ( N x. x ) )
9 6 7 8 syl2an 
 |-  ( ( x e. ZZ /\ N e. ZZ ) -> ( x x. N ) = ( N x. x ) )
10 4 5 9 syl2anc 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( ( M gcd N ) = 1 /\ x e. ZZ ) ) -> ( x x. N ) = ( N x. x ) )
11 10 breq2d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( ( M gcd N ) = 1 /\ x e. ZZ ) ) -> ( M || ( x x. N ) <-> M || ( N x. x ) ) )
12 simprl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( ( M gcd N ) = 1 /\ x e. ZZ ) ) -> ( M gcd N ) = 1 )
13 simpl1 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( ( M gcd N ) = 1 /\ x e. ZZ ) ) -> M e. ZZ )
14 coprmdvds 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ x e. ZZ ) -> ( ( M || ( N x. x ) /\ ( M gcd N ) = 1 ) -> M || x ) )
15 13 5 4 14 syl3anc 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( ( M gcd N ) = 1 /\ x e. ZZ ) ) -> ( ( M || ( N x. x ) /\ ( M gcd N ) = 1 ) -> M || x ) )
16 12 15 mpan2d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( ( M gcd N ) = 1 /\ x e. ZZ ) ) -> ( M || ( N x. x ) -> M || x ) )
17 11 16 sylbid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( ( M gcd N ) = 1 /\ x e. ZZ ) ) -> ( M || ( x x. N ) -> M || x ) )
18 dvdsmulc 
 |-  ( ( M e. ZZ /\ x e. ZZ /\ N e. ZZ ) -> ( M || x -> ( M x. N ) || ( x x. N ) ) )
19 13 4 5 18 syl3anc 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( ( M gcd N ) = 1 /\ x e. ZZ ) ) -> ( M || x -> ( M x. N ) || ( x x. N ) ) )
20 17 19 syld 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( ( M gcd N ) = 1 /\ x e. ZZ ) ) -> ( M || ( x x. N ) -> ( M x. N ) || ( x x. N ) ) )
21 breq2 
 |-  ( ( x x. N ) = K -> ( M || ( x x. N ) <-> M || K ) )
22 breq2 
 |-  ( ( x x. N ) = K -> ( ( M x. N ) || ( x x. N ) <-> ( M x. N ) || K ) )
23 21 22 imbi12d 
 |-  ( ( x x. N ) = K -> ( ( M || ( x x. N ) -> ( M x. N ) || ( x x. N ) ) <-> ( M || K -> ( M x. N ) || K ) ) )
24 20 23 syl5ibcom 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( ( M gcd N ) = 1 /\ x e. ZZ ) ) -> ( ( x x. N ) = K -> ( M || K -> ( M x. N ) || K ) ) )
25 24 anassrs 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M gcd N ) = 1 ) /\ x e. ZZ ) -> ( ( x x. N ) = K -> ( M || K -> ( M x. N ) || K ) ) )
26 25 rexlimdva 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( E. x e. ZZ ( x x. N ) = K -> ( M || K -> ( M x. N ) || K ) ) )
27 3 26 sylbid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( N || K -> ( M || K -> ( M x. N ) || K ) ) )
28 27 impcomd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( ( M || K /\ N || K ) -> ( M x. N ) || K ) )