Theorem cxproot

Description: The complex power function allows us to write n-th roots via the idiom A ^c ( 1 / N ) . (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Assertion	cxproot	|- ( ( A e. CC /\ N e. NN ) -> ( ( A ^c ( 1 / N ) ) ^ N ) = A )

Proof

Step	Hyp	Ref	Expression
1		nncn	|- ( N e. NN -> N e. CC )
2	1	adantl	|- ( ( A e. CC /\ N e. NN ) -> N e. CC )
3		nnne0	|- ( N e. NN -> N =/= 0 )
4	3	adantl	|- ( ( A e. CC /\ N e. NN ) -> N =/= 0 )
5	2 4	recid2d	|- ( ( A e. CC /\ N e. NN ) -> ( ( 1 / N ) x. N ) = 1 )
6	5	oveq2d	|- ( ( A e. CC /\ N e. NN ) -> ( A ^c ( ( 1 / N ) x. N ) ) = ( A ^c 1 ) )
7		simpl	|- ( ( A e. CC /\ N e. NN ) -> A e. CC )
8		nnrecre	|- ( N e. NN -> ( 1 / N ) e. RR )
9	8	adantl	|- ( ( A e. CC /\ N e. NN ) -> ( 1 / N ) e. RR )
10	9	recnd	|- ( ( A e. CC /\ N e. NN ) -> ( 1 / N ) e. CC )
11		nnnn0	|- ( N e. NN -> N e. NN0 )
12	11	adantl	|- ( ( A e. CC /\ N e. NN ) -> N e. NN0 )
13		cxpmul2	|- ( ( A e. CC /\ ( 1 / N ) e. CC /\ N e. NN0 ) -> ( A ^c ( ( 1 / N ) x. N ) ) = ( ( A ^c ( 1 / N ) ) ^ N ) )
14	7 10 12 13	syl3anc	|- ( ( A e. CC /\ N e. NN ) -> ( A ^c ( ( 1 / N ) x. N ) ) = ( ( A ^c ( 1 / N ) ) ^ N ) )
15		cxp1	|- ( A e. CC -> ( A ^c 1 ) = A )
16	15	adantr	|- ( ( A e. CC /\ N e. NN ) -> ( A ^c 1 ) = A )
17	6 14 16	3eqtr3d	|- ( ( A e. CC /\ N e. NN ) -> ( ( A ^c ( 1 / N ) ) ^ N ) = A )