Metamath Proof Explorer


Theorem modadd2mod

Description: The sum of a real number modulo a positive real number and another real number equals the sum of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018)

Ref Expression
Assertion modadd2mod ABM+B+AmodMmodM=B+AmodM

Proof

Step Hyp Ref Expression
1 recn BB
2 1 3ad2ant2 ABM+B
3 modcl AM+AmodM
4 3 recnd AM+AmodM
5 4 3adant2 ABM+AmodM
6 2 5 addcomd ABM+B+AmodM=AmodM+B
7 6 oveq1d ABM+B+AmodMmodM=AmodM+BmodM
8 modaddmod ABM+AmodM+BmodM=A+BmodM
9 recn AA
10 addcom ABA+B=B+A
11 9 1 10 syl2an ABA+B=B+A
12 11 oveq1d ABA+BmodM=B+AmodM
13 12 3adant3 ABM+A+BmodM=B+AmodM
14 7 8 13 3eqtrd ABM+B+AmodMmodM=B+AmodM