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