This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )