Metamath Proof Explorer

Theorem modmul1

Description: Multiplication property of the modulo operation. Note that the multiplier C must be an integer. (Contributed by NM, 12-Nov-2008)

Ref Expression
Assertion modmul1 
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) /\ ( A mod D ) = ( B mod D ) ) -> ( ( A x. C ) mod D ) = ( ( B x. C ) mod D ) )

Proof

Step Hyp Ref Expression
1 modval 
 |-  ( ( A e. RR /\ D e. RR+ ) -> ( A mod D ) = ( A - ( D x. ( |_ ` ( A / D ) ) ) ) )
2 modval 
 |-  ( ( B e. RR /\ D e. RR+ ) -> ( B mod D ) = ( B - ( D x. ( |_ ` ( B / D ) ) ) ) )
3 1 2 eqeqan12d 
 |-  ( ( ( A e. RR /\ D e. RR+ ) /\ ( B e. RR /\ D e. RR+ ) ) -> ( ( A mod D ) = ( B mod D ) <-> ( A - ( D x. ( |_ ` ( A / D ) ) ) ) = ( B - ( D x. ( |_ ` ( B / D ) ) ) ) ) )
4 3 anandirs 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ D e. RR+ ) -> ( ( A mod D ) = ( B mod D ) <-> ( A - ( D x. ( |_ ` ( A / D ) ) ) ) = ( B - ( D x. ( |_ ` ( B / D ) ) ) ) ) )
5 4 adantrl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( A mod D ) = ( B mod D ) <-> ( A - ( D x. ( |_ ` ( A / D ) ) ) ) = ( B - ( D x. ( |_ ` ( B / D ) ) ) ) ) )
6 oveq1 
 |-  ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) = ( B - ( D x. ( |_ ` ( B / D ) ) ) ) -> ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) x. C ) = ( ( B - ( D x. ( |_ ` ( B / D ) ) ) ) x. C ) )
7 5 6 biimtrdi 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( A mod D ) = ( B mod D ) -> ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) x. C ) = ( ( B - ( D x. ( |_ ` ( B / D ) ) ) ) x. C ) ) )
8 rpcn 
 |-  ( D e. RR+ -> D e. CC )
9 8 ad2antll 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> D e. CC )
10 zcn 
 |-  ( C e. ZZ -> C e. CC )
11 10 ad2antrl 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> C e. CC )
12 rerpdivcl 
 |-  ( ( A e. RR /\ D e. RR+ ) -> ( A / D ) e. RR )
13 12 flcld 
 |-  ( ( A e. RR /\ D e. RR+ ) -> ( |_ ` ( A / D ) ) e. ZZ )
14 13 zcnd 
 |-  ( ( A e. RR /\ D e. RR+ ) -> ( |_ ` ( A / D ) ) e. CC )
15 14 adantrl 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( |_ ` ( A / D ) ) e. CC )
16 9 11 15 mulassd 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( D x. C ) x. ( |_ ` ( A / D ) ) ) = ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) )
17 9 11 15 mul32d 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( D x. C ) x. ( |_ ` ( A / D ) ) ) = ( ( D x. ( |_ ` ( A / D ) ) ) x. C ) )
18 16 17 eqtr3d 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) = ( ( D x. ( |_ ` ( A / D ) ) ) x. C ) )
19 18 oveq2d 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( A x. C ) - ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) ) = ( ( A x. C ) - ( ( D x. ( |_ ` ( A / D ) ) ) x. C ) ) )
20 recn 
 |-  ( A e. RR -> A e. CC )
21 20 adantr 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> A e. CC )
22 8 adantl 
 |-  ( ( A e. RR /\ D e. RR+ ) -> D e. CC )
23 22 14 mulcld 
 |-  ( ( A e. RR /\ D e. RR+ ) -> ( D x. ( |_ ` ( A / D ) ) ) e. CC )
24 23 adantrl 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( D x. ( |_ ` ( A / D ) ) ) e. CC )
25 21 24 11 subdird 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) x. C ) = ( ( A x. C ) - ( ( D x. ( |_ ` ( A / D ) ) ) x. C ) ) )
26 19 25 eqtr4d 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( A x. C ) - ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) ) = ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) x. C ) )
27 26 adantlr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( A x. C ) - ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) ) = ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) x. C ) )
28 8 ad2antll 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> D e. CC )
29 10 ad2antrl 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> C e. CC )
30 rerpdivcl 
 |-  ( ( B e. RR /\ D e. RR+ ) -> ( B / D ) e. RR )
31 30 flcld 
 |-  ( ( B e. RR /\ D e. RR+ ) -> ( |_ ` ( B / D ) ) e. ZZ )
32 31 zcnd 
 |-  ( ( B e. RR /\ D e. RR+ ) -> ( |_ ` ( B / D ) ) e. CC )
33 32 adantrl 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( |_ ` ( B / D ) ) e. CC )
34 28 29 33 mulassd 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( D x. C ) x. ( |_ ` ( B / D ) ) ) = ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) )
35 28 29 33 mul32d 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( D x. C ) x. ( |_ ` ( B / D ) ) ) = ( ( D x. ( |_ ` ( B / D ) ) ) x. C ) )
36 34 35 eqtr3d 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) = ( ( D x. ( |_ ` ( B / D ) ) ) x. C ) )
37 36 oveq2d 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( B x. C ) - ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) ) = ( ( B x. C ) - ( ( D x. ( |_ ` ( B / D ) ) ) x. C ) ) )
38 recn 
 |-  ( B e. RR -> B e. CC )
39 38 adantr 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> B e. CC )
40 8 adantl 
 |-  ( ( B e. RR /\ D e. RR+ ) -> D e. CC )
41 40 32 mulcld 
 |-  ( ( B e. RR /\ D e. RR+ ) -> ( D x. ( |_ ` ( B / D ) ) ) e. CC )
42 41 adantrl 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( D x. ( |_ ` ( B / D ) ) ) e. CC )
43 39 42 29 subdird 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( B - ( D x. ( |_ ` ( B / D ) ) ) ) x. C ) = ( ( B x. C ) - ( ( D x. ( |_ ` ( B / D ) ) ) x. C ) ) )
44 37 43 eqtr4d 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( B x. C ) - ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) ) = ( ( B - ( D x. ( |_ ` ( B / D ) ) ) ) x. C ) )
45 44 adantll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( B x. C ) - ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) ) = ( ( B - ( D x. ( |_ ` ( B / D ) ) ) ) x. C ) )
46 27 45 eqeq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( ( A x. C ) - ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) ) = ( ( B x. C ) - ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) ) <-> ( ( A - ( D x. ( |_ ` ( A / D ) ) ) ) x. C ) = ( ( B - ( D x. ( |_ ` ( B / D ) ) ) ) x. C ) ) )
47 7 46 sylibrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( A mod D ) = ( B mod D ) -> ( ( A x. C ) - ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) ) = ( ( B x. C ) - ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) ) ) )
48 oveq1 
 |-  ( ( ( A x. C ) - ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) ) = ( ( B x. C ) - ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) ) -> ( ( ( A x. C ) - ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) ) mod D ) = ( ( ( B x. C ) - ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) ) mod D ) )
49 zre 
 |-  ( C e. ZZ -> C e. RR )
50 remulcl 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A x. C ) e. RR )
51 49 50 sylan2 
 |-  ( ( A e. RR /\ C e. ZZ ) -> ( A x. C ) e. RR )
52 51 adantrr 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( A x. C ) e. RR )
53 simprr 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> D e. RR+ )
54 simprl 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> C e. ZZ )
55 13 adantrl 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( |_ ` ( A / D ) ) e. ZZ )
56 54 55 zmulcld 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( C x. ( |_ ` ( A / D ) ) ) e. ZZ )
57 modcyc2 
 |-  ( ( ( A x. C ) e. RR /\ D e. RR+ /\ ( C x. ( |_ ` ( A / D ) ) ) e. ZZ ) -> ( ( ( A x. C ) - ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) ) mod D ) = ( ( A x. C ) mod D ) )
58 52 53 56 57 syl3anc 
 |-  ( ( A e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( ( A x. C ) - ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) ) mod D ) = ( ( A x. C ) mod D ) )
59 58 adantlr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( ( A x. C ) - ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) ) mod D ) = ( ( A x. C ) mod D ) )
60 remulcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B x. C ) e. RR )
61 49 60 sylan2 
 |-  ( ( B e. RR /\ C e. ZZ ) -> ( B x. C ) e. RR )
62 61 adantrr 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( B x. C ) e. RR )
63 simprr 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> D e. RR+ )
64 simprl 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> C e. ZZ )
65 31 adantrl 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( |_ ` ( B / D ) ) e. ZZ )
66 64 65 zmulcld 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( C x. ( |_ ` ( B / D ) ) ) e. ZZ )
67 modcyc2 
 |-  ( ( ( B x. C ) e. RR /\ D e. RR+ /\ ( C x. ( |_ ` ( B / D ) ) ) e. ZZ ) -> ( ( ( B x. C ) - ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) ) mod D ) = ( ( B x. C ) mod D ) )
68 62 63 66 67 syl3anc 
 |-  ( ( B e. RR /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( ( B x. C ) - ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) ) mod D ) = ( ( B x. C ) mod D ) )
69 68 adantll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( ( B x. C ) - ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) ) mod D ) = ( ( B x. C ) mod D ) )
70 59 69 eqeq12d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( ( ( A x. C ) - ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) ) mod D ) = ( ( ( B x. C ) - ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) ) mod D ) <-> ( ( A x. C ) mod D ) = ( ( B x. C ) mod D ) ) )
71 48 70 imbitrid 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( ( A x. C ) - ( D x. ( C x. ( |_ ` ( A / D ) ) ) ) ) = ( ( B x. C ) - ( D x. ( C x. ( |_ ` ( B / D ) ) ) ) ) -> ( ( A x. C ) mod D ) = ( ( B x. C ) mod D ) ) )
72 47 71 syld 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) ) -> ( ( A mod D ) = ( B mod D ) -> ( ( A x. C ) mod D ) = ( ( B x. C ) mod D ) ) )
73 72 3impia 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ZZ /\ D e. RR+ ) /\ ( A mod D ) = ( B mod D ) ) -> ( ( A x. C ) mod D ) = ( ( B x. C ) mod D ) )