Metamath Proof Explorer

Theorem modmul12d

Description: Multiplication property of the modulo operation, see theorem 5.2(b) in ApostolNT p. 107. (Contributed by Mario Carneiro, 5-Feb-2015)

Ref Expression
Hypotheses modmul12d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
modmul12d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
modmul12d.3 ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
modmul12d.4 ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
modmul12d.5 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
modmul12d.6 ⊢ ( 𝜑 → ( 𝐴 mod 𝐸 ) = ( 𝐵 mod 𝐸 ) )
modmul12d.7 ⊢ ( 𝜑 → ( 𝐶 mod 𝐸 ) = ( 𝐷 mod 𝐸 ) )
Assertion modmul12d ( 𝜑 → ( ( 𝐴 · 𝐶 ) mod 𝐸 ) = ( ( 𝐵 · 𝐷 ) mod 𝐸 ) )

Proof

Step Hyp Ref Expression
1 modmul12d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2 modmul12d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
3 modmul12d.3 ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
4 modmul12d.4 ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
5 modmul12d.5 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
6 modmul12d.6 ⊢ ( 𝜑 → ( 𝐴 mod 𝐸 ) = ( 𝐵 mod 𝐸 ) )
7 modmul12d.7 ⊢ ( 𝜑 → ( 𝐶 mod 𝐸 ) = ( 𝐷 mod 𝐸 ) )
8 1 zred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
9 2 zred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
10 modmul1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐸 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝐸 ) = ( 𝐵 mod 𝐸 ) ) → ( ( 𝐴 · 𝐶 ) mod 𝐸 ) = ( ( 𝐵 · 𝐶 ) mod 𝐸 ) )
11 8 9 3 5 6 10 syl221anc ⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) mod 𝐸 ) = ( ( 𝐵 · 𝐶 ) mod 𝐸 ) )
12 2 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
13 3 zcnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
14 12 13 mulcomd ⊢ ( 𝜑 → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
15 14 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) mod 𝐸 ) = ( ( 𝐶 · 𝐵 ) mod 𝐸 ) )
16 3 zred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
17 4 zred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
18 modmul1 ⊢ ( ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐸 ∈ ℝ+ ) ∧ ( 𝐶 mod 𝐸 ) = ( 𝐷 mod 𝐸 ) ) → ( ( 𝐶 · 𝐵 ) mod 𝐸 ) = ( ( 𝐷 · 𝐵 ) mod 𝐸 ) )
19 16 17 2 5 7 18 syl221anc ⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) mod 𝐸 ) = ( ( 𝐷 · 𝐵 ) mod 𝐸 ) )
20 4 zcnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
21 20 12 mulcomd ⊢ ( 𝜑 → ( 𝐷 · 𝐵 ) = ( 𝐵 · 𝐷 ) )
22 21 oveq1d ⊢ ( 𝜑 → ( ( 𝐷 · 𝐵 ) mod 𝐸 ) = ( ( 𝐵 · 𝐷 ) mod 𝐸 ) )
23 15 19 22 3eqtrd ⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) mod 𝐸 ) = ( ( 𝐵 · 𝐷 ) mod 𝐸 ) )
24 11 23 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) mod 𝐸 ) = ( ( 𝐵 · 𝐷 ) mod 𝐸 ) )