Theorem muldvds1d

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	muldvds1d.1	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
	muldvds1d.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	muldvds1d.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	muldvds1d.4	⊢ ( 𝜑 → ( 𝐾 · 𝑀 ) ∥ 𝑁 )
Assertion	muldvds1d	⊢ ( 𝜑 → 𝐾 ∥ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		muldvds1d.1	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2		muldvds1d.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		muldvds1d.3	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4		muldvds1d.4	⊢ ( 𝜑 → ( 𝐾 · 𝑀 ) ∥ 𝑁 )
5	1 2 3	3jca	⊢ ( 𝜑 → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
6		muldvds1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) ∥ 𝑁 → 𝐾 ∥ 𝑁 ) )
7	5 6	syl	⊢ ( 𝜑 → ( ( 𝐾 · 𝑀 ) ∥ 𝑁 → 𝐾 ∥ 𝑁 ) )
8	4 7	mpd	⊢ ( 𝜑 → 𝐾 ∥ 𝑁 )