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 A0MA<MA+MmodM=A

Proof

Step Hyp Ref Expression
1 nn0cn A0A
2 nncn MM
3 addcom AMA+M=M+A
4 1 2 3 syl2an A0MA+M=M+A
5 4 3adant3 A0MA<MA+M=M+A
6 5 oveq1d A0MA<MA+MmodM=M+AmodM
7 addmodid A0MA<MM+AmodM=A
8 6 7 eqtrd A0MA<MA+MmodM=A