This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 + 𝐵 ) 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 𝑁 ) ) )