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 ${⊢}{\phi }\to {A}\in ℤ$
modmul12d.2 ${⊢}{\phi }\to {B}\in ℤ$
modmul12d.3 ${⊢}{\phi }\to {C}\in ℤ$
modmul12d.4 ${⊢}{\phi }\to {D}\in ℤ$
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 {A}{C}\mathrm{mod}{E}={B}{D}\mathrm{mod}{E}$

Proof

Step Hyp Ref Expression
1 modmul12d.1 ${⊢}{\phi }\to {A}\in ℤ$
2 modmul12d.2 ${⊢}{\phi }\to {B}\in ℤ$
3 modmul12d.3 ${⊢}{\phi }\to {C}\in ℤ$
4 modmul12d.4 ${⊢}{\phi }\to {D}\in ℤ$
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 ℤ\wedge {E}\in {ℝ}^{+}\right)\wedge {A}\mathrm{mod}{E}={B}\mathrm{mod}{E}\right)\to {A}{C}\mathrm{mod}{E}={B}{C}\mathrm{mod}{E}$
11 8 9 3 5 6 10 syl221anc ${⊢}{\phi }\to {A}{C}\mathrm{mod}{E}={B}{C}\mathrm{mod}{E}$
12 2 zcnd ${⊢}{\phi }\to {B}\in ℂ$
13 3 zcnd ${⊢}{\phi }\to {C}\in ℂ$
14 12 13 mulcomd ${⊢}{\phi }\to {B}{C}={C}{B}$
15 14 oveq1d ${⊢}{\phi }\to {B}{C}\mathrm{mod}{E}={C}{B}\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 ℤ\wedge {E}\in {ℝ}^{+}\right)\wedge {C}\mathrm{mod}{E}={D}\mathrm{mod}{E}\right)\to {C}{B}\mathrm{mod}{E}={D}{B}\mathrm{mod}{E}$
19 16 17 2 5 7 18 syl221anc ${⊢}{\phi }\to {C}{B}\mathrm{mod}{E}={D}{B}\mathrm{mod}{E}$
20 4 zcnd ${⊢}{\phi }\to {D}\in ℂ$
21 20 12 mulcomd ${⊢}{\phi }\to {D}{B}={B}{D}$
22 21 oveq1d ${⊢}{\phi }\to {D}{B}\mathrm{mod}{E}={B}{D}\mathrm{mod}{E}$
23 15 19 22 3eqtrd ${⊢}{\phi }\to {B}{C}\mathrm{mod}{E}={B}{D}\mathrm{mod}{E}$
24 11 23 eqtrd ${⊢}{\phi }\to {A}{C}\mathrm{mod}{E}={B}{D}\mathrm{mod}{E}$