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	$$⊢\phi \to A\in \mathbb{Z}$$
	modmul12d.2	$$⊢\phi \to B\in \mathbb{Z}$$
	modmul12d.3	$$⊢\phi \to C\in \mathbb{Z}$$
	modmul12d.4	$$⊢\phi \to D\in \mathbb{Z}$$
	modmul12d.5	$$⊢\phi \to E\in {ℝ}^{+}$$
	modmul12d.6	$$⊢\phi \to A\mathrm{mod}E=B\mathrm{mod}E$$
	modmul12d.7	$$⊢\phi \to C\mathrm{mod}E=D\mathrm{mod}E$$
Assertion	modmul12d	$$⊢\phi \to AC\mathrm{mod}E=BD\mathrm{mod}E$$

Proof

Step	Hyp	Ref	Expression
1		modmul12d.1	$$⊢\phi \to A\in \mathbb{Z}$$
2		modmul12d.2	$$⊢\phi \to B\in \mathbb{Z}$$
3		modmul12d.3	$$⊢\phi \to C\in \mathbb{Z}$$
4		modmul12d.4	$$⊢\phi \to D\in \mathbb{Z}$$
5		modmul12d.5	$$⊢\phi \to E\in {ℝ}^{+}$$
6		modmul12d.6	$$⊢\phi \to A\mathrm{mod}E=B\mathrm{mod}E$$
7		modmul12d.7	$$⊢\phi \to C\mathrm{mod}E=D\mathrm{mod}E$$
8	1	zred	$$⊢\phi \to A\in ℝ$$
9	2	zred	$$⊢\phi \to B\in ℝ$$
10		modmul1	$$⊢\left(\left(A\in ℝ\wedge B\in ℝ\right)\wedge \left(C\in \mathbb{Z}\wedge E\in {ℝ}^{+}\right)\wedge A\mathrm{mod}E=B\mathrm{mod}E\right)\to AC\mathrm{mod}E=BC\mathrm{mod}E$$
11	8 9 3 5 6 10	syl221anc	$$⊢\phi \to AC\mathrm{mod}E=BC\mathrm{mod}E$$
12	2	zcnd	$$⊢\phi \to B\in ℂ$$
13	3	zcnd	$$⊢\phi \to C\in ℂ$$
14	12 13	mulcomd	$$⊢\phi \to BC=CB$$
15	14	oveq1d	$$⊢\phi \to BC\mathrm{mod}E=CB\mathrm{mod}E$$
16	3	zred	$$⊢\phi \to C\in ℝ$$
17	4	zred	$$⊢\phi \to D\in ℝ$$
18		modmul1	$$⊢\left(\left(C\in ℝ\wedge D\in ℝ\right)\wedge \left(B\in \mathbb{Z}\wedge E\in {ℝ}^{+}\right)\wedge C\mathrm{mod}E=D\mathrm{mod}E\right)\to CB\mathrm{mod}E=DB\mathrm{mod}E$$
19	16 17 2 5 7 18	syl221anc	$$⊢\phi \to CB\mathrm{mod}E=DB\mathrm{mod}E$$
20	4	zcnd	$$⊢\phi \to D\in ℂ$$
21	20 12	mulcomd	$$⊢\phi \to DB=BD$$
22	21	oveq1d	$$⊢\phi \to DB\mathrm{mod}E=BD\mathrm{mod}E$$
23	15 19 22	3eqtrd	$$⊢\phi \to BC\mathrm{mod}E=BD\mathrm{mod}E$$
24	11 23	eqtrd	$$⊢\phi \to AC\mathrm{mod}E=BD\mathrm{mod}E$$