Theorem summodnegmod

Description: The sum of two integers modulo a positive integer equals zero iff the first of the two integers equals the negative of the other integer modulo the positive integer. (Contributed by AV, 25-Jul-2021)

	Ref	Expression
Assertion	summodnegmod	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 + 𝐵 ) mod 𝑁 ) = 0 ↔ ( 𝐴 mod 𝑁 ) = ( - 𝐵 mod 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
2		simp1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℤ )
3		znegcl	⊢ ( 𝐵 ∈ ℤ → - 𝐵 ∈ ℤ )
4	3	3ad2ant2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → - 𝐵 ∈ ℤ )
5		moddvds	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ - 𝐵 ∈ ℤ ) → ( ( 𝐴 mod 𝑁 ) = ( - 𝐵 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝐴 − - 𝐵 ) ) )
6	1 2 4 5	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) = ( - 𝐵 mod 𝑁 ) ↔ 𝑁 ∥ ( 𝐴 − - 𝐵 ) ) )
7		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
8		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
9	7 8	anim12i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
10	9	3adant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
11		subneg	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − - 𝐵 ) = ( 𝐴 + 𝐵 ) )
12	11	eqcomd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) = ( 𝐴 − - 𝐵 ) )
13	10 12	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 + 𝐵 ) = ( 𝐴 − - 𝐵 ) )
14	13	breq2d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∥ ( 𝐴 + 𝐵 ) ↔ 𝑁 ∥ ( 𝐴 − - 𝐵 ) ) )
15		zaddcl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
16	15	3adant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
17		dvdsval3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 + 𝐵 ) ∈ ℤ ) → ( 𝑁 ∥ ( 𝐴 + 𝐵 ) ↔ ( ( 𝐴 + 𝐵 ) mod 𝑁 ) = 0 ) )
18	1 16 17	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∥ ( 𝐴 + 𝐵 ) ↔ ( ( 𝐴 + 𝐵 ) mod 𝑁 ) = 0 ) )
19	6 14 18	3bitr2rd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 + 𝐵 ) mod 𝑁 ) = 0 ↔ ( 𝐴 mod 𝑁 ) = ( - 𝐵 mod 𝑁 ) ) )