Step |
Hyp |
Ref |
Expression |
1 |
|
elznn0 |
|- ( C e. ZZ <-> ( C e. RR /\ ( C e. NN0 \/ -u C e. NN0 ) ) ) |
2 |
|
cxpmul2 |
|- ( ( A e. CC /\ B e. CC /\ C e. NN0 ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) |
3 |
2
|
3expia |
|- ( ( A e. CC /\ B e. CC ) -> ( C e. NN0 -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) ) |
4 |
3
|
ad4ant13 |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ C e. RR ) -> ( C e. NN0 -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) ) |
5 |
|
simplll |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> A e. CC ) |
6 |
|
simplr |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> B e. CC ) |
7 |
|
simprr |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> -u C e. NN0 ) |
8 |
|
cxpmul2 |
|- ( ( A e. CC /\ B e. CC /\ -u C e. NN0 ) -> ( A ^c ( B x. -u C ) ) = ( ( A ^c B ) ^ -u C ) ) |
9 |
5 6 7 8
|
syl3anc |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( A ^c ( B x. -u C ) ) = ( ( A ^c B ) ^ -u C ) ) |
10 |
9
|
oveq2d |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( 1 / ( A ^c ( B x. -u C ) ) ) = ( 1 / ( ( A ^c B ) ^ -u C ) ) ) |
11 |
|
simprl |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> C e. RR ) |
12 |
11
|
recnd |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> C e. CC ) |
13 |
6 12
|
mulneg2d |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( B x. -u C ) = -u ( B x. C ) ) |
14 |
13
|
negeqd |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> -u ( B x. -u C ) = -u -u ( B x. C ) ) |
15 |
6 12
|
mulcld |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( B x. C ) e. CC ) |
16 |
15
|
negnegd |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> -u -u ( B x. C ) = ( B x. C ) ) |
17 |
14 16
|
eqtrd |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> -u ( B x. -u C ) = ( B x. C ) ) |
18 |
17
|
oveq2d |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( A ^c -u ( B x. -u C ) ) = ( A ^c ( B x. C ) ) ) |
19 |
|
simpllr |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> A =/= 0 ) |
20 |
12
|
negcld |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> -u C e. CC ) |
21 |
6 20
|
mulcld |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( B x. -u C ) e. CC ) |
22 |
|
cxpneg |
|- ( ( A e. CC /\ A =/= 0 /\ ( B x. -u C ) e. CC ) -> ( A ^c -u ( B x. -u C ) ) = ( 1 / ( A ^c ( B x. -u C ) ) ) ) |
23 |
5 19 21 22
|
syl3anc |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( A ^c -u ( B x. -u C ) ) = ( 1 / ( A ^c ( B x. -u C ) ) ) ) |
24 |
18 23
|
eqtr3d |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( A ^c ( B x. C ) ) = ( 1 / ( A ^c ( B x. -u C ) ) ) ) |
25 |
|
cxpcl |
|- ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) e. CC ) |
26 |
25
|
ad4ant13 |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( A ^c B ) e. CC ) |
27 |
|
expneg2 |
|- ( ( ( A ^c B ) e. CC /\ C e. CC /\ -u C e. NN0 ) -> ( ( A ^c B ) ^ C ) = ( 1 / ( ( A ^c B ) ^ -u C ) ) ) |
28 |
26 12 7 27
|
syl3anc |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( ( A ^c B ) ^ C ) = ( 1 / ( ( A ^c B ) ^ -u C ) ) ) |
29 |
10 24 28
|
3eqtr4d |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) |
30 |
29
|
expr |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ C e. RR ) -> ( -u C e. NN0 -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) ) |
31 |
4 30
|
jaod |
|- ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ C e. RR ) -> ( ( C e. NN0 \/ -u C e. NN0 ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) ) |
32 |
31
|
expimpd |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) -> ( ( C e. RR /\ ( C e. NN0 \/ -u C e. NN0 ) ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) ) |
33 |
1 32
|
syl5bi |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) -> ( C e. ZZ -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) ) |
34 |
33
|
impr |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ C e. ZZ ) ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) |