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 eqtrid ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ ) ∧ 𝐴 ≠ 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 bitrid ⊢ ( 𝑛 = ( 𝑚 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 mulridd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ ) ∧ 𝑛 ∈ ( 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 / 𝑁 ) ) ↑ 𝑛 ) ) ) )