Theorem dvdsnegb

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

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

Proof

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