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 ) ) )