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