Metamath Proof Explorer


Theorem coprmdvds2d

Description: If an integer is divisible by two coprime integers, then it is divisible by their product, a deduction version. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses coprmdvds2d.1 ( 𝜑𝐾 ∈ ℤ )
coprmdvds2d.2 ( 𝜑𝑀 ∈ ℤ )
coprmdvds2d.3 ( 𝜑𝑁 ∈ ℤ )
coprmdvds2d.4 ( 𝜑 → ( 𝐾 gcd 𝑀 ) = 1 )
coprmdvds2d.5 ( 𝜑𝐾𝑁 )
coprmdvds2d.6 ( 𝜑𝑀𝑁 )
Assertion coprmdvds2d ( 𝜑 → ( 𝐾 · 𝑀 ) ∥ 𝑁 )

Proof

Step Hyp Ref Expression
1 coprmdvds2d.1 ( 𝜑𝐾 ∈ ℤ )
2 coprmdvds2d.2 ( 𝜑𝑀 ∈ ℤ )
3 coprmdvds2d.3 ( 𝜑𝑁 ∈ ℤ )
4 coprmdvds2d.4 ( 𝜑 → ( 𝐾 gcd 𝑀 ) = 1 )
5 coprmdvds2d.5 ( 𝜑𝐾𝑁 )
6 coprmdvds2d.6 ( 𝜑𝑀𝑁 )
7 1 2 3 3jca ( 𝜑 → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
8 7 4 jca ( 𝜑 → ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) )
9 coprmdvds2 ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 gcd 𝑀 ) = 1 ) → ( ( 𝐾𝑁𝑀𝑁 ) → ( 𝐾 · 𝑀 ) ∥ 𝑁 ) )
10 8 9 syl ( 𝜑 → ( ( 𝐾𝑁𝑀𝑁 ) → ( 𝐾 · 𝑀 ) ∥ 𝑁 ) )
11 5 6 10 mp2and ( 𝜑 → ( 𝐾 · 𝑀 ) ∥ 𝑁 )