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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 | |
|
2 | simp1 | |
|
3 | znegcl | |
|
4 | 3 | 3ad2ant2 | |
5 | moddvds | |
|
6 | 1 2 4 5 | syl3anc | |
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 | |
|
18 | 1 16 17 | syl2anc | |
19 | 6 14 18 | 3bitr2rd | |