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	\|- ( ( 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 ) ) )