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 ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝑀𝐾𝑁𝐾 ) → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 divides ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁𝐾 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝑁 ) = 𝐾 ) )
2 1 3adant1 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁𝐾 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝑁 ) = 𝐾 ) )
3 2 adantr ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑁𝐾 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝑁 ) = 𝐾 ) )
4 simprr ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
5 simpl2 ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
6 zcn ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
7 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
8 mulcom ( ( 𝑥 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑥 · 𝑁 ) = ( 𝑁 · 𝑥 ) )
9 6 7 8 syl2an ( ( 𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑥 · 𝑁 ) = ( 𝑁 · 𝑥 ) )
10 4 5 9 syl2anc ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑥 · 𝑁 ) = ( 𝑁 · 𝑥 ) )
11 10 breq2d ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑀 ∥ ( 𝑥 · 𝑁 ) ↔ 𝑀 ∥ ( 𝑁 · 𝑥 ) ) )
12 simprl ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑀 gcd 𝑁 ) = 1 )
13 simpl1 ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
14 coprmdvds ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( 𝑀 ∥ ( 𝑁 · 𝑥 ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝑀𝑥 ) )
15 13 5 4 14 syl3anc ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( ( 𝑀 ∥ ( 𝑁 · 𝑥 ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝑀𝑥 ) )
16 12 15 mpan2d ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑀 ∥ ( 𝑁 · 𝑥 ) → 𝑀𝑥 ) )
17 11 16 sylbid ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑀 ∥ ( 𝑥 · 𝑁 ) → 𝑀𝑥 ) )
18 dvdsmulc ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀𝑥 → ( 𝑀 · 𝑁 ) ∥ ( 𝑥 · 𝑁 ) ) )
19 13 4 5 18 syl3anc ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑀𝑥 → ( 𝑀 · 𝑁 ) ∥ ( 𝑥 · 𝑁 ) ) )
20 17 19 syld ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑀 ∥ ( 𝑥 · 𝑁 ) → ( 𝑀 · 𝑁 ) ∥ ( 𝑥 · 𝑁 ) ) )
21 breq2 ( ( 𝑥 · 𝑁 ) = 𝐾 → ( 𝑀 ∥ ( 𝑥 · 𝑁 ) ↔ 𝑀𝐾 ) )
22 breq2 ( ( 𝑥 · 𝑁 ) = 𝐾 → ( ( 𝑀 · 𝑁 ) ∥ ( 𝑥 · 𝑁 ) ↔ ( 𝑀 · 𝑁 ) ∥ 𝐾 ) )
23 21 22 imbi12d ( ( 𝑥 · 𝑁 ) = 𝐾 → ( ( 𝑀 ∥ ( 𝑥 · 𝑁 ) → ( 𝑀 · 𝑁 ) ∥ ( 𝑥 · 𝑁 ) ) ↔ ( 𝑀𝐾 → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) ) )
24 20 23 syl5ibcom ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( ( 𝑥 · 𝑁 ) = 𝐾 → ( 𝑀𝐾 → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) ) )
25 24 anassrs ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑁 ) = 𝐾 → ( 𝑀𝐾 → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) ) )
26 25 rexlimdva ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝑁 ) = 𝐾 → ( 𝑀𝐾 → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) ) )
27 3 26 sylbid ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑁𝐾 → ( 𝑀𝐾 → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) ) )
28 27 impcomd ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝑀𝐾𝑁𝐾 ) → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) )