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 ABNA+BmodN=0AmodN=BmodN

Proof

Step Hyp Ref Expression
1 simp3 ABNN
2 simp1 ABNA
3 znegcl BB
4 3 3ad2ant2 ABNB
5 moddvds NABAmodN=BmodNNAB
6 1 2 4 5 syl3anc ABNAmodN=BmodNNAB
7 zcn AA
8 zcn BB
9 7 8 anim12i ABAB
10 9 3adant3 ABNAB
11 subneg ABAB=A+B
12 11 eqcomd ABA+B=AB
13 10 12 syl ABNA+B=AB
14 13 breq2d ABNNA+BNAB
15 zaddcl ABA+B
16 15 3adant3 ABNA+B
17 dvdsval3 NA+BNA+BA+BmodN=0
18 1 16 17 syl2anc ABNNA+BA+BmodN=0
19 6 14 18 3bitr2rd ABNA+BmodN=0AmodN=BmodN