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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ( 𝑁 + 𝑀 ) ) )