This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cxproot

Description: The complex power function allows 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 )