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 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ N ↔ M ∥ -N

Proof

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