Metamath Proof Explorer


Theorem moddi

Description: Distribute multiplication over a modulo operation. (Contributed by NM, 11-Nov-2008)

Ref Expression
Assertion moddi ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · ( 𝐵 mod 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) mod ( 𝐴 · 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 rpcn ( 𝐴 ∈ ℝ+𝐴 ∈ ℂ )
2 1 3ad2ant1 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
3 recn ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
4 3 3ad2ant2 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
5 rpre ( 𝐶 ∈ ℝ+𝐶 ∈ ℝ )
6 5 adantl ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
7 refldivcl ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℝ )
8 6 7 remulcld ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ∈ ℝ )
9 8 recnd ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ∈ ℂ )
10 9 3adant1 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ∈ ℂ )
11 2 4 10 subdid ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) = ( ( 𝐴 · 𝐵 ) − ( 𝐴 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) )
12 rpcnne0 ( 𝐶 ∈ ℝ+ → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
13 12 3ad2ant3 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
14 rpcnne0 ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
15 14 3ad2ant1 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
16 divcan5 ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) = ( 𝐵 / 𝐶 ) )
17 4 13 15 16 syl3anc ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) = ( 𝐵 / 𝐶 ) )
18 17 fveq2d ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) = ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) )
19 18 oveq2d ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) ) = ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) )
20 rpcn ( 𝐶 ∈ ℝ+𝐶 ∈ ℂ )
21 20 3ad2ant3 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
22 rerpdivcl ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 / 𝐶 ) ∈ ℝ )
23 reflcl ( ( 𝐵 / 𝐶 ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℝ )
24 23 recnd ( ( 𝐵 / 𝐶 ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℂ )
25 22 24 syl ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℂ )
26 25 3adant1 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ∈ ℂ )
27 2 21 26 mulassd ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) = ( 𝐴 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) )
28 19 27 eqtr2d ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) = ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) ) )
29 28 oveq2d ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 · 𝐵 ) − ( 𝐴 · ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) = ( ( 𝐴 · 𝐵 ) − ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) ) ) )
30 11 29 eqtrd ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) = ( ( 𝐴 · 𝐵 ) − ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) ) ) )
31 modval ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) = ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) )
32 31 3adant1 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) = ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) )
33 32 oveq2d ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · ( 𝐵 mod 𝐶 ) ) = ( 𝐴 · ( 𝐵 − ( 𝐶 · ( ⌊ ‘ ( 𝐵 / 𝐶 ) ) ) ) ) )
34 rpre ( 𝐴 ∈ ℝ+𝐴 ∈ ℝ )
35 remulcl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
36 34 35 sylan ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
37 36 3adant3 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
38 rpmulcl ( ( 𝐴 ∈ ℝ+𝐶 ∈ ℝ+ ) → ( 𝐴 · 𝐶 ) ∈ ℝ+ )
39 modval ( ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ ( 𝐴 · 𝐶 ) ∈ ℝ+ ) → ( ( 𝐴 · 𝐵 ) mod ( 𝐴 · 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) − ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) ) ) )
40 37 38 39 3imp3i2an ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 · 𝐵 ) mod ( 𝐴 · 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) − ( ( 𝐴 · 𝐶 ) · ( ⌊ ‘ ( ( 𝐴 · 𝐵 ) / ( 𝐴 · 𝐶 ) ) ) ) ) )
41 30 33 40 3eqtr4d ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 · ( 𝐵 mod 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) mod ( 𝐴 · 𝐶 ) ) )