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	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \lor K ∥ N) \to K ∥ M \cdot N)$

Proof

Step	Hyp	Ref	Expression
1		dvdsmultr1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K ∥ M \to K ∥ M \cdot N)$
2		dvdsmultr2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K ∥ N \to K ∥ M \cdot N)$
3	1 2	jaod	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to ((K ∥ M \lor K ∥ N) \to K ∥ M \cdot N)$