Metamath Proof Explorer

Theorem moddi

Description: Distribute multiplication over a modulo operation. (Contributed by NM, 11-Nov-2008)

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

Proof

Step Hyp Ref Expression
1 rpcn 
 |-  ( A e. RR+ -> A e. CC )
2 1 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> A e. CC )
3 recn 
 |-  ( B e. RR -> B e. CC )
4 3 3ad2ant2 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> B e. CC )
5 rpre 
 |-  ( C e. RR+ -> C e. RR )
6 5 adantl 
 |-  ( ( B e. RR /\ C e. RR+ ) -> C e. RR )
7 refldivcl 
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( |_ ` ( B / C ) ) e. RR )
8 6 7 remulcld 
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( C x. ( |_ ` ( B / C ) ) ) e. RR )
9 8 recnd 
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( C x. ( |_ ` ( B / C ) ) ) e. CC )
10 9 3adant1 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( C x. ( |_ ` ( B / C ) ) ) e. CC )
11 2 4 10 subdid 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( A x. ( B - ( C x. ( |_ ` ( B / C ) ) ) ) ) = ( ( A x. B ) - ( A x. ( C x. ( |_ ` ( B / C ) ) ) ) ) )
12 rpcnne0 
 |-  ( C e. RR+ -> ( C e. CC /\ C =/= 0 ) )
13 12 3ad2ant3 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( C e. CC /\ C =/= 0 ) )
14 rpcnne0 
 |-  ( A e. RR+ -> ( A e. CC /\ A =/= 0 ) )
15 14 3ad2ant1 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( A e. CC /\ A =/= 0 ) )
16 divcan5 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( A x. B ) / ( A x. C ) ) = ( B / C ) )
17 4 13 15 16 syl3anc 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( ( A x. B ) / ( A x. C ) ) = ( B / C ) )
18 17 fveq2d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( |_ ` ( ( A x. B ) / ( A x. C ) ) ) = ( |_ ` ( B / C ) ) )
19 18 oveq2d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( ( A x. C ) x. ( |_ ` ( ( A x. B ) / ( A x. C ) ) ) ) = ( ( A x. C ) x. ( |_ ` ( B / C ) ) ) )
20 rpcn 
 |-  ( C e. RR+ -> C e. CC )
21 20 3ad2ant3 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> C e. CC )
22 rerpdivcl 
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( B / C ) e. RR )
23 reflcl 
 |-  ( ( B / C ) e. RR -> ( |_ ` ( B / C ) ) e. RR )
24 23 recnd 
 |-  ( ( B / C ) e. RR -> ( |_ ` ( B / C ) ) e. CC )
25 22 24 syl 
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( |_ ` ( B / C ) ) e. CC )
26 25 3adant1 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( |_ ` ( B / C ) ) e. CC )
27 2 21 26 mulassd 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( ( A x. C ) x. ( |_ ` ( B / C ) ) ) = ( A x. ( C x. ( |_ ` ( B / C ) ) ) ) )
28 19 27 eqtr2d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( A x. ( C x. ( |_ ` ( B / C ) ) ) ) = ( ( A x. C ) x. ( |_ ` ( ( A x. B ) / ( A x. C ) ) ) ) )
29 28 oveq2d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( ( A x. B ) - ( A x. ( C x. ( |_ ` ( B / C ) ) ) ) ) = ( ( A x. B ) - ( ( A x. C ) x. ( |_ ` ( ( A x. B ) / ( A x. C ) ) ) ) ) )
30 11 29 eqtrd 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( A x. ( B - ( C x. ( |_ ` ( B / C ) ) ) ) ) = ( ( A x. B ) - ( ( A x. C ) x. ( |_ ` ( ( A x. B ) / ( A x. C ) ) ) ) ) )
31 modval 
 |-  ( ( B e. RR /\ C e. RR+ ) -> ( B mod C ) = ( B - ( C x. ( |_ ` ( B / C ) ) ) ) )
32 31 3adant1 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( B mod C ) = ( B - ( C x. ( |_ ` ( B / C ) ) ) ) )
33 32 oveq2d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( A x. ( B mod C ) ) = ( A x. ( B - ( C x. ( |_ ` ( B / C ) ) ) ) ) )
34 rpre 
 |-  ( A e. RR+ -> A e. RR )
35 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
36 34 35 sylan 
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( A x. B ) e. RR )
37 36 3adant3 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( A x. B ) e. RR )
38 rpmulcl 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> ( A x. C ) e. RR+ )
39 modval 
 |-  ( ( ( A x. B ) e. RR /\ ( A x. C ) e. RR+ ) -> ( ( A x. B ) mod ( A x. C ) ) = ( ( A x. B ) - ( ( A x. C ) x. ( |_ ` ( ( A x. B ) / ( A x. C ) ) ) ) ) )
40 37 38 39 3imp3i2an 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( ( A x. B ) mod ( A x. C ) ) = ( ( A x. B ) - ( ( A x. C ) x. ( |_ ` ( ( A x. B ) / ( A x. C ) ) ) ) ) )
41 30 33 40 3eqtr4d 
 |-  ( ( A e. RR+ /\ B e. RR /\ C e. RR+ ) -> ( A x. ( B mod C ) ) = ( ( A x. B ) mod ( A x. C ) ) )