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

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 ( 𝐴 · 𝐶 ) ) )