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 ` CCfld ) |`s ( CC \ { 0 } ) )
proot1ex.o 
|- O = ( od ` G )
Assertion proot1ex 
|- ( N e. NN -> ( -u 1 ^c ( 2 / N ) ) e. ( `' O " { N } ) )

Proof

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