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 ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴𝑁 ) = 𝐵 ↔ ∃ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) 𝐴 = ( ( 𝐵𝑐 ( 1 / 𝑁 ) ) · ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑛 ) ) ) )

Proof

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