Metamath Proof Explorer


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 )