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	⊢ ( 𝜑 → 𝑀 ∥ 𝑁 )