This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑀 ) )