proot1ex

Description: The complex field has primitive N -th roots of unity for all N . (Contributed by Stefan O'Rear, 12-Sep-2015)

	Ref	Expression
Hypotheses	proot1ex.g	$⊢ G = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})$
	proot1ex.o	$⊢ O = od (G)$
Assertion	proot1ex	$⊢ N \in ℕ \to {(- 1)}^{\frac{2}{N}} \in O^{-1} [\{N\}]$

Proof

Step	Hyp	Ref	Expression
1		proot1ex.g	$⊢ G = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})$
2		proot1ex.o	$⊢ O = od (G)$
3		neg1cn	$⊢ - 1 \in ℂ$
4		2rp	$⊢ 2 \in ℝ^{+}$
5		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
6		rpdivcl	$⊢ (2 \in ℝ^{+} \land N \in ℝ^{+}) \to \frac{2}{N} \in ℝ^{+}$
7	4 5 6	sylancr	$⊢ N \in ℕ \to \frac{2}{N} \in ℝ^{+}$
8	7	rpcnd	$⊢ N \in ℕ \to \frac{2}{N} \in ℂ$
9		cxpcl	$⊢ (- 1 \in ℂ \land \frac{2}{N} \in ℂ) \to {(- 1)}^{\frac{2}{N}} \in ℂ$
10	3 8 9	sylancr	$⊢ N \in ℕ \to {(- 1)}^{\frac{2}{N}} \in ℂ$
11	3	a1i	$⊢ N \in ℕ \to - 1 \in ℂ$
12		neg1ne0	$⊢ - 1 \neq 0$
13	12	a1i	$⊢ N \in ℕ \to - 1 \neq 0$
14	11 13 8	cxpne0d	$⊢ N \in ℕ \to {(- 1)}^{\frac{2}{N}} \neq 0$
15		eldifsn	$⊢ {(- 1)}^{\frac{2}{N}} \in (ℂ ∖ \{0\}) \leftrightarrow ({(- 1)}^{\frac{2}{N}} \in ℂ \land {(- 1)}^{\frac{2}{N}} \neq 0)$
16	10 14 15	sylanbrc	$⊢ N \in ℕ \to {(- 1)}^{\frac{2}{N}} \in (ℂ ∖ \{0\})$
17	3	a1i	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to - 1 \in ℂ$
18	12	a1i	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to - 1 \neq 0$
19		nn0cn	$⊢ x \in ℕ_{0} \to x \in ℂ$
20		mulcl	$⊢ (\frac{2}{N} \in ℂ \land x \in ℂ) \to (\frac{2}{N}) x \in ℂ$
21	8 19 20	syl2an	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to (\frac{2}{N}) x \in ℂ$
22	17 18 21	cxpefd	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to {(- 1)}^{(\frac{2}{N}) x} = e^{(\frac{2}{N}) x \log -1}$
23	22	eqeq1d	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to ({(- 1)}^{(\frac{2}{N}) x} = 1 \leftrightarrow e^{(\frac{2}{N}) x \log -1} = 1)$
24		logcl	$⊢ (- 1 \in ℂ \land - 1 \neq 0) \to \log -1 \in ℂ$
25	3 12 24	mp2an	$⊢ \log -1 \in ℂ$
26		mulcl	$⊢ ((\frac{2}{N}) x \in ℂ \land \log -1 \in ℂ) \to (\frac{2}{N}) x \log -1 \in ℂ$
27	21 25 26	sylancl	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to (\frac{2}{N}) x \log -1 \in ℂ$
28		efeq1	$⊢ (\frac{2}{N}) x \log -1 \in ℂ \to (e^{(\frac{2}{N}) x \log -1} = 1 \leftrightarrow \frac{(\frac{2}{N}) x \log -1}{i 2 π} \in ℤ)$
29	27 28	syl	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to (e^{(\frac{2}{N}) x \log -1} = 1 \leftrightarrow \frac{(\frac{2}{N}) x \log -1}{i 2 π} \in ℤ)$
30		2cn	$⊢ 2 \in ℂ$
31	30	a1i	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to 2 \in ℂ$
32		nncn	$⊢ N \in ℕ \to N \in ℂ$
33	32	adantr	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to N \in ℂ$
34	19	adantl	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to x \in ℂ$
35		nnne0	$⊢ N \in ℕ \to N \neq 0$
36	35	adantr	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to N \neq 0$
37	31 33 34 36	div13d	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to (\frac{2}{N}) x = (\frac{x}{N}) \cdot 2$
38		logm1	$⊢ \log -1 = i π$
39	38	a1i	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to \log -1 = i π$
40	37 39	oveq12d	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to (\frac{2}{N}) x \log -1 = (\frac{x}{N}) \cdot 2 i π$
41	34 33 36	divcld	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to \frac{x}{N} \in ℂ$
42		ax-icn	$⊢ i \in ℂ$
43		picn	$⊢ π \in ℂ$
44	42 43	mulcli	$⊢ i π \in ℂ$
45	44	a1i	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to i π \in ℂ$
46	41 31 45	mulassd	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to (\frac{x}{N}) \cdot 2 i π = (\frac{x}{N}) 2 i π$
47	42	a1i	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to i \in ℂ$
48	43	a1i	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to π \in ℂ$
49	31 47 48	mul12d	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to 2 i π = i 2 π$
50	49	oveq2d	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to (\frac{x}{N}) 2 i π = (\frac{x}{N}) i 2 π$
51	40 46 50	3eqtrd	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to (\frac{2}{N}) x \log -1 = (\frac{x}{N}) i 2 π$
52	51	oveq1d	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to \frac{(\frac{2}{N}) x \log -1}{i 2 π} = \frac{(\frac{x}{N}) i 2 π}{i 2 π}$
53	30 43	mulcli	$⊢ 2 π \in ℂ$
54	42 53	mulcli	$⊢ i 2 π \in ℂ$
55	54	a1i	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to i 2 π \in ℂ$
56		ine0	$⊢ i \neq 0$
57		2ne0	$⊢ 2 \neq 0$
58		pire	$⊢ π \in ℝ$
59		pipos	$⊢ 0 < π$
60	58 59	gt0ne0ii	$⊢ π \neq 0$
61	30 43 57 60	mulne0i	$⊢ 2 π \neq 0$
62	42 53 56 61	mulne0i	$⊢ i 2 π \neq 0$
63	62	a1i	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to i 2 π \neq 0$
64	41 55 63	divcan4d	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to \frac{(\frac{x}{N}) i 2 π}{i 2 π} = \frac{x}{N}$
65	52 64	eqtrd	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to \frac{(\frac{2}{N}) x \log -1}{i 2 π} = \frac{x}{N}$
66	65	eleq1d	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to (\frac{(\frac{2}{N}) x \log -1}{i 2 π} \in ℤ \leftrightarrow \frac{x}{N} \in ℤ)$
67	23 29 66	3bitrd	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to ({(- 1)}^{(\frac{2}{N}) x} = 1 \leftrightarrow \frac{x}{N} \in ℤ)$
68	8	adantr	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to \frac{2}{N} \in ℂ$
69		simpr	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to x \in ℕ_{0}$
70	17 68 69	cxpmul2d	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to {(- 1)}^{(\frac{2}{N}) x} = {({-1}^{\frac{2}{N}})}^{x}$
71		cnfldexp	$⊢ ({(- 1)}^{\frac{2}{N}} \in ℂ \land x \in ℕ_{0}) \to x \cdot_{{mulGrp}_{ℂ_{fld}}} {(- 1)}^{\frac{2}{N}} = {({-1}^{\frac{2}{N}})}^{x}$
72	10 71	sylan	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to x \cdot_{{mulGrp}_{ℂ_{fld}}} {(- 1)}^{\frac{2}{N}} = {({-1}^{\frac{2}{N}})}^{x}$
73		cnring	$⊢ ℂ_{fld} \in Ring$
74		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
75		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
76		cndrng	$⊢ ℂ_{fld} \in DivRing$
77	74 75 76	drngui	$⊢ ℂ ∖ \{0\} = Unit (ℂ_{fld})$
78		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
79	77 78	unitsubm	$⊢ ℂ_{fld} \in Ring \to ℂ ∖ \{0\} \in SubMnd ({mulGrp}_{ℂ_{fld}})$
80	73 79	mp1i	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to ℂ ∖ \{0\} \in SubMnd ({mulGrp}_{ℂ_{fld}})$
81	16	adantr	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to {(- 1)}^{\frac{2}{N}} \in (ℂ ∖ \{0\})$
82		eqid	$⊢ \cdot_{{mulGrp}_{ℂ_{fld}}} = \cdot_{{mulGrp}_{ℂ_{fld}}}$
83		eqid	$⊢ \cdot_{G} = \cdot_{G}$
84	82 1 83	submmulg	$⊢ (ℂ ∖ \{0\} \in SubMnd ({mulGrp}_{ℂ_{fld}}) \land x \in ℕ_{0} \land {(- 1)}^{\frac{2}{N}} \in (ℂ ∖ \{0\})) \to x \cdot_{{mulGrp}_{ℂ_{fld}}} {(- 1)}^{\frac{2}{N}} = x \cdot_{G} {(- 1)}^{\frac{2}{N}}$
85	80 69 81 84	syl3anc	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to x \cdot_{{mulGrp}_{ℂ_{fld}}} {(- 1)}^{\frac{2}{N}} = x \cdot_{G} {(- 1)}^{\frac{2}{N}}$
86	70 72 85	3eqtr2rd	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to x \cdot_{G} {(- 1)}^{\frac{2}{N}} = {(- 1)}^{(\frac{2}{N}) x}$
87	86	eqeq1d	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to (x \cdot_{G} {(- 1)}^{\frac{2}{N}} = 1 \leftrightarrow {(- 1)}^{(\frac{2}{N}) x} = 1)$
88		nnz	$⊢ N \in ℕ \to N \in ℤ$
89	88	adantr	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to N \in ℤ$
90		nn0z	$⊢ x \in ℕ_{0} \to x \in ℤ$
91	90	adantl	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to x \in ℤ$
92		dvdsval2	$⊢ (N \in ℤ \land N \neq 0 \land x \in ℤ) \to (N ∥ x \leftrightarrow \frac{x}{N} \in ℤ)$
93	89 36 91 92	syl3anc	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to (N ∥ x \leftrightarrow \frac{x}{N} \in ℤ)$
94	67 87 93	3bitr4rd	$⊢ (N \in ℕ \land x \in ℕ_{0}) \to (N ∥ x \leftrightarrow x \cdot_{G} {(- 1)}^{\frac{2}{N}} = 1)$
95	94	ralrimiva	$⊢ N \in ℕ \to \forall x \in ℕ_{0} (N ∥ x \leftrightarrow x \cdot_{G} {(- 1)}^{\frac{2}{N}} = 1)$
96	77 1	unitgrp	$⊢ ℂ_{fld} \in Ring \to G \in Grp$
97	73 96	mp1i	$⊢ N \in ℕ \to G \in Grp$
98		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
99	77 1	unitgrpbas	$⊢ ℂ ∖ \{0\} = {Base}_{G}$
100		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
101	77 1 100	unitgrpid	$⊢ ℂ_{fld} \in Ring \to 1 = 0_{G}$
102	73 101	ax-mp	$⊢ 1 = 0_{G}$
103	99 2 83 102	odeq	$⊢ (G \in Grp \land {(- 1)}^{\frac{2}{N}} \in (ℂ ∖ \{0\}) \land N \in ℕ_{0}) \to (N = O ({(- 1)}^{\frac{2}{N}}) \leftrightarrow \forall x \in ℕ_{0} (N ∥ x \leftrightarrow x \cdot_{G} {(- 1)}^{\frac{2}{N}} = 1))$
104	97 16 98 103	syl3anc	$⊢ N \in ℕ \to (N = O ({(- 1)}^{\frac{2}{N}}) \leftrightarrow \forall x \in ℕ_{0} (N ∥ x \leftrightarrow x \cdot_{G} {(- 1)}^{\frac{2}{N}} = 1))$
105	95 104	mpbird	$⊢ N \in ℕ \to N = O ({(- 1)}^{\frac{2}{N}})$
106	105	eqcomd	$⊢ N \in ℕ \to O ({(- 1)}^{\frac{2}{N}}) = N$
107	99 2	odf	$⊢ O : ℂ ∖ \{0\} ⟶ ℕ_{0}$
108		ffn	$⊢ O : ℂ ∖ \{0\} ⟶ ℕ_{0} \to O Fn (ℂ ∖ \{0\})$
109	107 108	ax-mp	$⊢ O Fn (ℂ ∖ \{0\})$
110		fniniseg	$⊢ O Fn (ℂ ∖ \{0\}) \to ({(- 1)}^{\frac{2}{N}} \in O^{-1} [\{N\}] \leftrightarrow ({(- 1)}^{\frac{2}{N}} \in (ℂ ∖ \{0\}) \land O ({(- 1)}^{\frac{2}{N}}) = N))$
111	109 110	mp1i	$⊢ N \in ℕ \to ({(- 1)}^{\frac{2}{N}} \in O^{-1} [\{N\}] \leftrightarrow ({(- 1)}^{\frac{2}{N}} \in (ℂ ∖ \{0\}) \land O ({(- 1)}^{\frac{2}{N}}) = N))$
112	16 106 111	mpbir2and	$⊢ N \in ℕ \to {(- 1)}^{\frac{2}{N}} \in O^{-1} [\{N\}]$

Metamath Proof Explorer

Theorem proot1ex

Proof