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 e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( ( A + B ) mod N ) = 0 <-> ( A mod N ) = ( -u B mod N ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> N e. NN )
2		simp1	|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> A e. ZZ )
3		znegcl	|- ( B e. ZZ -> -u B e. ZZ )
4	3	3ad2ant2	|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> -u B e. ZZ )
5		moddvds	|- ( ( N e. NN /\ A e. ZZ /\ -u B e. ZZ ) -> ( ( A mod N ) = ( -u B mod N ) <-> N || ( A - -u B ) ) )
6	1 2 4 5	syl3anc	|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( A mod N ) = ( -u B mod N ) <-> N || ( A - -u B ) ) )
7		zcn	|- ( A e. ZZ -> A e. CC )
8		zcn	|- ( B e. ZZ -> B e. CC )
9	7 8	anim12i	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A e. CC /\ B e. CC ) )
10	9	3adant3	|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( A e. CC /\ B e. CC ) )
11		subneg	|- ( ( A e. CC /\ B e. CC ) -> ( A - -u B ) = ( A + B ) )
12	11	eqcomd	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( A - -u B ) )
13	10 12	syl	|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( A + B ) = ( A - -u B ) )
14	13	breq2d	|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( N || ( A + B ) <-> N || ( A - -u B ) ) )
15		zaddcl	|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. ZZ )
16	15	3adant3	|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( A + B ) e. ZZ )
17		dvdsval3	|- ( ( N e. NN /\ ( A + B ) e. ZZ ) -> ( N || ( A + B ) <-> ( ( A + B ) mod N ) = 0 ) )
18	1 16 17	syl2anc	|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( N || ( A + B ) <-> ( ( A + B ) mod N ) = 0 ) )
19	6 14 18	3bitr2rd	|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( ( A + B ) mod N ) = 0 <-> ( A mod N ) = ( -u B mod N ) ) )