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∈ℤ∧AD∈ℤ∧BD∈ℤ→A+BD∈ℤ

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+BD=AD+BD
7 1 2 5 6 syl3an ⊢A∈ℤ∧B∈ℤ∧D∈ℕ→A+BD=AD+BD
8 7 3comr ⊢D∈ℕ∧A∈ℤ∧B∈ℤ→A+BD=AD+BD
9 8 adantr ⊢D∈ℕ∧A∈ℤ∧B∈ℤ∧AD∈ℤ∧BD∈ℤ→A+BD=AD+BD
10 zaddcl ⊢AD∈ℤ∧BD∈ℤ→AD+BD∈ℤ
11 10 adantl ⊢D∈ℕ∧A∈ℤ∧B∈ℤ∧AD∈ℤ∧BD∈ℤ→AD+BD∈ℤ
12 9 11 eqeltrd ⊢D∈ℕ∧A∈ℤ∧B∈ℤ∧AD∈ℤ∧BD∈ℤ→A+BD∈ℤ