Metamath Proof Explorer

Theorem addmulmodb

Description: An integer plus a product is itself modulo a positive integer iff the product is divisible by the positive integer. (Contributed by AV, 8-Sep-2025)

		Ref	Expression
	Assertion	addmulmodb	\|- ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( N \|\| ( B x. C ) <-> ( ( A + ( B x. C ) ) mod N ) = ( A mod N ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	\|- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> A e. ZZ )
2	1	zcnd	\|- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> A e. CC )
3	2	adantl	\|- ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> A e. CC )
4		zmulcl	\|- ( ( B e. ZZ /\ C e. ZZ ) -> ( B x. C ) e. ZZ )
5	4	zcnd	\|- ( ( B e. ZZ /\ C e. ZZ ) -> ( B x. C ) e. CC )
6	5	3adant1	\|- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( B x. C ) e. CC )
7	6	adantl	\|- ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( B x. C ) e. CC )
8	3 7	pncan2d	\|- ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( A + ( B x. C ) ) - A ) = ( B x. C ) )
9	8	eqcomd	\|- ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( B x. C ) = ( ( A + ( B x. C ) ) - A ) )
10	9	breq2d	\|- ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( N \|\| ( B x. C ) <-> N \|\| ( ( A + ( B x. C ) ) - A ) ) )
11		simpl	\|- ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> N e. NN )
12	4	3adant1	\|- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( B x. C ) e. ZZ )
13	1 12	zaddcld	\|- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A + ( B x. C ) ) e. ZZ )
14	13	adantl	\|- ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( A + ( B x. C ) ) e. ZZ )
15	1	adantl	\|- ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> A e. ZZ )
16		moddvds	\|- ( ( N e. NN /\ ( A + ( B x. C ) ) e. ZZ /\ A e. ZZ ) -> ( ( ( A + ( B x. C ) ) mod N ) = ( A mod N ) <-> N \|\| ( ( A + ( B x. C ) ) - A ) ) )
17	11 14 15 16	syl3anc	\|- ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( ( A + ( B x. C ) ) mod N ) = ( A mod N ) <-> N \|\| ( ( A + ( B x. C ) ) - A ) ) )
18	10 17	bitr4d	\|- ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( N \|\| ( B x. C ) <-> ( ( A + ( B x. C ) ) mod N ) = ( A mod N ) ) )