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 syl5eq
 |-  ( ( ( ( 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 syl5bb
 |-  ( 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 mulid1d
 |-  ( ( ( 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 ) ) ) )