Metamath Proof Explorer

Theorem modaddmulmod

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 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℤ ) ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 + ( ( 𝐵 mod 𝑀 ) · 𝐶 ) ) mod 𝑀 ) = ( ( 𝐴 + ( 𝐵 · 𝐶 ) ) mod 𝑀 ) )

Proof

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