Theorem negdvdsb

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

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

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
2		znegcl	⊢ ( 𝑀 ∈ ℤ → - 𝑀 ∈ ℤ )
3	2	anim1i	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
4		znegcl	⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ )
5	4	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → - 𝑥 ∈ ℤ )
6		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
7		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
8		mul2neg	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( - 𝑥 · - 𝑀 ) = ( 𝑥 · 𝑀 ) )
9	6 7 8	syl2anr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( - 𝑥 · - 𝑀 ) = ( 𝑥 · 𝑀 ) )
10	9	adantlr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( - 𝑥 · - 𝑀 ) = ( 𝑥 · 𝑀 ) )
11	10	eqeq1d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( - 𝑥 · - 𝑀 ) = 𝑁 ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
12	11	biimprd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑀 ) = 𝑁 → ( - 𝑥 · - 𝑀 ) = 𝑁 ) )
13	1 3 5 12	dvds1lem	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 → - 𝑀 ∥ 𝑁 ) )
14		mulneg12	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( - 𝑥 · 𝑀 ) = ( 𝑥 · - 𝑀 ) )
15	6 7 14	syl2anr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( - 𝑥 · 𝑀 ) = ( 𝑥 · - 𝑀 ) )
16	15	adantlr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( - 𝑥 · 𝑀 ) = ( 𝑥 · - 𝑀 ) )
17	16	eqeq1d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( - 𝑥 · 𝑀 ) = 𝑁 ↔ ( 𝑥 · - 𝑀 ) = 𝑁 ) )
18	17	biimprd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · - 𝑀 ) = 𝑁 → ( - 𝑥 · 𝑀 ) = 𝑁 ) )
19	3 1 5 18	dvds1lem	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 ∥ 𝑁 → 𝑀 ∥ 𝑁 ) )
20	13 19	impbid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ - 𝑀 ∥ 𝑁 ) )