# Metamath Proof Explorer

Description: The sum of a real number and the product of a second real number modulo a positive real number and an integer equals the sum of the real number and the product of the other real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018)

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

### Proof

Step Hyp Ref Expression
1 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
2 1 3ad2ant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\to {A}\in ℂ$
3 2 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {A}\in ℂ$
4 simpl2 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {B}\in ℝ$
5 simpr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {M}\in {ℝ}^{+}$
6 4 5 modcld ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {B}\mathrm{mod}{M}\in ℝ$
7 6 recnd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {B}\mathrm{mod}{M}\in ℂ$
8 zcn ${⊢}{C}\in ℤ\to {C}\in ℂ$
9 8 3ad2ant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\to {C}\in ℂ$
10 9 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {C}\in ℂ$
11 7 10 mulcld ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({B}\mathrm{mod}{M}\right){C}\in ℂ$
12 3 11 addcomd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {A}+\left({B}\mathrm{mod}{M}\right){C}=\left({B}\mathrm{mod}{M}\right){C}+{A}$
13 12 oveq1d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({A}+\left({B}\mathrm{mod}{M}\right){C}\right)\mathrm{mod}{M}=\left(\left({B}\mathrm{mod}{M}\right){C}+{A}\right)\mathrm{mod}{M}$
14 zre ${⊢}{C}\in ℤ\to {C}\in ℝ$
15 14 3ad2ant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\to {C}\in ℝ$
16 15 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {C}\in ℝ$
17 6 16 remulcld ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({B}\mathrm{mod}{M}\right){C}\in ℝ$
18 simpl ${⊢}\left({B}\in ℝ\wedge {C}\in ℤ\right)\to {B}\in ℝ$
19 14 adantl ${⊢}\left({B}\in ℝ\wedge {C}\in ℤ\right)\to {C}\in ℝ$
20 18 19 remulcld ${⊢}\left({B}\in ℝ\wedge {C}\in ℤ\right)\to {B}{C}\in ℝ$
21 20 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\to {B}{C}\in ℝ$
22 21 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {B}{C}\in ℝ$
23 22 5 modcld ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {B}{C}\mathrm{mod}{M}\in ℝ$
24 simp1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\to {A}\in ℝ$
25 24 anim1i ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)$
26 simpl3 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {C}\in ℤ$
27 modmulmod ${⊢}\left({B}\in ℝ\wedge {C}\in ℤ\wedge {M}\in {ℝ}^{+}\right)\to \left({B}\mathrm{mod}{M}\right){C}\mathrm{mod}{M}={B}{C}\mathrm{mod}{M}$
28 4 26 5 27 syl3anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({B}\mathrm{mod}{M}\right){C}\mathrm{mod}{M}={B}{C}\mathrm{mod}{M}$
29 remulcl ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to {B}{C}\in ℝ$
30 14 29 sylan2 ${⊢}\left({B}\in ℝ\wedge {C}\in ℤ\right)\to {B}{C}\in ℝ$
31 30 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\to {B}{C}\in ℝ$
32 modabs2 ${⊢}\left({B}{C}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({B}{C}\mathrm{mod}{M}\right)\mathrm{mod}{M}={B}{C}\mathrm{mod}{M}$
33 31 32 sylan ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({B}{C}\mathrm{mod}{M}\right)\mathrm{mod}{M}={B}{C}\mathrm{mod}{M}$
34 28 33 eqtr4d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({B}\mathrm{mod}{M}\right){C}\mathrm{mod}{M}=\left({B}{C}\mathrm{mod}{M}\right)\mathrm{mod}{M}$
35 modadd1 ${⊢}\left(\left(\left({B}\mathrm{mod}{M}\right){C}\in ℝ\wedge {B}{C}\mathrm{mod}{M}\in ℝ\right)\wedge \left({A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\wedge \left({B}\mathrm{mod}{M}\right){C}\mathrm{mod}{M}=\left({B}{C}\mathrm{mod}{M}\right)\mathrm{mod}{M}\right)\to \left(\left({B}\mathrm{mod}{M}\right){C}+{A}\right)\mathrm{mod}{M}=\left(\left({B}{C}\mathrm{mod}{M}\right)+{A}\right)\mathrm{mod}{M}$
36 17 23 25 34 35 syl211anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to \left(\left({B}\mathrm{mod}{M}\right){C}+{A}\right)\mathrm{mod}{M}=\left(\left({B}{C}\mathrm{mod}{M}\right)+{A}\right)\mathrm{mod}{M}$
37 31 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {B}{C}\in ℝ$
38 24 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {A}\in ℝ$
39 modaddmod ${⊢}\left({B}{C}\in ℝ\wedge {A}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left(\left({B}{C}\mathrm{mod}{M}\right)+{A}\right)\mathrm{mod}{M}=\left({B}{C}+{A}\right)\mathrm{mod}{M}$
40 37 38 5 39 syl3anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to \left(\left({B}{C}\mathrm{mod}{M}\right)+{A}\right)\mathrm{mod}{M}=\left({B}{C}+{A}\right)\mathrm{mod}{M}$
41 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
42 mulcl ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\right)\to {B}{C}\in ℂ$
43 41 8 42 syl2an ${⊢}\left({B}\in ℝ\wedge {C}\in ℤ\right)\to {B}{C}\in ℂ$
44 43 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\to {B}{C}\in ℂ$
45 44 2 addcomd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\to {B}{C}+{A}={A}+{B}{C}$
46 45 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to {B}{C}+{A}={A}+{B}{C}$
47 46 oveq1d ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({B}{C}+{A}\right)\mathrm{mod}{M}=\left({A}+{B}{C}\right)\mathrm{mod}{M}$
48 40 47 eqtrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to \left(\left({B}{C}\mathrm{mod}{M}\right)+{A}\right)\mathrm{mod}{M}=\left({A}+{B}{C}\right)\mathrm{mod}{M}$
49 13 36 48 3eqtrd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℤ\right)\wedge {M}\in {ℝ}^{+}\right)\to \left({A}+\left({B}\mathrm{mod}{M}\right){C}\right)\mathrm{mod}{M}=\left({A}+{B}{C}\right)\mathrm{mod}{M}$