# Metamath Proof Explorer

Description: Absorption law for modulo. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion modaddabs ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left(\left({A}\mathrm{mod}{C}\right)+\left({B}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}=\left({A}+{B}\right)\mathrm{mod}{C}$

### Proof

Step Hyp Ref Expression
1 modcl ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{C}\in ℝ$
2 1 recnd ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{C}\in ℂ$
3 2 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\mathrm{mod}{C}\in ℂ$
4 modcl ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\mathrm{mod}{C}\in ℝ$
5 4 recnd ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\mathrm{mod}{C}\in ℂ$
6 5 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\mathrm{mod}{C}\in ℂ$
7 3 6 addcomd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{C}\right)+\left({B}\mathrm{mod}{C}\right)=\left({B}\mathrm{mod}{C}\right)+\left({A}\mathrm{mod}{C}\right)$
8 7 oveq1d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left(\left({A}\mathrm{mod}{C}\right)+\left({B}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}=\left(\left({B}\mathrm{mod}{C}\right)+\left({A}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}$
9 simpl ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\in ℝ$
10 4 9 jca ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({B}\mathrm{mod}{C}\in ℝ\wedge {B}\in ℝ\right)$
11 10 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({B}\mathrm{mod}{C}\in ℝ\wedge {B}\in ℝ\right)$
12 simpr ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {C}\in {ℝ}^{+}$
13 1 12 jca ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{C}\in ℝ\wedge {C}\in {ℝ}^{+}\right)$
14 13 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{C}\in ℝ\wedge {C}\in {ℝ}^{+}\right)$
15 modabs2 ${⊢}\left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({B}\mathrm{mod}{C}\right)\mathrm{mod}{C}={B}\mathrm{mod}{C}$
16 15 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({B}\mathrm{mod}{C}\right)\mathrm{mod}{C}={B}\mathrm{mod}{C}$
17 modadd1 ${⊢}\left(\left({B}\mathrm{mod}{C}\in ℝ\wedge {B}\in ℝ\right)\wedge \left({A}\mathrm{mod}{C}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge \left({B}\mathrm{mod}{C}\right)\mathrm{mod}{C}={B}\mathrm{mod}{C}\right)\to \left(\left({B}\mathrm{mod}{C}\right)+\left({A}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}=\left({B}+\left({A}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}$
18 11 14 16 17 syl3anc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left(\left({B}\mathrm{mod}{C}\right)+\left({A}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}=\left({B}+\left({A}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}$
19 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
20 19 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {B}\in ℂ$
21 3 20 addcomd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{C}\right)+{B}={B}+\left({A}\mathrm{mod}{C}\right)$
22 21 oveq1d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left(\left({A}\mathrm{mod}{C}\right)+{B}\right)\mathrm{mod}{C}=\left({B}+\left({A}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}$
23 18 22 eqtr4d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left(\left({B}\mathrm{mod}{C}\right)+\left({A}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}=\left(\left({A}\mathrm{mod}{C}\right)+{B}\right)\mathrm{mod}{C}$
24 simpl ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to {A}\in ℝ$
25 1 24 jca ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{C}\in ℝ\wedge {A}\in ℝ\right)$
26 25 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{C}\in ℝ\wedge {A}\in ℝ\right)$
27 3simpc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)$
28 modabs2 ${⊢}\left({A}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{C}\right)\mathrm{mod}{C}={A}\mathrm{mod}{C}$
29 28 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left({A}\mathrm{mod}{C}\right)\mathrm{mod}{C}={A}\mathrm{mod}{C}$
30 modadd1 ${⊢}\left(\left({A}\mathrm{mod}{C}\in ℝ\wedge {A}\in ℝ\right)\wedge \left({B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\wedge \left({A}\mathrm{mod}{C}\right)\mathrm{mod}{C}={A}\mathrm{mod}{C}\right)\to \left(\left({A}\mathrm{mod}{C}\right)+{B}\right)\mathrm{mod}{C}=\left({A}+{B}\right)\mathrm{mod}{C}$
31 26 27 29 30 syl3anc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left(\left({A}\mathrm{mod}{C}\right)+{B}\right)\mathrm{mod}{C}=\left({A}+{B}\right)\mathrm{mod}{C}$
32 8 23 31 3eqtrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in {ℝ}^{+}\right)\to \left(\left({A}\mathrm{mod}{C}\right)+\left({B}\mathrm{mod}{C}\right)\right)\mathrm{mod}{C}=\left({A}+{B}\right)\mathrm{mod}{C}$