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