Step |
Hyp |
Ref |
Expression |
1 |
|
simp1l |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> A e. RR ) |
2 |
|
simp1r |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> 0 <_ A ) |
3 |
|
simp2 |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> B e. RR+ ) |
4 |
3
|
rpreccld |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( 1 / B ) e. RR+ ) |
5 |
4
|
rpred |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( 1 / B ) e. RR ) |
6 |
4
|
rpge0d |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> 0 <_ ( 1 / B ) ) |
7 |
|
simp3 |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> C e. CC ) |
8 |
|
mulcxp |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( ( 1 / B ) e. RR /\ 0 <_ ( 1 / B ) ) /\ C e. CC ) -> ( ( A x. ( 1 / B ) ) ^c C ) = ( ( A ^c C ) x. ( ( 1 / B ) ^c C ) ) ) |
9 |
1 2 5 6 7 8
|
syl221anc |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( ( A x. ( 1 / B ) ) ^c C ) = ( ( A ^c C ) x. ( ( 1 / B ) ^c C ) ) ) |
10 |
|
cxprec |
|- ( ( B e. RR+ /\ C e. CC ) -> ( ( 1 / B ) ^c C ) = ( 1 / ( B ^c C ) ) ) |
11 |
3 7 10
|
syl2anc |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( ( 1 / B ) ^c C ) = ( 1 / ( B ^c C ) ) ) |
12 |
11
|
oveq2d |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( ( A ^c C ) x. ( ( 1 / B ) ^c C ) ) = ( ( A ^c C ) x. ( 1 / ( B ^c C ) ) ) ) |
13 |
9 12
|
eqtrd |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( ( A x. ( 1 / B ) ) ^c C ) = ( ( A ^c C ) x. ( 1 / ( B ^c C ) ) ) ) |
14 |
1
|
recnd |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> A e. CC ) |
15 |
3
|
rpcnd |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> B e. CC ) |
16 |
3
|
rpne0d |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> B =/= 0 ) |
17 |
14 15 16
|
divrecd |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( A / B ) = ( A x. ( 1 / B ) ) ) |
18 |
17
|
oveq1d |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( ( A / B ) ^c C ) = ( ( A x. ( 1 / B ) ) ^c C ) ) |
19 |
|
cxpcl |
|- ( ( A e. CC /\ C e. CC ) -> ( A ^c C ) e. CC ) |
20 |
14 7 19
|
syl2anc |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( A ^c C ) e. CC ) |
21 |
|
cxpcl |
|- ( ( B e. CC /\ C e. CC ) -> ( B ^c C ) e. CC ) |
22 |
15 7 21
|
syl2anc |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( B ^c C ) e. CC ) |
23 |
|
cxpne0 |
|- ( ( B e. CC /\ B =/= 0 /\ C e. CC ) -> ( B ^c C ) =/= 0 ) |
24 |
15 16 7 23
|
syl3anc |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( B ^c C ) =/= 0 ) |
25 |
20 22 24
|
divrecd |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( ( A ^c C ) / ( B ^c C ) ) = ( ( A ^c C ) x. ( 1 / ( B ^c C ) ) ) ) |
26 |
13 18 25
|
3eqtr4d |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( ( A / B ) ^c C ) = ( ( A ^c C ) / ( B ^c C ) ) ) |