This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ordvdsmul

Description: If an integer divides either of two others, it divides their product. (Contributed by Paul Chapman, 17-Nov-2012) (Proof shortened by Mario Carneiro, 17-Jul-2014)

		Ref	Expression
	Assertion	ordvdsmul	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∨ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvdsmultr1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ 𝑀 → 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )
2		dvdsmultr2	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∥ 𝑁 → 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )
3	1 2	jaod	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∨ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( 𝑀 · 𝑁 ) ) )