Theorem addmodidr

Description: The sum of a positive integer and a nonnegative integer less than the positive integer is equal to the nonnegative integer modulo the positive integer. (Contributed by AV, 19-Mar-2021)

	Ref	Expression
Assertion	addmodidr	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> ( ( A + M ) mod M ) = A )

Proof

Step	Hyp	Ref	Expression
1		nn0cn	|- ( A e. NN0 -> A e. CC )
2		nncn	|- ( M e. NN -> M e. CC )
3		addcom	|- ( ( A e. CC /\ M e. CC ) -> ( A + M ) = ( M + A ) )
4	1 2 3	syl2an	|- ( ( A e. NN0 /\ M e. NN ) -> ( A + M ) = ( M + A ) )
5	4	3adant3	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> ( A + M ) = ( M + A ) )
6	5	oveq1d	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> ( ( A + M ) mod M ) = ( ( M + A ) mod M ) )
7		addmodid	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> ( ( M + A ) mod M ) = A )
8	6 7	eqtrd	|- ( ( A e. NN0 /\ M e. NN /\ A < M ) -> ( ( A + M ) mod M ) = A )