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 
|- ( ph -> A e. ZZ )
modmul12d.2 
|- ( ph -> B e. ZZ )
modmul12d.3 
|- ( ph -> C e. ZZ )
modmul12d.4 
|- ( ph -> D e. ZZ )
modmul12d.5 
|- ( ph -> E e. RR+ )
modmul12d.6 
|- ( ph -> ( A mod E ) = ( B mod E ) )
modmul12d.7 
|- ( ph -> ( C mod E ) = ( D mod E ) )
Assertion modmul12d 
|- ( ph -> ( ( A x. C ) mod E ) = ( ( B x. D ) mod E ) )

Proof

Step Hyp Ref Expression
1 modmul12d.1 
 |-  ( ph -> A e. ZZ )
2 modmul12d.2 
 |-  ( ph -> B e. ZZ )
3 modmul12d.3 
 |-  ( ph -> C e. ZZ )
4 modmul12d.4 
 |-  ( ph -> D e. ZZ )
5 modmul12d.5 
 |-  ( ph -> E e. RR+ )
6 modmul12d.6 
 |-  ( ph -> ( A mod E ) = ( B mod E ) )
7 modmul12d.7 
 |-  ( ph -> ( C mod E ) = ( D mod E ) )
8 1 zred 
 |-  ( ph -> A e. RR )
9 2 zred 
 |-  ( ph -> B e. RR )
10 modmul1 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ E e. RR+ ) /\ ( A mod E ) = ( B mod E ) ) -> ( ( A x. C ) mod E ) = ( ( B x. C ) mod E ) )
11 8 9 3 5 6 10 syl221anc 
 |-  ( ph -> ( ( A x. C ) mod E ) = ( ( B x. C ) mod E ) )
12 2 zcnd 
 |-  ( ph -> B e. CC )
13 3 zcnd 
 |-  ( ph -> C e. CC )
14 12 13 mulcomd 
 |-  ( ph -> ( B x. C ) = ( C x. B ) )
15 14 oveq1d 
 |-  ( ph -> ( ( B x. C ) mod E ) = ( ( C x. B ) mod E ) )
16 3 zred 
 |-  ( ph -> C e. RR )
17 4 zred 
 |-  ( ph -> D e. RR )
18 modmul1 
 |-  ( ( ( C e. RR /\ D e. RR ) /\ ( B e. ZZ /\ E e. RR+ ) /\ ( C mod E ) = ( D mod E ) ) -> ( ( C x. B ) mod E ) = ( ( D x. B ) mod E ) )
19 16 17 2 5 7 18 syl221anc 
 |-  ( ph -> ( ( C x. B ) mod E ) = ( ( D x. B ) mod E ) )
20 4 zcnd 
 |-  ( ph -> D e. CC )
21 20 12 mulcomd 
 |-  ( ph -> ( D x. B ) = ( B x. D ) )
22 21 oveq1d 
 |-  ( ph -> ( ( D x. B ) mod E ) = ( ( B x. D ) mod E ) )
23 15 19 22 3eqtrd 
 |-  ( ph -> ( ( B x. C ) mod E ) = ( ( B x. D ) mod E ) )
24 11 23 eqtrd 
 |-  ( ph -> ( ( A x. C ) mod E ) = ( ( B x. D ) mod E ) )