Step |
Hyp |
Ref |
Expression |
1 |
|
divcl |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC ) |
2 |
|
abscl |
|- ( ( A / B ) e. CC -> ( abs ` ( A / B ) ) e. RR ) |
3 |
1 2
|
syl |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` ( A / B ) ) e. RR ) |
4 |
3
|
recnd |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` ( A / B ) ) e. CC ) |
5 |
|
absrpcl |
|- ( ( B e. CC /\ B =/= 0 ) -> ( abs ` B ) e. RR+ ) |
6 |
5
|
3adant1 |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` B ) e. RR+ ) |
7 |
6
|
rpcnd |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` B ) e. CC ) |
8 |
6
|
rpne0d |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` B ) =/= 0 ) |
9 |
4 7 8
|
divcan4d |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( ( abs ` ( A / B ) ) x. ( abs ` B ) ) / ( abs ` B ) ) = ( abs ` ( A / B ) ) ) |
10 |
|
simp2 |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> B e. CC ) |
11 |
|
absmul |
|- ( ( ( A / B ) e. CC /\ B e. CC ) -> ( abs ` ( ( A / B ) x. B ) ) = ( ( abs ` ( A / B ) ) x. ( abs ` B ) ) ) |
12 |
1 10 11
|
syl2anc |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` ( ( A / B ) x. B ) ) = ( ( abs ` ( A / B ) ) x. ( abs ` B ) ) ) |
13 |
|
divcan1 |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) x. B ) = A ) |
14 |
13
|
fveq2d |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` ( ( A / B ) x. B ) ) = ( abs ` A ) ) |
15 |
12 14
|
eqtr3d |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( abs ` ( A / B ) ) x. ( abs ` B ) ) = ( abs ` A ) ) |
16 |
15
|
oveq1d |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( ( abs ` ( A / B ) ) x. ( abs ` B ) ) / ( abs ` B ) ) = ( ( abs ` A ) / ( abs ` B ) ) ) |
17 |
9 16
|
eqtr3d |
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( abs ` ( A / B ) ) = ( ( abs ` A ) / ( abs ` B ) ) ) |