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

Metamath Proof Explorer

Theorem dvdsnegb

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

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

Proof

Step Hyp Ref Expression
1 id ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
2 znegcl ⊢ ( 𝑁 ∈ ℤ → - 𝑁 ∈ ℤ )
3 2 anim2i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ℤ ∧ - 𝑁 ∈ ℤ ) )
4 znegcl ⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ )
5 4 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → - 𝑥 ∈ ℤ )
6 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
7 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
8 mulneg1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( - 𝑥 · 𝑀 ) = - ( 𝑥 · 𝑀 ) )
9 negeq ⊢ ( ( 𝑥 · 𝑀 ) = 𝑁 → - ( 𝑥 · 𝑀 ) = - 𝑁 )
10 9 eqeq2d ⊢ ( ( 𝑥 · 𝑀 ) = 𝑁 → ( ( - 𝑥 · 𝑀 ) = - ( 𝑥 · 𝑀 ) ↔ ( - 𝑥 · 𝑀 ) = - 𝑁 ) )
11 8 10 syl5ibcom ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑥 · 𝑀 ) = 𝑁 → ( - 𝑥 · 𝑀 ) = - 𝑁 ) )
12 6 7 11 syl2anr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑀 ) = 𝑁 → ( - 𝑥 · 𝑀 ) = - 𝑁 ) )
13 12 adantlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑀 ) = 𝑁 → ( - 𝑥 · 𝑀 ) = - 𝑁 ) )
14 1 3 5 13 dvds1lem ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 → 𝑀 ∥ - 𝑁 ) )
15 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
16 negeq ⊢ ( ( 𝑥 · 𝑀 ) = - 𝑁 → - ( 𝑥 · 𝑀 ) = - - 𝑁 )
17 negneg ⊢ ( 𝑁 ∈ ℂ → - - 𝑁 = 𝑁 )
18 16 17 sylan9eqr ⊢ ( ( 𝑁 ∈ ℂ ∧ ( 𝑥 · 𝑀 ) = - 𝑁 ) → - ( 𝑥 · 𝑀 ) = 𝑁 )
19 8 18 sylan9eq ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ ( 𝑁 ∈ ℂ ∧ ( 𝑥 · 𝑀 ) = - 𝑁 ) ) → ( - 𝑥 · 𝑀 ) = 𝑁 )
20 19 expr ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ 𝑁 ∈ ℂ ) → ( ( 𝑥 · 𝑀 ) = - 𝑁 → ( - 𝑥 · 𝑀 ) = 𝑁 ) )
21 20 3impa ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑥 · 𝑀 ) = - 𝑁 → ( - 𝑥 · 𝑀 ) = 𝑁 ) )
22 6 7 15 21 syl3an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑥 · 𝑀 ) = - 𝑁 → ( - 𝑥 · 𝑀 ) = 𝑁 ) )
23 22 3coml ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑀 ) = - 𝑁 → ( - 𝑥 · 𝑀 ) = 𝑁 ) )
24 23 3expa ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑀 ) = - 𝑁 → ( - 𝑥 · 𝑀 ) = 𝑁 ) )
25 3 1 5 24 dvds1lem ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ - 𝑁 → 𝑀 ∥ 𝑁 ) )
26 14 25 impbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ 𝑀 ∥ - 𝑁 ) )