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 ⊢ 𝐺 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
proot1ex.o ⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion proot1ex ( 𝑁 ∈ ℕ → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ( ◡ 𝑂 “ { 𝑁 } ) )

Proof

Step Hyp Ref Expression
1 proot1ex.g ⊢ 𝐺 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
2 proot1ex.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 neg1cn ⊢ - 1 ∈ ℂ
4 2rp ⊢ 2 ∈ ℝ+
5 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
6 rpdivcl ⊢ ( ( 2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) → ( 2 / 𝑁 ) ∈ ℝ+ )
7 4 5 6 sylancr ⊢ ( 𝑁 ∈ ℕ → ( 2 / 𝑁 ) ∈ ℝ+ )
8 7 rpcnd ⊢ ( 𝑁 ∈ ℕ → ( 2 / 𝑁 ) ∈ ℂ )
9 cxpcl ⊢ ( ( - 1 ∈ ℂ ∧ ( 2 / 𝑁 ) ∈ ℂ ) → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ℂ )
10 3 8 9 sylancr ⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ℂ )
11 3 a1i ⊢ ( 𝑁 ∈ ℕ → - 1 ∈ ℂ )
12 neg1ne0 ⊢ - 1 ≠ 0
13 12 a1i ⊢ ( 𝑁 ∈ ℕ → - 1 ≠ 0 )
14 11 13 8 cxpne0d ⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ≠ 0 )
15 eldifsn ⊢ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ℂ ∧ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ≠ 0 ) )
16 10 14 15 sylanbrc ⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ( ℂ ∖ { 0 } ) )
17 3 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → - 1 ∈ ℂ )
18 12 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → - 1 ≠ 0 )
19 nn0cn ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℂ )
20 mulcl ⊢ ( ( ( 2 / 𝑁 ) ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( 2 / 𝑁 ) · 𝑥 ) ∈ ℂ )
21 8 19 20 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( 2 / 𝑁 ) · 𝑥 ) ∈ ℂ )
22 17 18 21 cxpefd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( - 1 ↑𝑐 ( ( 2 / 𝑁 ) · 𝑥 ) ) = ( exp ‘ ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) ) )
23 22 eqeq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( - 1 ↑𝑐 ( ( 2 / 𝑁 ) · 𝑥 ) ) = 1 ↔ ( exp ‘ ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) ) = 1 ) )
24 logcl ⊢ ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) → ( log ‘ - 1 ) ∈ ℂ )
25 3 12 24 mp2an ⊢ ( log ‘ - 1 ) ∈ ℂ
26 mulcl ⊢ ( ( ( ( 2 / 𝑁 ) · 𝑥 ) ∈ ℂ ∧ ( log ‘ - 1 ) ∈ ℂ ) → ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) ∈ ℂ )
27 21 25 26 sylancl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) ∈ ℂ )
28 efeq1 ⊢ ( ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) ∈ ℂ → ( ( exp ‘ ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) ) = 1 ↔ ( ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
29 27 28 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( exp ‘ ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) ) = 1 ↔ ( ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
30 2cn ⊢ 2 ∈ ℂ
31 30 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → 2 ∈ ℂ )
32 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
33 32 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
34 19 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℂ )
35 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
36 35 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → 𝑁 ≠ 0 )
37 31 33 34 36 div13d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( 2 / 𝑁 ) · 𝑥 ) = ( ( 𝑥 / 𝑁 ) · 2 ) )
38 logm1 ⊢ ( log ‘ - 1 ) = ( i · π )
39 38 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( log ‘ - 1 ) = ( i · π ) )
40 37 39 oveq12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) = ( ( ( 𝑥 / 𝑁 ) · 2 ) · ( i · π ) ) )
41 34 33 36 divcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 / 𝑁 ) ∈ ℂ )
42 ax-icn ⊢ i ∈ ℂ
43 picn ⊢ π ∈ ℂ
44 42 43 mulcli ⊢ ( i · π ) ∈ ℂ
45 44 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( i · π ) ∈ ℂ )
46 41 31 45 mulassd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑥 / 𝑁 ) · 2 ) · ( i · π ) ) = ( ( 𝑥 / 𝑁 ) · ( 2 · ( i · π ) ) ) )
47 42 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → i ∈ ℂ )
48 43 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → π ∈ ℂ )
49 31 47 48 mul12d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( 2 · ( i · π ) ) = ( i · ( 2 · π ) ) )
50 49 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 / 𝑁 ) · ( 2 · ( i · π ) ) ) = ( ( 𝑥 / 𝑁 ) · ( i · ( 2 · π ) ) ) )
51 40 46 50 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) = ( ( 𝑥 / 𝑁 ) · ( i · ( 2 · π ) ) ) )
52 51 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) / ( i · ( 2 · π ) ) ) = ( ( ( 𝑥 / 𝑁 ) · ( i · ( 2 · π ) ) ) / ( i · ( 2 · π ) ) ) )
53 30 43 mulcli ⊢ ( 2 · π ) ∈ ℂ
54 42 53 mulcli ⊢ ( i · ( 2 · π ) ) ∈ ℂ
55 54 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ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 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( i · ( 2 · π ) ) ≠ 0 )
64 41 55 63 divcan4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑥 / 𝑁 ) · ( i · ( 2 · π ) ) ) / ( i · ( 2 · π ) ) ) = ( 𝑥 / 𝑁 ) )
65 52 64 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) / ( i · ( 2 · π ) ) ) = ( 𝑥 / 𝑁 ) )
66 65 eleq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( ( ( ( 2 / 𝑁 ) · 𝑥 ) · ( log ‘ - 1 ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ↔ ( 𝑥 / 𝑁 ) ∈ ℤ ) )
67 23 29 66 3bitrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( - 1 ↑𝑐 ( ( 2 / 𝑁 ) · 𝑥 ) ) = 1 ↔ ( 𝑥 / 𝑁 ) ∈ ℤ ) )
68 8 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( 2 / 𝑁 ) ∈ ℂ )
69 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℕ0 )
70 17 68 69 cxpmul2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( - 1 ↑𝑐 ( ( 2 / 𝑁 ) · 𝑥 ) ) = ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑥 ) )
71 cnfldexp ⊢ ( ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ℂ ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑥 ) )
72 10 71 sylan ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑥 ) )
73 cnring ⊢ ℂfld ∈ Ring
74 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
75 cnfld0 ⊢ 0 = ( 0g ‘ ℂ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 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
81 16 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ( ℂ ∖ { 0 } ) )
82 eqid ⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
83 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
84 82 1 83 submmulg ⊢ ( ( ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) ∧ 𝑥 ∈ ℕ0 ∧ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = ( 𝑥 ( .g ‘ 𝐺 ) ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) )
85 80 69 81 84 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = ( 𝑥 ( .g ‘ 𝐺 ) ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) )
86 70 72 85 3eqtr2rd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 ( .g ‘ 𝐺 ) ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = ( - 1 ↑𝑐 ( ( 2 / 𝑁 ) · 𝑥 ) ) )
87 86 eqeq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑥 ( .g ‘ 𝐺 ) ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = 1 ↔ ( - 1 ↑𝑐 ( ( 2 / 𝑁 ) · 𝑥 ) ) = 1 ) )
88 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
89 88 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
90 nn0z ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℤ )
91 90 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℤ )
92 dvdsval2 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ 𝑥 ∈ ℤ ) → ( 𝑁 ∥ 𝑥 ↔ ( 𝑥 / 𝑁 ) ∈ ℤ ) )
93 89 36 91 92 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( 𝑁 ∥ 𝑥 ↔ ( 𝑥 / 𝑁 ) ∈ ℤ ) )
94 67 87 93 3bitr4rd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ℕ0 ) → ( 𝑁 ∥ 𝑥 ↔ ( 𝑥 ( .g ‘ 𝐺 ) ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = 1 ) )
95 94 ralrimiva ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑥 ∈ ℕ0 ( 𝑁 ∥ 𝑥 ↔ ( 𝑥 ( .g ‘ 𝐺 ) ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = 1 ) )
96 77 1 unitgrp ⊢ ( ℂfld ∈ Ring → 𝐺 ∈ Grp )
97 73 96 mp1i ⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Grp )
98 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
99 77 1 unitgrpbas ⊢ ( ℂ ∖ { 0 } ) = ( Base ‘ 𝐺 )
100 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
101 77 1 100 unitgrpid ⊢ ( ℂfld ∈ Ring → 1 = ( 0g ‘ 𝐺 ) )
102 73 101 ax-mp ⊢ 1 = ( 0g ‘ 𝐺 )
103 99 2 83 102 odeq ⊢ ( ( 𝐺 ∈ Grp ∧ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ( ℂ ∖ { 0 } ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 = ( 𝑂 ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑁 ∥ 𝑥 ↔ ( 𝑥 ( .g ‘ 𝐺 ) ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = 1 ) ) )
104 97 16 98 103 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = ( 𝑂 ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑁 ∥ 𝑥 ↔ ( 𝑥 ( .g ‘ 𝐺 ) ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = 1 ) ) )
105 95 104 mpbird ⊢ ( 𝑁 ∈ ℕ → 𝑁 = ( 𝑂 ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) )
106 105 eqcomd ⊢ ( 𝑁 ∈ ℕ → ( 𝑂 ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = 𝑁 )
107 99 2 odf ⊢ 𝑂 : ( ℂ ∖ { 0 } ) ⟶ ℕ0
108 ffn ⊢ ( 𝑂 : ( ℂ ∖ { 0 } ) ⟶ ℕ0 → 𝑂 Fn ( ℂ ∖ { 0 } ) )
109 107 108 ax-mp ⊢ 𝑂 Fn ( ℂ ∖ { 0 } )
110 fniniseg ⊢ ( 𝑂 Fn ( ℂ ∖ { 0 } ) → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↔ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ( ℂ ∖ { 0 } ) ∧ ( 𝑂 ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = 𝑁 ) ) )
111 109 110 mp1i ⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ( ◡ 𝑂 “ { 𝑁 } ) ↔ ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ( ℂ ∖ { 0 } ) ∧ ( 𝑂 ‘ ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ) = 𝑁 ) ) )
112 16 106 111 mpbir2and ⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ∈ ( ◡ 𝑂 “ { 𝑁 } ) )