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 \in ℂ \land N \in ℕ \land B \in ℂ) \to (A^{N} = B \leftrightarrow \exists n \in (0 \dots N - 1) A = B^{\frac{1}{N}} {({-1}^{\frac{2}{N}})}^{n})$

Proof

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

Metamath Proof Explorer

Theorem cxpeq

Proof