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