Metamath Proof Explorer


Theorem dvdsaddr

Description: An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Assertion dvdsaddr ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀𝑁𝑀 ∥ ( 𝑁 + 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 dvdsadd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀𝑁𝑀 ∥ ( 𝑀 + 𝑁 ) ) )
2 zcn ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
3 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
4 addcom ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑀 + 𝑁 ) = ( 𝑁 + 𝑀 ) )
5 2 3 4 syl2an ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) = ( 𝑁 + 𝑀 ) )
6 5 breq2d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ ( 𝑀 + 𝑁 ) ↔ 𝑀 ∥ ( 𝑁 + 𝑀 ) ) )
7 1 6 bitrd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀𝑁𝑀 ∥ ( 𝑁 + 𝑀 ) ) )