Metamath Proof Explorer

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 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ N ∈ ℕ → A + B mod N = 0 ↔ A mod N = − B mod N

Proof

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