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

Metamath Proof Explorer

Theorem negdvdsb

Description: An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion negdvdsb ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ - 𝑀 ∥ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
2 znegcl ⊢ ( 𝑀 ∈ ℤ → - 𝑀 ∈ ℤ )
3 2 anim1i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
4 znegcl ⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ )
5 4 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → - 𝑥 ∈ ℤ )
6 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
7 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
8 mul2neg ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( - 𝑥 · - 𝑀 ) = ( 𝑥 · 𝑀 ) )
9 6 7 8 syl2anr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( - 𝑥 · - 𝑀 ) = ( 𝑥 · 𝑀 ) )
10 9 adantlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( - 𝑥 · - 𝑀 ) = ( 𝑥 · 𝑀 ) )
11 10 eqeq1d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( - 𝑥 · - 𝑀 ) = 𝑁 ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
12 11 biimprd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑀 ) = 𝑁 → ( - 𝑥 · - 𝑀 ) = 𝑁 ) )
13 1 3 5 12 dvds1lem ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 → - 𝑀 ∥ 𝑁 ) )
14 mulneg12 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( - 𝑥 · 𝑀 ) = ( 𝑥 · - 𝑀 ) )
15 6 7 14 syl2anr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( - 𝑥 · 𝑀 ) = ( 𝑥 · - 𝑀 ) )
16 15 adantlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( - 𝑥 · 𝑀 ) = ( 𝑥 · - 𝑀 ) )
17 16 eqeq1d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( - 𝑥 · 𝑀 ) = 𝑁 ↔ ( 𝑥 · - 𝑀 ) = 𝑁 ) )
18 17 biimprd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · - 𝑀 ) = 𝑁 → ( - 𝑥 · 𝑀 ) = 𝑁 ) )
19 3 1 5 18 dvds1lem ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 ∥ 𝑁 → 𝑀 ∥ 𝑁 ) )
20 13 19 impbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ - 𝑀 ∥ 𝑁 ) )