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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recn | |
|
2 | 1 | 3ad2ant2 | |
3 | modcl | |
|
4 | 3 | recnd | |
5 | 4 | 3adant2 | |
6 | 2 5 | addcomd | |
7 | 6 | oveq1d | |
8 | modaddmod | |
|
9 | recn | |
|
10 | addcom | |
|
11 | 9 1 10 | syl2an | |
12 | 11 | oveq1d | |
13 | 12 | 3adant3 | |
14 | 7 8 13 | 3eqtrd | |