# 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, 13-May-2018)

Ref Expression
Assertion 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}$

### Proof

Step Hyp Ref Expression
1 modcl ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{M}\in ℝ$
2 simpl ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to {A}\in ℝ$
3 1 2 jca ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}\in ℝ\wedge {A}\in ℝ\right)$
4 3 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}\in ℝ\wedge {A}\in ℝ\right)$
5 3simpc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)$
6 modabs2 ${⊢}\left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}\right)\mathrm{mod}{M}={A}\mathrm{mod}{M}$
7 6 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{M}\right)\mathrm{mod}{M}={A}\mathrm{mod}{M}$
8 modadd1 ${⊢}\left(\left({A}\mathrm{mod}{M}\in ℝ\wedge {A}\in ℝ\right)\wedge \left({B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({A}\mathrm{mod}{M}\right)\mathrm{mod}{M}={A}\mathrm{mod}{M}\right)\to \left(\left({A}\mathrm{mod}{M}\right)+{B}\right)\mathrm{mod}{M}=\left({A}+{B}\right)\mathrm{mod}{M}$
9 4 5 7 8 syl3anc ${⊢}\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}$