This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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