Theorem cxprec

Description: Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 2-Aug-2014)

	Ref	Expression
Assertion	cxprec	|- ( ( A e. RR+ /\ B e. CC ) -> ( ( 1 / A ) ^c B ) = ( 1 / ( A ^c B ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpcn	|- ( A e. RR+ -> A e. CC )
2		cxpcl	|- ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) e. CC )
3	1 2	sylan	|- ( ( A e. RR+ /\ B e. CC ) -> ( A ^c B ) e. CC )
4		rpreccl	|- ( A e. RR+ -> ( 1 / A ) e. RR+ )
5	4	rpcnd	|- ( A e. RR+ -> ( 1 / A ) e. CC )
6		cxpcl	|- ( ( ( 1 / A ) e. CC /\ B e. CC ) -> ( ( 1 / A ) ^c B ) e. CC )
7	5 6	sylan	|- ( ( A e. RR+ /\ B e. CC ) -> ( ( 1 / A ) ^c B ) e. CC )
8	1	adantr	|- ( ( A e. RR+ /\ B e. CC ) -> A e. CC )
9		rpne0	|- ( A e. RR+ -> A =/= 0 )
10	9	adantr	|- ( ( A e. RR+ /\ B e. CC ) -> A =/= 0 )
11		simpr	|- ( ( A e. RR+ /\ B e. CC ) -> B e. CC )
12		cxpne0	|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) =/= 0 )
13	8 10 11 12	syl3anc	|- ( ( A e. RR+ /\ B e. CC ) -> ( A ^c B ) =/= 0 )
14	8 10	recidd	|- ( ( A e. RR+ /\ B e. CC ) -> ( A x. ( 1 / A ) ) = 1 )
15	14	oveq1d	|- ( ( A e. RR+ /\ B e. CC ) -> ( ( A x. ( 1 / A ) ) ^c B ) = ( 1 ^c B ) )
16		rprege0	|- ( A e. RR+ -> ( A e. RR /\ 0 <_ A ) )
17	16	adantr	|- ( ( A e. RR+ /\ B e. CC ) -> ( A e. RR /\ 0 <_ A ) )
18	4	rprege0d	|- ( A e. RR+ -> ( ( 1 / A ) e. RR /\ 0 <_ ( 1 / A ) ) )
19	18	adantr	|- ( ( A e. RR+ /\ B e. CC ) -> ( ( 1 / A ) e. RR /\ 0 <_ ( 1 / A ) ) )
20		mulcxp	|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( ( 1 / A ) e. RR /\ 0 <_ ( 1 / A ) ) /\ B e. CC ) -> ( ( A x. ( 1 / A ) ) ^c B ) = ( ( A ^c B ) x. ( ( 1 / A ) ^c B ) ) )
21	17 19 11 20	syl3anc	|- ( ( A e. RR+ /\ B e. CC ) -> ( ( A x. ( 1 / A ) ) ^c B ) = ( ( A ^c B ) x. ( ( 1 / A ) ^c B ) ) )
22		1cxp	|- ( B e. CC -> ( 1 ^c B ) = 1 )
23	11 22	syl	|- ( ( A e. RR+ /\ B e. CC ) -> ( 1 ^c B ) = 1 )
24	15 21 23	3eqtr3d	|- ( ( A e. RR+ /\ B e. CC ) -> ( ( A ^c B ) x. ( ( 1 / A ) ^c B ) ) = 1 )
25	3 7 13 24	mvllmuld	|- ( ( A e. RR+ /\ B e. CC ) -> ( ( 1 / A ) ^c B ) = ( 1 / ( A ^c B ) ) )