Theorem dvdsadd

Description: An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 13-Jul-2014)

	Ref	Expression
Assertion	dvdsadd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ( 𝑀 + 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℤ )
2		zaddcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
3		simpr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
4		iddvds	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∥ 𝑀 )
5	4	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∥ 𝑀 )
6		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
7		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
8		pncan	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
9	6 7 8	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
10	5 9	breqtrrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∥ ( ( 𝑀 + 𝑁 ) − 𝑁 ) )
11		dvdssub2	⊢ ( ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ∥ ( ( 𝑀 + 𝑁 ) − 𝑁 ) ) → ( 𝑀 ∥ ( 𝑀 + 𝑁 ) ↔ 𝑀 ∥ 𝑁 ) )
12	1 2 3 10 11	syl31anc	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ ( 𝑀 + 𝑁 ) ↔ 𝑀 ∥ 𝑁 ) )
13	12	bicomd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ( 𝑀 + 𝑁 ) ) )