Metamath Proof Explorer

Theorem 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 ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ A D ∈ ℤ → B ⁢ A D ∈ ℤ

Proof

Step Hyp Ref Expression
1 zcn ⊢ B ∈ ℤ → B ∈ ℂ
2 1 3ad2ant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ D ∈ ℕ → B ∈ ℂ
3 zcn ⊢ A ∈ ℤ → A ∈ ℂ
4 3 3ad2ant1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ D ∈ ℕ → A ∈ ℂ
5 nncn ⊢ D ∈ ℕ → D ∈ ℂ
6 nnne0 ⊢ D ∈ ℕ → D ≠ 0
7 5 6 jca ⊢ D ∈ ℕ → D ∈ ℂ ∧ D ≠ 0
8 7 3ad2ant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ D ∈ ℕ → D ∈ ℂ ∧ D ≠ 0
9 divass ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → B ⁢ A D = B ⁢ A D
10 2 4 8 9 syl3anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ D ∈ ℕ → B ⁢ A D = B ⁢ A D
11 10 3comr ⊢ D ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ → B ⁢ A D = B ⁢ A D
12 11 adantr ⊢ D ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ A D ∈ ℤ → B ⁢ A D = B ⁢ A D
13 zmulcl ⊢ B ∈ ℤ ∧ A D ∈ ℤ → B ⁢ A D ∈ ℤ
14 13 3ad2antl3 ⊢ D ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ A D ∈ ℤ → B ⁢ A D ∈ ℤ
15 12 14 eqeltrd ⊢ D ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ A D ∈ ℤ → B ⁢ A D ∈ ℤ