Metamath Proof Explorer


Theorem 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 1 2 N O -1 N

Proof

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