Metamath Proof Explorer

Theorem 1cubrlem

Description: The cube roots of unity. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion 1cubrlem ( ( - 1 ↑𝑐 ( 2 / 3 ) ) = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ∧ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 2 ) = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 neg1cn ⊢ - 1 ∈ ℂ
2 neg1ne0 ⊢ - 1 ≠ 0
3 2re ⊢ 2 ∈ ℝ
4 3nn ⊢ 3 ∈ ℕ
5 nndivre ⊢ ( ( 2 ∈ ℝ ∧ 3 ∈ ℕ ) → ( 2 / 3 ) ∈ ℝ )
6 3 4 5 mp2an ⊢ ( 2 / 3 ) ∈ ℝ
7 6 recni ⊢ ( 2 / 3 ) ∈ ℂ
8 cxpef ⊢ ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ∧ ( 2 / 3 ) ∈ ℂ ) → ( - 1 ↑𝑐 ( 2 / 3 ) ) = ( exp ‘ ( ( 2 / 3 ) · ( log ‘ - 1 ) ) ) )
9 1 2 7 8 mp3an ⊢ ( - 1 ↑𝑐 ( 2 / 3 ) ) = ( exp ‘ ( ( 2 / 3 ) · ( log ‘ - 1 ) ) )
10 logm1 ⊢ ( log ‘ - 1 ) = ( i · π )
11 10 oveq2i ⊢ ( ( 2 / 3 ) · ( log ‘ - 1 ) ) = ( ( 2 / 3 ) · ( i · π ) )
12 ax-icn ⊢ i ∈ ℂ
13 pire ⊢ π ∈ ℝ
14 13 recni ⊢ π ∈ ℂ
15 7 12 14 mul12i ⊢ ( ( 2 / 3 ) · ( i · π ) ) = ( i · ( ( 2 / 3 ) · π ) )
16 11 15 eqtri ⊢ ( ( 2 / 3 ) · ( log ‘ - 1 ) ) = ( i · ( ( 2 / 3 ) · π ) )
17 16 fveq2i ⊢ ( exp ‘ ( ( 2 / 3 ) · ( log ‘ - 1 ) ) ) = ( exp ‘ ( i · ( ( 2 / 3 ) · π ) ) )
18 6nn ⊢ 6 ∈ ℕ
19 nndivre ⊢ ( ( π ∈ ℝ ∧ 6 ∈ ℕ ) → ( π / 6 ) ∈ ℝ )
20 13 18 19 mp2an ⊢ ( π / 6 ) ∈ ℝ
21 20 recni ⊢ ( π / 6 ) ∈ ℂ
22 coshalfpip ⊢ ( ( π / 6 ) ∈ ℂ → ( cos ‘ ( ( π / 2 ) + ( π / 6 ) ) ) = - ( sin ‘ ( π / 6 ) ) )
23 21 22 ax-mp ⊢ ( cos ‘ ( ( π / 2 ) + ( π / 6 ) ) ) = - ( sin ‘ ( π / 6 ) )
24 2cn ⊢ 2 ∈ ℂ
25 2ne0 ⊢ 2 ≠ 0
26 divrec2 ⊢ ( ( π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( π / 2 ) = ( ( 1 / 2 ) · π ) )
27 14 24 25 26 mp3an ⊢ ( π / 2 ) = ( ( 1 / 2 ) · π )
28 6cn ⊢ 6 ∈ ℂ
29 18 nnne0i ⊢ 6 ≠ 0
30 divrec2 ⊢ ( ( π ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0 ) → ( π / 6 ) = ( ( 1 / 6 ) · π ) )
31 14 28 29 30 mp3an ⊢ ( π / 6 ) = ( ( 1 / 6 ) · π )
32 27 31 oveq12i ⊢ ( ( π / 2 ) + ( π / 6 ) ) = ( ( ( 1 / 2 ) · π ) + ( ( 1 / 6 ) · π ) )
33 24 25 reccli ⊢ ( 1 / 2 ) ∈ ℂ
34 28 29 reccli ⊢ ( 1 / 6 ) ∈ ℂ
35 33 34 14 adddiri ⊢ ( ( ( 1 / 2 ) + ( 1 / 6 ) ) · π ) = ( ( ( 1 / 2 ) · π ) + ( ( 1 / 6 ) · π ) )
36 halfpm6th ⊢ ( ( ( 1 / 2 ) − ( 1 / 6 ) ) = ( 1 / 3 ) ∧ ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 ) )
37 36 simpri ⊢ ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 )
38 37 oveq1i ⊢ ( ( ( 1 / 2 ) + ( 1 / 6 ) ) · π ) = ( ( 2 / 3 ) · π )
39 32 35 38 3eqtr2i ⊢ ( ( π / 2 ) + ( π / 6 ) ) = ( ( 2 / 3 ) · π )
40 39 fveq2i ⊢ ( cos ‘ ( ( π / 2 ) + ( π / 6 ) ) ) = ( cos ‘ ( ( 2 / 3 ) · π ) )
41 sincos6thpi ⊢ ( ( sin ‘ ( π / 6 ) ) = ( 1 / 2 ) ∧ ( cos ‘ ( π / 6 ) ) = ( ( √ ‘ 3 ) / 2 ) )
42 41 simpli ⊢ ( sin ‘ ( π / 6 ) ) = ( 1 / 2 )
43 42 negeqi ⊢ - ( sin ‘ ( π / 6 ) ) = - ( 1 / 2 )
44 ax-1cn ⊢ 1 ∈ ℂ
45 divneg ⊢ ( ( 1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( 1 / 2 ) = ( - 1 / 2 ) )
46 44 24 25 45 mp3an ⊢ - ( 1 / 2 ) = ( - 1 / 2 )
47 43 46 eqtri ⊢ - ( sin ‘ ( π / 6 ) ) = ( - 1 / 2 )
48 23 40 47 3eqtr3i ⊢ ( cos ‘ ( ( 2 / 3 ) · π ) ) = ( - 1 / 2 )
49 sinhalfpip ⊢ ( ( π / 6 ) ∈ ℂ → ( sin ‘ ( ( π / 2 ) + ( π / 6 ) ) ) = ( cos ‘ ( π / 6 ) ) )
50 21 49 ax-mp ⊢ ( sin ‘ ( ( π / 2 ) + ( π / 6 ) ) ) = ( cos ‘ ( π / 6 ) )
51 39 fveq2i ⊢ ( sin ‘ ( ( π / 2 ) + ( π / 6 ) ) ) = ( sin ‘ ( ( 2 / 3 ) · π ) )
52 41 simpri ⊢ ( cos ‘ ( π / 6 ) ) = ( ( √ ‘ 3 ) / 2 )
53 50 51 52 3eqtr3i ⊢ ( sin ‘ ( ( 2 / 3 ) · π ) ) = ( ( √ ‘ 3 ) / 2 )
54 53 oveq2i ⊢ ( i · ( sin ‘ ( ( 2 / 3 ) · π ) ) ) = ( i · ( ( √ ‘ 3 ) / 2 ) )
55 3re ⊢ 3 ∈ ℝ
56 3nn0 ⊢ 3 ∈ ℕ0
57 56 nn0ge0i ⊢ 0 ≤ 3
58 resqrtcl ⊢ ( ( 3 ∈ ℝ ∧ 0 ≤ 3 ) → ( √ ‘ 3 ) ∈ ℝ )
59 55 57 58 mp2an ⊢ ( √ ‘ 3 ) ∈ ℝ
60 59 recni ⊢ ( √ ‘ 3 ) ∈ ℂ
61 12 60 24 25 divassi ⊢ ( ( i · ( √ ‘ 3 ) ) / 2 ) = ( i · ( ( √ ‘ 3 ) / 2 ) )
62 54 61 eqtr4i ⊢ ( i · ( sin ‘ ( ( 2 / 3 ) · π ) ) ) = ( ( i · ( √ ‘ 3 ) ) / 2 )
63 48 62 oveq12i ⊢ ( ( cos ‘ ( ( 2 / 3 ) · π ) ) + ( i · ( sin ‘ ( ( 2 / 3 ) · π ) ) ) ) = ( ( - 1 / 2 ) + ( ( i · ( √ ‘ 3 ) ) / 2 ) )
64 7 14 mulcli ⊢ ( ( 2 / 3 ) · π ) ∈ ℂ
65 efival ⊢ ( ( ( 2 / 3 ) · π ) ∈ ℂ → ( exp ‘ ( i · ( ( 2 / 3 ) · π ) ) ) = ( ( cos ‘ ( ( 2 / 3 ) · π ) ) + ( i · ( sin ‘ ( ( 2 / 3 ) · π ) ) ) ) )
66 64 65 ax-mp ⊢ ( exp ‘ ( i · ( ( 2 / 3 ) · π ) ) ) = ( ( cos ‘ ( ( 2 / 3 ) · π ) ) + ( i · ( sin ‘ ( ( 2 / 3 ) · π ) ) ) )
67 12 60 mulcli ⊢ ( i · ( √ ‘ 3 ) ) ∈ ℂ
68 1 67 24 25 divdiri ⊢ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) = ( ( - 1 / 2 ) + ( ( i · ( √ ‘ 3 ) ) / 2 ) )
69 63 66 68 3eqtr4i ⊢ ( exp ‘ ( i · ( ( 2 / 3 ) · π ) ) ) = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 )
70 9 17 69 3eqtri ⊢ ( - 1 ↑𝑐 ( 2 / 3 ) ) = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 )
71 1z ⊢ 1 ∈ ℤ
72 root1cj ⊢ ( ( 3 ∈ ℕ ∧ 1 ∈ ℤ ) → ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) ) = ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ ( 3 − 1 ) ) )
73 4 71 72 mp2an ⊢ ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) ) = ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ ( 3 − 1 ) )
74 cxpcl ⊢ ( ( - 1 ∈ ℂ ∧ ( 2 / 3 ) ∈ ℂ ) → ( - 1 ↑𝑐 ( 2 / 3 ) ) ∈ ℂ )
75 1 7 74 mp2an ⊢ ( - 1 ↑𝑐 ( 2 / 3 ) ) ∈ ℂ
76 exp1 ⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ∈ ℂ → ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) = ( - 1 ↑𝑐 ( 2 / 3 ) ) )
77 75 76 ax-mp ⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) = ( - 1 ↑𝑐 ( 2 / 3 ) )
78 77 70 eqtri ⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 )
79 78 fveq2i ⊢ ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) ) = ( ∗ ‘ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) )
80 1 67 addcli ⊢ ( - 1 + ( i · ( √ ‘ 3 ) ) ) ∈ ℂ
81 80 24 cjdivi ⊢ ( 2 ≠ 0 → ( ∗ ‘ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ) = ( ( ∗ ‘ ( - 1 + ( i · ( √ ‘ 3 ) ) ) ) / ( ∗ ‘ 2 ) ) )
82 25 81 ax-mp ⊢ ( ∗ ‘ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ) = ( ( ∗ ‘ ( - 1 + ( i · ( √ ‘ 3 ) ) ) ) / ( ∗ ‘ 2 ) )
83 1 67 cjaddi ⊢ ( ∗ ‘ ( - 1 + ( i · ( √ ‘ 3 ) ) ) ) = ( ( ∗ ‘ - 1 ) + ( ∗ ‘ ( i · ( √ ‘ 3 ) ) ) )
84 neg1rr ⊢ - 1 ∈ ℝ
85 cjre ⊢ ( - 1 ∈ ℝ → ( ∗ ‘ - 1 ) = - 1 )
86 84 85 ax-mp ⊢ ( ∗ ‘ - 1 ) = - 1
87 12 60 cjmuli ⊢ ( ∗ ‘ ( i · ( √ ‘ 3 ) ) ) = ( ( ∗ ‘ i ) · ( ∗ ‘ ( √ ‘ 3 ) ) )
88 cji ⊢ ( ∗ ‘ i ) = - i
89 cjre ⊢ ( ( √ ‘ 3 ) ∈ ℝ → ( ∗ ‘ ( √ ‘ 3 ) ) = ( √ ‘ 3 ) )
90 59 89 ax-mp ⊢ ( ∗ ‘ ( √ ‘ 3 ) ) = ( √ ‘ 3 )
91 88 90 oveq12i ⊢ ( ( ∗ ‘ i ) · ( ∗ ‘ ( √ ‘ 3 ) ) ) = ( - i · ( √ ‘ 3 ) )
92 12 60 mulneg1i ⊢ ( - i · ( √ ‘ 3 ) ) = - ( i · ( √ ‘ 3 ) )
93 87 91 92 3eqtri ⊢ ( ∗ ‘ ( i · ( √ ‘ 3 ) ) ) = - ( i · ( √ ‘ 3 ) )
94 86 93 oveq12i ⊢ ( ( ∗ ‘ - 1 ) + ( ∗ ‘ ( i · ( √ ‘ 3 ) ) ) ) = ( - 1 + - ( i · ( √ ‘ 3 ) ) )
95 1 67 negsubi ⊢ ( - 1 + - ( i · ( √ ‘ 3 ) ) ) = ( - 1 − ( i · ( √ ‘ 3 ) ) )
96 83 94 95 3eqtri ⊢ ( ∗ ‘ ( - 1 + ( i · ( √ ‘ 3 ) ) ) ) = ( - 1 − ( i · ( √ ‘ 3 ) ) )
97 cjre ⊢ ( 2 ∈ ℝ → ( ∗ ‘ 2 ) = 2 )
98 3 97 ax-mp ⊢ ( ∗ ‘ 2 ) = 2
99 96 98 oveq12i ⊢ ( ( ∗ ‘ ( - 1 + ( i · ( √ ‘ 3 ) ) ) ) / ( ∗ ‘ 2 ) ) = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 )
100 79 82 99 3eqtri ⊢ ( ∗ ‘ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 1 ) ) = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 )
101 3m1e2 ⊢ ( 3 − 1 ) = 2
102 101 oveq2i ⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ ( 3 − 1 ) ) = ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 2 )
103 73 100 102 3eqtr3ri ⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 2 ) = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 )
104 70 103 pm3.2i ⊢ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ∧ ( ( - 1 ↑𝑐 ( 2 / 3 ) ) ↑ 2 ) = ( ( - 1 − ( i · ( √ ‘ 3 ) ) ) / 2 ) )