Metamath Proof Explorer

Theorem zdivadd

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

Ref Expression
Assertion zdivadd ⊢ D ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ A D ∈ ℤ ∧ B D ∈ ℤ → A + B D ∈ ℤ

Proof

Step Hyp Ref Expression
1 zcn ⊢ A ∈ ℤ → A ∈ ℂ
2 zcn ⊢ B ∈ ℤ → B ∈ ℂ
3 nncn ⊢ D ∈ ℕ → D ∈ ℂ
4 nnne0 ⊢ D ∈ ℕ → D ≠ 0
5 3 4 jca ⊢ D ∈ ℕ → D ∈ ℂ ∧ D ≠ 0
6 divdir ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → A + B D = A D + B D
7 1 2 5 6 syl3an ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ D ∈ ℕ → A + B D = A D + B D
8 7 3comr ⊢ D ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ → A + B D = A D + B D
9 8 adantr ⊢ D ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ A D ∈ ℤ ∧ B D ∈ ℤ → A + B D = A D + B D
10 zaddcl ⊢ A D ∈ ℤ ∧ B D ∈ ℤ → A D + B D ∈ ℤ
11 10 adantl ⊢ D ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ A D ∈ ℤ ∧ B D ∈ ℤ → A D + B D ∈ ℤ
12 9 11 eqeltrd ⊢ D ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ A D ∈ ℤ ∧ B D ∈ ℤ → A + B D ∈ ℤ