Metamath Proof Explorer

Theorem divcxp

Description: Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Assertion divcxp 
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( ( A / B ) ^c C ) = ( ( A ^c C ) / ( B ^c C ) ) )

Proof

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