# Metamath Proof Explorer

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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({B}+\left({A}\mathrm{mod}{M}\right)\right)\mathrm{mod}{M}=\left({B}+{A}\right)\mathrm{mod}{M}$

### Proof

Step Hyp Ref Expression
1 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
2 1 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {B}\in ℂ$
3 modcl ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{M}\in ℝ$
4 3 recnd ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{M}\in ℂ$
5 4 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{M}\in ℂ$
6 2 5 addcomd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {B}+\left({A}\mathrm{mod}{M}\right)=\left({A}\mathrm{mod}{M}\right)+{B}$
7 6 oveq1d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({B}+\left({A}\mathrm{mod}{M}\right)\right)\mathrm{mod}{M}=\left(\left({A}\mathrm{mod}{M}\right)+{B}\right)\mathrm{mod}{M}$
8 modaddmod ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left(\left({A}\mathrm{mod}{M}\right)+{B}\right)\mathrm{mod}{M}=\left({A}+{B}\right)\mathrm{mod}{M}$
9 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
10 addcom ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}={B}+{A}$
11 9 1 10 syl2an ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}+{B}={B}+{A}$
12 11 oveq1d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}+{B}\right)\mathrm{mod}{M}=\left({B}+{A}\right)\mathrm{mod}{M}$
13 12 3adant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}+{B}\right)\mathrm{mod}{M}=\left({B}+{A}\right)\mathrm{mod}{M}$
14 7 8 13 3eqtrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({B}+\left({A}\mathrm{mod}{M}\right)\right)\mathrm{mod}{M}=\left({B}+{A}\right)\mathrm{mod}{M}$