Metamath Proof Explorer


Theorem muldvds2d

Description: If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses muldvds2d.1 ( 𝜑𝐾 ∈ ℤ )
muldvds2d.2 ( 𝜑𝑀 ∈ ℤ )
muldvds2d.3 ( 𝜑𝑁 ∈ ℤ )
muldvds2d.4 ( 𝜑 → ( 𝐾 · 𝑀 ) ∥ 𝑁 )
Assertion muldvds2d ( 𝜑𝑀𝑁 )

Proof

Step Hyp Ref Expression
1 muldvds2d.1 ( 𝜑𝐾 ∈ ℤ )
2 muldvds2d.2 ( 𝜑𝑀 ∈ ℤ )
3 muldvds2d.3 ( 𝜑𝑁 ∈ ℤ )
4 muldvds2d.4 ( 𝜑 → ( 𝐾 · 𝑀 ) ∥ 𝑁 )
5 1 2 3 3jca ( 𝜑 → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
6 muldvds2 ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) ∥ 𝑁𝑀𝑁 ) )
7 5 4 6 sylc ( 𝜑𝑀𝑁 )