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 ) ∈ ℕ₀ )
3	1 2	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐴 = 0 ∧ ( 𝐴 ↑ 𝑁 ) = 𝐵 ) ) → ( 𝑁 − 1 ) ∈ ℕ₀ )
4		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 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 ∈ ℕ₀
18		expcl	⊢ ( ( ( - 1 ↑_𝑐 ( 2 / 𝑁 ) ) ∈ ℂ ∧ 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 ) → 𝑁 ∈ ℕ₀ )
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 𝑁 ) ∈ ℕ₀ )
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 ) ) → 𝑛 ∈ ℕ₀ )
182		expcl	⊢ ( ( ( - 1 ↑_𝑐 ( 2 / 𝑁 ) ) ∈ ℂ ∧ 𝑛 ∈ ℕ₀ ) → ( ( - 1 ↑_𝑐 ( 2 / 𝑁 ) ) ↑ 𝑛 ) ∈ ℂ )
183	15 181 182	syl2an	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( - 1 ↑_𝑐 ( 2 / 𝑁 ) ) ↑ 𝑛 ) ∈ ℂ )
184	10	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℕ )
185	184	nnnn0d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℂ ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℕ₀ )
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 ) ) ) → 𝑛 ∈ ℕ₀ )
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 / 𝑁 ) ) ↑ 𝑛 ) ) ) )

Metamath Proof Explorer

Theorem cxpeq

Proof