zdivmul

Description: Property of divisibility: if D divides A then it divides B x. A . (Contributed by NM, 3-Oct-2008)

		Ref	Expression
	Assertion	zdivmul	$⊢ ((D \in ℕ \land A \in ℤ \land B \in ℤ) \land \frac{A}{D} \in ℤ) \to \frac{B A}{D} \in ℤ$

Step	Hyp	Ref	Expression
1		zcn	$⊢ B \in ℤ \to B \in ℂ$
2	1	3ad2ant2	$⊢ (A \in ℤ \land B \in ℤ \land D \in ℕ) \to B \in ℂ$
3		zcn	$⊢ A \in ℤ \to A \in ℂ$
4	3	3ad2ant1	$⊢ (A \in ℤ \land B \in ℤ \land D \in ℕ) \to A \in ℂ$
5		nncn	$⊢ D \in ℕ \to D \in ℂ$
6		nnne0	$⊢ D \in ℕ \to D \neq 0$
7	5 6	jca	$⊢ D \in ℕ \to (D \in ℂ \land D \neq 0)$
8	7	3ad2ant3	$⊢ (A \in ℤ \land B \in ℤ \land D \in ℕ) \to (D \in ℂ \land D \neq 0)$
9		divass	$⊢ (B \in ℂ \land A \in ℂ \land (D \in ℂ \land D \neq 0)) \to \frac{B A}{D} = B (\frac{A}{D})$
10	2 4 8 9	syl3anc	$⊢ (A \in ℤ \land B \in ℤ \land D \in ℕ) \to \frac{B A}{D} = B (\frac{A}{D})$
11	10	3comr	$⊢ (D \in ℕ \land A \in ℤ \land B \in ℤ) \to \frac{B A}{D} = B (\frac{A}{D})$
12	11	adantr	$⊢ ((D \in ℕ \land A \in ℤ \land B \in ℤ) \land \frac{A}{D} \in ℤ) \to \frac{B A}{D} = B (\frac{A}{D})$
13		zmulcl	$⊢ (B \in ℤ \land \frac{A}{D} \in ℤ) \to B (\frac{A}{D}) \in ℤ$
14	13	3ad2antl3	$⊢ ((D \in ℕ \land A \in ℤ \land B \in ℤ) \land \frac{A}{D} \in ℤ) \to B (\frac{A}{D}) \in ℤ$
15	12 14	eqeltrd	$⊢ ((D \in ℕ \land A \in ℤ \land B \in ℤ) \land \frac{A}{D} \in ℤ) \to \frac{B A}{D} \in ℤ$

Metamath Proof Explorer