Theorem divcxpd

Description: Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 30-May-2016)

	Ref	Expression
Hypotheses	recxpcld.1	|- ( ph -> A e. RR )
	recxpcld.2	|- ( ph -> 0 <_ A )
	divcxpd.4	|- ( ph -> B e. RR+ )
	divcxpd.5	|- ( ph -> C e. CC )
Assertion	divcxpd	|- ( ph -> ( ( A / B ) ^c C ) = ( ( A ^c C ) / ( B ^c C ) ) )

Proof

Step	Hyp	Ref	Expression
1		recxpcld.1	|- ( ph -> A e. RR )
2		recxpcld.2	|- ( ph -> 0 <_ A )
3		divcxpd.4	|- ( ph -> B e. RR+ )
4		divcxpd.5	|- ( ph -> C e. CC )
5		divcxp	|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( ( A / B ) ^c C ) = ( ( A ^c C ) / ( B ^c C ) ) )
6	1 2 3 4 5	syl211anc	|- ( ph -> ( ( A / B ) ^c C ) = ( ( A ^c C ) / ( B ^c C ) ) )