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