Step |
Hyp |
Ref |
Expression |
1 |
|
negcl |
|- ( C e. CC -> -u C e. CC ) |
2 |
|
cxpadd |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ -u C e. CC ) -> ( A ^c ( B + -u C ) ) = ( ( A ^c B ) x. ( A ^c -u C ) ) ) |
3 |
1 2
|
syl3an3 |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c ( B + -u C ) ) = ( ( A ^c B ) x. ( A ^c -u C ) ) ) |
4 |
|
simp2 |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> B e. CC ) |
5 |
|
simp3 |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> C e. CC ) |
6 |
4 5
|
negsubd |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( B + -u C ) = ( B - C ) ) |
7 |
6
|
oveq2d |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c ( B + -u C ) ) = ( A ^c ( B - C ) ) ) |
8 |
|
simp1l |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> A e. CC ) |
9 |
|
simp1r |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> A =/= 0 ) |
10 |
|
cxpneg |
|- ( ( A e. CC /\ A =/= 0 /\ C e. CC ) -> ( A ^c -u C ) = ( 1 / ( A ^c C ) ) ) |
11 |
8 9 5 10
|
syl3anc |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c -u C ) = ( 1 / ( A ^c C ) ) ) |
12 |
11
|
oveq2d |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( ( A ^c B ) x. ( A ^c -u C ) ) = ( ( A ^c B ) x. ( 1 / ( A ^c C ) ) ) ) |
13 |
|
cxpcl |
|- ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) e. CC ) |
14 |
8 4 13
|
syl2anc |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c B ) e. CC ) |
15 |
|
cxpcl |
|- ( ( A e. CC /\ C e. CC ) -> ( A ^c C ) e. CC ) |
16 |
8 5 15
|
syl2anc |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c C ) e. CC ) |
17 |
|
cxpne0 |
|- ( ( A e. CC /\ A =/= 0 /\ C e. CC ) -> ( A ^c C ) =/= 0 ) |
18 |
8 9 5 17
|
syl3anc |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c C ) =/= 0 ) |
19 |
14 16 18
|
divrecd |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( ( A ^c B ) / ( A ^c C ) ) = ( ( A ^c B ) x. ( 1 / ( A ^c C ) ) ) ) |
20 |
12 19
|
eqtr4d |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( ( A ^c B ) x. ( A ^c -u C ) ) = ( ( A ^c B ) / ( A ^c C ) ) ) |
21 |
3 7 20
|
3eqtr3d |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c ( B - C ) ) = ( ( A ^c B ) / ( A ^c C ) ) ) |