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

Metamath Proof Explorer

Theorem cxpeq

Description: Solve an equation involving an N -th power. The expression -u 1 ^c ( 2 / N ) = exp ( 2pi i / N ) is a way to write the primitive N -th root of unity with the smallest positive argument. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion cxpeq 
|- ( ( A e. CC /\ N e. NN /\ B e. CC ) -> ( ( A ^ N ) = B <-> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl2 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> N e. NN )
2 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
3 1 2 syl 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> ( N - 1 ) e. NN0 )
4 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
5 3 4 eleqtrdi 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> ( N - 1 ) e. ( ZZ>= ` 0 ) )
6 eluzfz1 
 |-  ( ( N - 1 ) e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... ( N - 1 ) ) )
7 5 6 syl 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> 0 e. ( 0 ... ( N - 1 ) ) )
8 neg1cn 
 |-  -u 1 e. CC
9 2re 
 |-  2 e. RR
10 simp2 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> N e. NN )
11 nndivre 
 |-  ( ( 2 e. RR /\ N e. NN ) -> ( 2 / N ) e. RR )
12 9 10 11 sylancr 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> ( 2 / N ) e. RR )
13 12 recnd 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> ( 2 / N ) e. CC )
14 cxpcl 
 |-  ( ( -u 1 e. CC /\ ( 2 / N ) e. CC ) -> ( -u 1 ^c ( 2 / N ) ) e. CC )
15 8 13 14 sylancr 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> ( -u 1 ^c ( 2 / N ) ) e. CC )
16 15 adantr 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> ( -u 1 ^c ( 2 / N ) ) e. CC )
17 0nn0 
 |-  0 e. NN0
18 expcl 
 |-  ( ( ( -u 1 ^c ( 2 / N ) ) e. CC /\ 0 e. NN0 ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ 0 ) e. CC )
19 16 17 18 sylancl 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ 0 ) e. CC )
20 19 mul02d 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> ( 0 x. ( ( -u 1 ^c ( 2 / N ) ) ^ 0 ) ) = 0 )
21 simprl 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> A = 0 )
22 21 oveq1d 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> ( A ^ N ) = ( 0 ^ N ) )
23 simprr 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> ( A ^ N ) = B )
24 1 0expd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> ( 0 ^ N ) = 0 )
25 22 23 24 3eqtr3d 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> B = 0 )
26 25 oveq1d 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> ( B ^c ( 1 / N ) ) = ( 0 ^c ( 1 / N ) ) )
27 nncn 
 |-  ( N e. NN -> N e. CC )
28 nnne0 
 |-  ( N e. NN -> N =/= 0 )
29 reccl 
 |-  ( ( N e. CC /\ N =/= 0 ) -> ( 1 / N ) e. CC )
30 recne0 
 |-  ( ( N e. CC /\ N =/= 0 ) -> ( 1 / N ) =/= 0 )
31 29 30 0cxpd 
 |-  ( ( N e. CC /\ N =/= 0 ) -> ( 0 ^c ( 1 / N ) ) = 0 )
32 27 28 31 syl2anc 
 |-  ( N e. NN -> ( 0 ^c ( 1 / N ) ) = 0 )
33 1 32 syl 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> ( 0 ^c ( 1 / N ) ) = 0 )
34 26 33 eqtrd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> ( B ^c ( 1 / N ) ) = 0 )
35 34 oveq1d 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ 0 ) ) = ( 0 x. ( ( -u 1 ^c ( 2 / N ) ) ^ 0 ) ) )
36 20 35 21 3eqtr4rd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ 0 ) ) )
37 oveq2 
 |-  ( n = 0 -> ( ( -u 1 ^c ( 2 / N ) ) ^ n ) = ( ( -u 1 ^c ( 2 / N ) ) ^ 0 ) )
38 37 oveq2d 
 |-  ( n = 0 -> ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ 0 ) ) )
39 38 rspceeqv 
 |-  ( ( 0 e. ( 0 ... ( N - 1 ) ) /\ A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ 0 ) ) ) -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) )
40 7 36 39 syl2anc 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ ( A = 0 /\ ( A ^ N ) = B ) ) -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) )
41 40 expr 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A = 0 ) -> ( ( A ^ N ) = B -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )
42 simpl1 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> A e. CC )
43 simpr 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> A =/= 0 )
44 simpl2 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> N e. NN )
45 44 nnzd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> N e. ZZ )
46 explog 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) = ( exp ` ( N x. ( log ` A ) ) ) )
47 42 43 45 46 syl3anc 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> ( A ^ N ) = ( exp ` ( N x. ( log ` A ) ) ) )
48 47 eqcomd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> ( exp ` ( N x. ( log ` A ) ) ) = ( A ^ N ) )
49 10 nncnd 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> N e. CC )
50 49 adantr 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> N e. CC )
51 42 43 logcld 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> ( log ` A ) e. CC )
52 50 51 mulcld 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> ( N x. ( log ` A ) ) e. CC )
53 44 nnnn0d 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> N e. NN0 )
54 42 53 expcld 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> ( A ^ N ) e. CC )
55 42 43 45 expne0d 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> ( A ^ N ) =/= 0 )
56 eflogeq 
 |-  ( ( ( N x. ( log ` A ) ) e. CC /\ ( A ^ N ) e. CC /\ ( A ^ N ) =/= 0 ) -> ( ( exp ` ( N x. ( log ` A ) ) ) = ( A ^ N ) <-> E. m e. ZZ ( N x. ( log ` A ) ) = ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) ) )
57 52 54 55 56 syl3anc 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> ( ( exp ` ( N x. ( log ` A ) ) ) = ( A ^ N ) <-> E. m e. ZZ ( N x. ( log ` A ) ) = ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) ) )
58 48 57 mpbid 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> E. m e. ZZ ( N x. ( log ` A ) ) = ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) )
59 54 55 logcld 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> ( log ` ( A ^ N ) ) e. CC )
60 59 adantr 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( log ` ( A ^ N ) ) e. CC )
61 ax-icn 
 |-  _i e. CC
62 2cn 
 |-  2 e. CC
63 picn 
 |-  _pi e. CC
64 62 63 mulcli 
 |-  ( 2 x. _pi ) e. CC
65 61 64 mulcli 
 |-  ( _i x. ( 2 x. _pi ) ) e. CC
66 zcn 
 |-  ( m e. ZZ -> m e. CC )
67 66 adantl 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> m e. CC )
68 mulcl 
 |-  ( ( ( _i x. ( 2 x. _pi ) ) e. CC /\ m e. CC ) -> ( ( _i x. ( 2 x. _pi ) ) x. m ) e. CC )
69 65 67 68 sylancr 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( _i x. ( 2 x. _pi ) ) x. m ) e. CC )
70 60 69 addcld 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) e. CC )
71 50 adantr 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> N e. CC )
72 51 adantr 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( log ` A ) e. CC )
73 10 nnne0d 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> N =/= 0 )
74 73 ad2antrr 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> N =/= 0 )
75 70 71 72 74 divmuld 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) / N ) = ( log ` A ) <-> ( N x. ( log ` A ) ) = ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) ) )
76 fveq2 
 |-  ( ( ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) / N ) = ( log ` A ) -> ( exp ` ( ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) / N ) ) = ( exp ` ( log ` A ) ) )
77 71 74 reccld 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( 1 / N ) e. CC )
78 77 60 mulcld 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( 1 / N ) x. ( log ` ( A ^ N ) ) ) e. CC )
79 13 ad2antrr 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( 2 / N ) e. CC )
80 79 67 mulcld 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( 2 / N ) x. m ) e. CC )
81 61 63 mulcli 
 |-  ( _i x. _pi ) e. CC
82 mulcl 
 |-  ( ( ( ( 2 / N ) x. m ) e. CC /\ ( _i x. _pi ) e. CC ) -> ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) e. CC )
83 80 81 82 sylancl 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) e. CC )
84 efadd 
 |-  ( ( ( ( 1 / N ) x. ( log ` ( A ^ N ) ) ) e. CC /\ ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) e. CC ) -> ( exp ` ( ( ( 1 / N ) x. ( log ` ( A ^ N ) ) ) + ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) ) ) = ( ( exp ` ( ( 1 / N ) x. ( log ` ( A ^ N ) ) ) ) x. ( exp ` ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) ) ) )
85 78 83 84 syl2anc 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( exp ` ( ( ( 1 / N ) x. ( log ` ( A ^ N ) ) ) + ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) ) ) = ( ( exp ` ( ( 1 / N ) x. ( log ` ( A ^ N ) ) ) ) x. ( exp ` ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) ) ) )
86 60 69 71 74 divdird 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) / N ) = ( ( ( log ` ( A ^ N ) ) / N ) + ( ( ( _i x. ( 2 x. _pi ) ) x. m ) / N ) ) )
87 60 71 74 divrec2d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( log ` ( A ^ N ) ) / N ) = ( ( 1 / N ) x. ( log ` ( A ^ N ) ) ) )
88 65 a1i 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( _i x. ( 2 x. _pi ) ) e. CC )
89 88 67 71 74 div23d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( _i x. ( 2 x. _pi ) ) x. m ) / N ) = ( ( ( _i x. ( 2 x. _pi ) ) / N ) x. m ) )
90 61 62 63 mul12i 
 |-  ( _i x. ( 2 x. _pi ) ) = ( 2 x. ( _i x. _pi ) )
91 90 oveq1i 
 |-  ( ( _i x. ( 2 x. _pi ) ) / N ) = ( ( 2 x. ( _i x. _pi ) ) / N )
92 62 a1i 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> 2 e. CC )
93 81 a1i 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( _i x. _pi ) e. CC )
94 92 93 71 74 div23d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( 2 x. ( _i x. _pi ) ) / N ) = ( ( 2 / N ) x. ( _i x. _pi ) ) )
95 91 94 eqtrid 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( _i x. ( 2 x. _pi ) ) / N ) = ( ( 2 / N ) x. ( _i x. _pi ) ) )
96 95 oveq1d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( _i x. ( 2 x. _pi ) ) / N ) x. m ) = ( ( ( 2 / N ) x. ( _i x. _pi ) ) x. m ) )
97 79 93 67 mul32d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( 2 / N ) x. ( _i x. _pi ) ) x. m ) = ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) )
98 89 96 97 3eqtrd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( _i x. ( 2 x. _pi ) ) x. m ) / N ) = ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) )
99 87 98 oveq12d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( log ` ( A ^ N ) ) / N ) + ( ( ( _i x. ( 2 x. _pi ) ) x. m ) / N ) ) = ( ( ( 1 / N ) x. ( log ` ( A ^ N ) ) ) + ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) ) )
100 86 99 eqtrd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) / N ) = ( ( ( 1 / N ) x. ( log ` ( A ^ N ) ) ) + ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) ) )
101 100 fveq2d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( exp ` ( ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) / N ) ) = ( exp ` ( ( ( 1 / N ) x. ( log ` ( A ^ N ) ) ) + ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) ) ) )
102 54 adantr 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( A ^ N ) e. CC )
103 55 adantr 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( A ^ N ) =/= 0 )
104 102 103 77 cxpefd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( A ^ N ) ^c ( 1 / N ) ) = ( exp ` ( ( 1 / N ) x. ( log ` ( A ^ N ) ) ) ) )
105 8 a1i 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> -u 1 e. CC )
106 neg1ne0 
 |-  -u 1 =/= 0
107 106 a1i 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> -u 1 =/= 0 )
108 simpr 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> m e. ZZ )
109 105 107 79 108 cxpmul2zd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( -u 1 ^c ( ( 2 / N ) x. m ) ) = ( ( -u 1 ^c ( 2 / N ) ) ^ m ) )
110 105 107 80 cxpefd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( -u 1 ^c ( ( 2 / N ) x. m ) ) = ( exp ` ( ( ( 2 / N ) x. m ) x. ( log ` -u 1 ) ) ) )
111 logm1 
 |-  ( log ` -u 1 ) = ( _i x. _pi )
112 111 oveq2i 
 |-  ( ( ( 2 / N ) x. m ) x. ( log ` -u 1 ) ) = ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) )
113 112 fveq2i 
 |-  ( exp ` ( ( ( 2 / N ) x. m ) x. ( log ` -u 1 ) ) ) = ( exp ` ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) )
114 110 113 eqtrdi 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( -u 1 ^c ( ( 2 / N ) x. m ) ) = ( exp ` ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) ) )
115 105 79 cxpcld 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( -u 1 ^c ( 2 / N ) ) e. CC )
116 8 a1i 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> -u 1 e. CC )
117 106 a1i 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> -u 1 =/= 0 )
118 116 117 13 cxpne0d 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> ( -u 1 ^c ( 2 / N ) ) =/= 0 )
119 118 ad2antrr 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( -u 1 ^c ( 2 / N ) ) =/= 0 )
120 115 119 108 expclzd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ m ) e. CC )
121 44 adantr 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> N e. NN )
122 108 121 zmodcld 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( m mod N ) e. NN0 )
123 115 122 expcld 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) e. CC )
124 122 nn0zd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( m mod N ) e. ZZ )
125 115 119 124 expne0d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) =/= 0 )
126 115 119 124 108 expsubd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ ( m - ( m mod N ) ) ) = ( ( ( -u 1 ^c ( 2 / N ) ) ^ m ) / ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) ) )
127 121 nnzd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> N e. ZZ )
128 zre 
 |-  ( m e. ZZ -> m e. RR )
129 121 nnrpd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> N e. RR+ )
130 moddifz 
 |-  ( ( m e. RR /\ N e. RR+ ) -> ( ( m - ( m mod N ) ) / N ) e. ZZ )
131 128 129 130 syl2an2 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( m - ( m mod N ) ) / N ) e. ZZ )
132 expmulz 
 |-  ( ( ( ( -u 1 ^c ( 2 / N ) ) e. CC /\ ( -u 1 ^c ( 2 / N ) ) =/= 0 ) /\ ( N e. ZZ /\ ( ( m - ( m mod N ) ) / N ) e. ZZ ) ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ ( N x. ( ( m - ( m mod N ) ) / N ) ) ) = ( ( ( -u 1 ^c ( 2 / N ) ) ^ N ) ^ ( ( m - ( m mod N ) ) / N ) ) )
133 115 119 127 131 132 syl22anc 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ ( N x. ( ( m - ( m mod N ) ) / N ) ) ) = ( ( ( -u 1 ^c ( 2 / N ) ) ^ N ) ^ ( ( m - ( m mod N ) ) / N ) ) )
134 122 nn0cnd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( m mod N ) e. CC )
135 67 134 subcld 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( m - ( m mod N ) ) e. CC )
136 135 71 74 divcan2d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( N x. ( ( m - ( m mod N ) ) / N ) ) = ( m - ( m mod N ) ) )
137 136 oveq2d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ ( N x. ( ( m - ( m mod N ) ) / N ) ) ) = ( ( -u 1 ^c ( 2 / N ) ) ^ ( m - ( m mod N ) ) ) )
138 root1id 
 |-  ( N e. NN -> ( ( -u 1 ^c ( 2 / N ) ) ^ N ) = 1 )
139 121 138 syl 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ N ) = 1 )
140 139 oveq1d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( -u 1 ^c ( 2 / N ) ) ^ N ) ^ ( ( m - ( m mod N ) ) / N ) ) = ( 1 ^ ( ( m - ( m mod N ) ) / N ) ) )
141 1exp 
 |-  ( ( ( m - ( m mod N ) ) / N ) e. ZZ -> ( 1 ^ ( ( m - ( m mod N ) ) / N ) ) = 1 )
142 131 141 syl 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( 1 ^ ( ( m - ( m mod N ) ) / N ) ) = 1 )
143 140 142 eqtrd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( -u 1 ^c ( 2 / N ) ) ^ N ) ^ ( ( m - ( m mod N ) ) / N ) ) = 1 )
144 133 137 143 3eqtr3d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ ( m - ( m mod N ) ) ) = 1 )
145 126 144 eqtr3d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( -u 1 ^c ( 2 / N ) ) ^ m ) / ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) ) = 1 )
146 120 123 125 145 diveq1d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ m ) = ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) )
147 109 114 146 3eqtr3rd 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) = ( exp ` ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) ) )
148 104 147 oveq12d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) ) = ( ( exp ` ( ( 1 / N ) x. ( log ` ( A ^ N ) ) ) ) x. ( exp ` ( ( ( 2 / N ) x. m ) x. ( _i x. _pi ) ) ) ) )
149 85 101 148 3eqtr4d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( exp ` ( ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) / N ) ) = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) ) )
150 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
151 42 43 150 syl2anc 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
152 151 adantr 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( exp ` ( log ` A ) ) = A )
153 149 152 eqeq12d 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( exp ` ( ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) / N ) ) = ( exp ` ( log ` A ) ) <-> ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) ) = A ) )
154 zmodfz 
 |-  ( ( m e. ZZ /\ N e. NN ) -> ( m mod N ) e. ( 0 ... ( N - 1 ) ) )
155 108 121 154 syl2anc 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( m mod N ) e. ( 0 ... ( N - 1 ) ) )
156 eqcom 
 |-  ( A = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) <-> ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) = A )
157 oveq2 
 |-  ( n = ( m mod N ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ n ) = ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) )
158 157 oveq2d 
 |-  ( n = ( m mod N ) -> ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) ) )
159 158 eqeq1d 
 |-  ( n = ( m mod N ) -> ( ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) = A <-> ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) ) = A ) )
160 156 159 bitrid 
 |-  ( n = ( m mod N ) -> ( A = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) <-> ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) ) = A ) )
161 160 rspcev 
 |-  ( ( ( m mod N ) e. ( 0 ... ( N - 1 ) ) /\ ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) ) = A ) -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) )
162 161 ex 
 |-  ( ( m mod N ) e. ( 0 ... ( N - 1 ) ) -> ( ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) ) = A -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )
163 155 162 syl 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ ( m mod N ) ) ) = A -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )
164 153 163 sylbid 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( exp ` ( ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) / N ) ) = ( exp ` ( log ` A ) ) -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )
165 76 164 syl5 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) / N ) = ( log ` A ) -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )
166 75 165 sylbird 
 |-  ( ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) /\ m e. ZZ ) -> ( ( N x. ( log ` A ) ) = ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )
167 166 rexlimdva 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> ( E. m e. ZZ ( N x. ( log ` A ) ) = ( ( log ` ( A ^ N ) ) + ( ( _i x. ( 2 x. _pi ) ) x. m ) ) -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )
168 58 167 mpd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) )
169 oveq1 
 |-  ( ( A ^ N ) = B -> ( ( A ^ N ) ^c ( 1 / N ) ) = ( B ^c ( 1 / N ) ) )
170 169 oveq1d 
 |-  ( ( A ^ N ) = B -> ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) )
171 170 eqeq2d 
 |-  ( ( A ^ N ) = B -> ( A = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) <-> A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )
172 171 rexbidv 
 |-  ( ( A ^ N ) = B -> ( E. n e. ( 0 ... ( N - 1 ) ) A = ( ( ( A ^ N ) ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) <-> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )
173 168 172 syl5ibcom 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ A =/= 0 ) -> ( ( A ^ N ) = B -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )
174 41 173 pm2.61dane 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> ( ( A ^ N ) = B -> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )
175 simp3 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> B e. CC )
176 nnrecre 
 |-  ( N e. NN -> ( 1 / N ) e. RR )
177 176 3ad2ant2 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> ( 1 / N ) e. RR )
178 177 recnd 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> ( 1 / N ) e. CC )
179 175 178 cxpcld 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> ( B ^c ( 1 / N ) ) e. CC )
180 179 adantr 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( B ^c ( 1 / N ) ) e. CC )
181 elfznn0 
 |-  ( n e. ( 0 ... ( N - 1 ) ) -> n e. NN0 )
182 expcl 
 |-  ( ( ( -u 1 ^c ( 2 / N ) ) e. CC /\ n e. NN0 ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ n ) e. CC )
183 15 181 182 syl2an 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ n ) e. CC )
184 10 adantr 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> N e. NN )
185 184 nnnn0d 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> N e. NN0 )
186 180 183 185 mulexpd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ^ N ) = ( ( ( B ^c ( 1 / N ) ) ^ N ) x. ( ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ^ N ) ) )
187 175 adantr 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> B e. CC )
188 cxproot 
 |-  ( ( B e. CC /\ N e. NN ) -> ( ( B ^c ( 1 / N ) ) ^ N ) = B )
189 187 184 188 syl2anc 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( B ^c ( 1 / N ) ) ^ N ) = B )
190 181 adantl 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> n e. NN0 )
191 190 nn0cnd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> n e. CC )
192 184 nncnd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> N e. CC )
193 191 192 mulcomd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( n x. N ) = ( N x. n ) )
194 193 oveq2d 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ ( n x. N ) ) = ( ( -u 1 ^c ( 2 / N ) ) ^ ( N x. n ) ) )
195 15 adantr 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( -u 1 ^c ( 2 / N ) ) e. CC )
196 195 185 190 expmuld 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ ( n x. N ) ) = ( ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ^ N ) )
197 195 190 185 expmuld 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ ( N x. n ) ) = ( ( ( -u 1 ^c ( 2 / N ) ) ^ N ) ^ n ) )
198 194 196 197 3eqtr3d 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ^ N ) = ( ( ( -u 1 ^c ( 2 / N ) ) ^ N ) ^ n ) )
199 184 138 syl 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ N ) = 1 )
200 199 oveq1d 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( -u 1 ^c ( 2 / N ) ) ^ N ) ^ n ) = ( 1 ^ n ) )
201 elfzelz 
 |-  ( n e. ( 0 ... ( N - 1 ) ) -> n e. ZZ )
202 201 adantl 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> n e. ZZ )
203 1exp 
 |-  ( n e. ZZ -> ( 1 ^ n ) = 1 )
204 202 203 syl 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ^ n ) = 1 )
205 198 200 204 3eqtrd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ^ N ) = 1 )
206 189 205 oveq12d 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( B ^c ( 1 / N ) ) ^ N ) x. ( ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ^ N ) ) = ( B x. 1 ) )
207 187 mulridd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( B x. 1 ) = B )
208 186 206 207 3eqtrd 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ^ N ) = B )
209 oveq1 
 |-  ( A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) -> ( A ^ N ) = ( ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ^ N ) )
210 209 eqeq1d 
 |-  ( A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) -> ( ( A ^ N ) = B <-> ( ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ^ N ) = B ) )
211 208 210 syl5ibrcom 
 |-  ( ( ( A e. CC /\ N e. NN /\ B e. CC ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) -> ( A ^ N ) = B ) )
212 211 rexlimdva 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> ( E. n e. ( 0 ... ( N - 1 ) ) A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) -> ( A ^ N ) = B ) )
213 174 212 impbid 
 |-  ( ( A e. CC /\ N e. NN /\ B e. CC ) -> ( ( A ^ N ) = B <-> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )