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