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

Proof

Step Hyp Ref Expression
1 id ⊢M∈ℤ∧N∈ℤ→M∈ℤ∧N∈ℤ
2 znegcl ⊢M∈ℤ→−M∈ℤ
3 2 anim1i ⊢M∈ℤ∧N∈ℤ→−M∈ℤ∧N∈ℤ
4 znegcl ⊢x∈ℤ→−x∈ℤ
5 4 adantl ⊢M∈ℤ∧N∈ℤ∧x∈ℤ→−x∈ℤ
6 zcn ⊢x∈ℤ→x∈ℂ
7 zcn ⊢M∈ℤ→M∈ℂ
8 mul2neg ⊢x∈ℂ∧M∈ℂ→−x⁢- M=x⋅ M
9 6 7 8 syl2anr ⊢M∈ℤ∧x∈ℤ→−x⁢- M=x⋅ M
10 9 adantlr ⊢M∈ℤ∧N∈ℤ∧x∈ℤ→−x⁢- M=x⋅ M
11 10 eqeq1d ⊢M∈ℤ∧N∈ℤ∧x∈ℤ→−x⁢- M=N↔x⋅ M=N
12 11 biimprd ⊢M∈ℤ∧N∈ℤ∧x∈ℤ→x⋅ M=N→−x⁢- M=N
13 1 3 5 12 dvds1lem ⊢M∈ℤ∧N∈ℤ→M∥N→- M∥N
14 mulneg12 ⊢x∈ℂ∧M∈ℂ→−x⋅ M=x⁢- M
15 6 7 14 syl2anr ⊢M∈ℤ∧x∈ℤ→−x⋅ M=x⁢- M
16 15 adantlr ⊢M∈ℤ∧N∈ℤ∧x∈ℤ→−x⋅ M=x⁢- M
17 16 eqeq1d ⊢M∈ℤ∧N∈ℤ∧x∈ℤ→−x⋅ M=N↔x⁢- M=N
18 17 biimprd ⊢M∈ℤ∧N∈ℤ∧x∈ℤ→x⁢- M=N→−x⋅ M=N
19 3 1 5 18 dvds1lem ⊢M∈ℤ∧N∈ℤ→- M∥N→M∥N
20 13 19 impbid ⊢M∈ℤ∧N∈ℤ→M∥N↔- M∥N