Metamath Proof Explorer

Theorem 1cubrlem

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

Ref Expression
Assertion 1cubrlem 
|- ( ( -u 1 ^c ( 2 / 3 ) ) = ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) /\ ( ( -u 1 ^c ( 2 / 3 ) ) ^ 2 ) = ( ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 neg1cn 
 |-  -u 1 e. CC
2 neg1ne0 
 |-  -u 1 =/= 0
3 2re 
 |-  2 e. RR
4 3nn 
 |-  3 e. NN
5 nndivre 
 |-  ( ( 2 e. RR /\ 3 e. NN ) -> ( 2 / 3 ) e. RR )
6 3 4 5 mp2an 
 |-  ( 2 / 3 ) e. RR
7 6 recni 
 |-  ( 2 / 3 ) e. CC
8 cxpef 
 |-  ( ( -u 1 e. CC /\ -u 1 =/= 0 /\ ( 2 / 3 ) e. CC ) -> ( -u 1 ^c ( 2 / 3 ) ) = ( exp ` ( ( 2 / 3 ) x. ( log ` -u 1 ) ) ) )
9 1 2 7 8 mp3an 
 |-  ( -u 1 ^c ( 2 / 3 ) ) = ( exp ` ( ( 2 / 3 ) x. ( log ` -u 1 ) ) )
10 logm1 
 |-  ( log ` -u 1 ) = ( _i x. _pi )
11 10 oveq2i 
 |-  ( ( 2 / 3 ) x. ( log ` -u 1 ) ) = ( ( 2 / 3 ) x. ( _i x. _pi ) )
12 ax-icn 
 |-  _i e. CC
13 pire 
 |-  _pi e. RR
14 13 recni 
 |-  _pi e. CC
15 7 12 14 mul12i 
 |-  ( ( 2 / 3 ) x. ( _i x. _pi ) ) = ( _i x. ( ( 2 / 3 ) x. _pi ) )
16 11 15 eqtri 
 |-  ( ( 2 / 3 ) x. ( log ` -u 1 ) ) = ( _i x. ( ( 2 / 3 ) x. _pi ) )
17 16 fveq2i 
 |-  ( exp ` ( ( 2 / 3 ) x. ( log ` -u 1 ) ) ) = ( exp ` ( _i x. ( ( 2 / 3 ) x. _pi ) ) )
18 6nn 
 |-  6 e. NN
19 nndivre 
 |-  ( ( _pi e. RR /\ 6 e. NN ) -> ( _pi / 6 ) e. RR )
20 13 18 19 mp2an 
 |-  ( _pi / 6 ) e. RR
21 20 recni 
 |-  ( _pi / 6 ) e. CC
22 coshalfpip 
 |-  ( ( _pi / 6 ) e. CC -> ( cos ` ( ( _pi / 2 ) + ( _pi / 6 ) ) ) = -u ( sin ` ( _pi / 6 ) ) )
23 21 22 ax-mp 
 |-  ( cos ` ( ( _pi / 2 ) + ( _pi / 6 ) ) ) = -u ( sin ` ( _pi / 6 ) )
24 2cn 
 |-  2 e. CC
25 2ne0 
 |-  2 =/= 0
26 divrec2 
 |-  ( ( _pi e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( _pi / 2 ) = ( ( 1 / 2 ) x. _pi ) )
27 14 24 25 26 mp3an 
 |-  ( _pi / 2 ) = ( ( 1 / 2 ) x. _pi )
28 6cn 
 |-  6 e. CC
29 18 nnne0i 
 |-  6 =/= 0
30 divrec2 
 |-  ( ( _pi e. CC /\ 6 e. CC /\ 6 =/= 0 ) -> ( _pi / 6 ) = ( ( 1 / 6 ) x. _pi ) )
31 14 28 29 30 mp3an 
 |-  ( _pi / 6 ) = ( ( 1 / 6 ) x. _pi )
32 27 31 oveq12i 
 |-  ( ( _pi / 2 ) + ( _pi / 6 ) ) = ( ( ( 1 / 2 ) x. _pi ) + ( ( 1 / 6 ) x. _pi ) )
33 24 25 reccli 
 |-  ( 1 / 2 ) e. CC
34 28 29 reccli 
 |-  ( 1 / 6 ) e. CC
35 33 34 14 adddiri 
 |-  ( ( ( 1 / 2 ) + ( 1 / 6 ) ) x. _pi ) = ( ( ( 1 / 2 ) x. _pi ) + ( ( 1 / 6 ) x. _pi ) )
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 ) ) x. _pi ) = ( ( 2 / 3 ) x. _pi )
39 32 35 38 3eqtr2i 
 |-  ( ( _pi / 2 ) + ( _pi / 6 ) ) = ( ( 2 / 3 ) x. _pi )
40 39 fveq2i 
 |-  ( cos ` ( ( _pi / 2 ) + ( _pi / 6 ) ) ) = ( cos ` ( ( 2 / 3 ) x. _pi ) )
41 sincos6thpi 
 |-  ( ( sin ` ( _pi / 6 ) ) = ( 1 / 2 ) /\ ( cos ` ( _pi / 6 ) ) = ( ( sqrt ` 3 ) / 2 ) )
42 41 simpli 
 |-  ( sin ` ( _pi / 6 ) ) = ( 1 / 2 )
43 42 negeqi 
 |-  -u ( sin ` ( _pi / 6 ) ) = -u ( 1 / 2 )
44 ax-1cn 
 |-  1 e. CC
45 divneg 
 |-  ( ( 1 e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( 1 / 2 ) = ( -u 1 / 2 ) )
46 44 24 25 45 mp3an 
 |-  -u ( 1 / 2 ) = ( -u 1 / 2 )
47 43 46 eqtri 
 |-  -u ( sin ` ( _pi / 6 ) ) = ( -u 1 / 2 )
48 23 40 47 3eqtr3i 
 |-  ( cos ` ( ( 2 / 3 ) x. _pi ) ) = ( -u 1 / 2 )
49 sinhalfpip 
 |-  ( ( _pi / 6 ) e. CC -> ( sin ` ( ( _pi / 2 ) + ( _pi / 6 ) ) ) = ( cos ` ( _pi / 6 ) ) )
50 21 49 ax-mp 
 |-  ( sin ` ( ( _pi / 2 ) + ( _pi / 6 ) ) ) = ( cos ` ( _pi / 6 ) )
51 39 fveq2i 
 |-  ( sin ` ( ( _pi / 2 ) + ( _pi / 6 ) ) ) = ( sin ` ( ( 2 / 3 ) x. _pi ) )
52 41 simpri 
 |-  ( cos ` ( _pi / 6 ) ) = ( ( sqrt ` 3 ) / 2 )
53 50 51 52 3eqtr3i 
 |-  ( sin ` ( ( 2 / 3 ) x. _pi ) ) = ( ( sqrt ` 3 ) / 2 )
54 53 oveq2i 
 |-  ( _i x. ( sin ` ( ( 2 / 3 ) x. _pi ) ) ) = ( _i x. ( ( sqrt ` 3 ) / 2 ) )
55 3re 
 |-  3 e. RR
56 3nn0 
 |-  3 e. NN0
57 56 nn0ge0i 
 |-  0 <_ 3
58 resqrtcl 
 |-  ( ( 3 e. RR /\ 0 <_ 3 ) -> ( sqrt ` 3 ) e. RR )
59 55 57 58 mp2an 
 |-  ( sqrt ` 3 ) e. RR
60 59 recni 
 |-  ( sqrt ` 3 ) e. CC
61 12 60 24 25 divassi 
 |-  ( ( _i x. ( sqrt ` 3 ) ) / 2 ) = ( _i x. ( ( sqrt ` 3 ) / 2 ) )
62 54 61 eqtr4i 
 |-  ( _i x. ( sin ` ( ( 2 / 3 ) x. _pi ) ) ) = ( ( _i x. ( sqrt ` 3 ) ) / 2 )
63 48 62 oveq12i 
 |-  ( ( cos ` ( ( 2 / 3 ) x. _pi ) ) + ( _i x. ( sin ` ( ( 2 / 3 ) x. _pi ) ) ) ) = ( ( -u 1 / 2 ) + ( ( _i x. ( sqrt ` 3 ) ) / 2 ) )
64 7 14 mulcli 
 |-  ( ( 2 / 3 ) x. _pi ) e. CC
65 efival 
 |-  ( ( ( 2 / 3 ) x. _pi ) e. CC -> ( exp ` ( _i x. ( ( 2 / 3 ) x. _pi ) ) ) = ( ( cos ` ( ( 2 / 3 ) x. _pi ) ) + ( _i x. ( sin ` ( ( 2 / 3 ) x. _pi ) ) ) ) )
66 64 65 ax-mp 
 |-  ( exp ` ( _i x. ( ( 2 / 3 ) x. _pi ) ) ) = ( ( cos ` ( ( 2 / 3 ) x. _pi ) ) + ( _i x. ( sin ` ( ( 2 / 3 ) x. _pi ) ) ) )
67 12 60 mulcli 
 |-  ( _i x. ( sqrt ` 3 ) ) e. CC
68 1 67 24 25 divdiri 
 |-  ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) = ( ( -u 1 / 2 ) + ( ( _i x. ( sqrt ` 3 ) ) / 2 ) )
69 63 66 68 3eqtr4i 
 |-  ( exp ` ( _i x. ( ( 2 / 3 ) x. _pi ) ) ) = ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 )
70 9 17 69 3eqtri 
 |-  ( -u 1 ^c ( 2 / 3 ) ) = ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 )
71 1z 
 |-  1 e. ZZ
72 root1cj 
 |-  ( ( 3 e. NN /\ 1 e. ZZ ) -> ( * ` ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 ) ) = ( ( -u 1 ^c ( 2 / 3 ) ) ^ ( 3 - 1 ) ) )
73 4 71 72 mp2an 
 |-  ( * ` ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 ) ) = ( ( -u 1 ^c ( 2 / 3 ) ) ^ ( 3 - 1 ) )
74 cxpcl 
 |-  ( ( -u 1 e. CC /\ ( 2 / 3 ) e. CC ) -> ( -u 1 ^c ( 2 / 3 ) ) e. CC )
75 1 7 74 mp2an 
 |-  ( -u 1 ^c ( 2 / 3 ) ) e. CC
76 exp1 
 |-  ( ( -u 1 ^c ( 2 / 3 ) ) e. CC -> ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 ) = ( -u 1 ^c ( 2 / 3 ) ) )
77 75 76 ax-mp 
 |-  ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 ) = ( -u 1 ^c ( 2 / 3 ) )
78 77 70 eqtri 
 |-  ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 ) = ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 )
79 78 fveq2i 
 |-  ( * ` ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 ) ) = ( * ` ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) )
80 1 67 addcli 
 |-  ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) e. CC
81 80 24 cjdivi 
 |-  ( 2 =/= 0 -> ( * ` ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) ) = ( ( * ` ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) ) / ( * ` 2 ) ) )
82 25 81 ax-mp 
 |-  ( * ` ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) ) = ( ( * ` ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) ) / ( * ` 2 ) )
83 1 67 cjaddi 
 |-  ( * ` ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) ) = ( ( * ` -u 1 ) + ( * ` ( _i x. ( sqrt ` 3 ) ) ) )
84 neg1rr 
 |-  -u 1 e. RR
85 cjre 
 |-  ( -u 1 e. RR -> ( * ` -u 1 ) = -u 1 )
86 84 85 ax-mp 
 |-  ( * ` -u 1 ) = -u 1
87 12 60 cjmuli 
 |-  ( * ` ( _i x. ( sqrt ` 3 ) ) ) = ( ( * ` _i ) x. ( * ` ( sqrt ` 3 ) ) )
88 cji 
 |-  ( * ` _i ) = -u _i
89 cjre 
 |-  ( ( sqrt ` 3 ) e. RR -> ( * ` ( sqrt ` 3 ) ) = ( sqrt ` 3 ) )
90 59 89 ax-mp 
 |-  ( * ` ( sqrt ` 3 ) ) = ( sqrt ` 3 )
91 88 90 oveq12i 
 |-  ( ( * ` _i ) x. ( * ` ( sqrt ` 3 ) ) ) = ( -u _i x. ( sqrt ` 3 ) )
92 12 60 mulneg1i 
 |-  ( -u _i x. ( sqrt ` 3 ) ) = -u ( _i x. ( sqrt ` 3 ) )
93 87 91 92 3eqtri 
 |-  ( * ` ( _i x. ( sqrt ` 3 ) ) ) = -u ( _i x. ( sqrt ` 3 ) )
94 86 93 oveq12i 
 |-  ( ( * ` -u 1 ) + ( * ` ( _i x. ( sqrt ` 3 ) ) ) ) = ( -u 1 + -u ( _i x. ( sqrt ` 3 ) ) )
95 1 67 negsubi 
 |-  ( -u 1 + -u ( _i x. ( sqrt ` 3 ) ) ) = ( -u 1 - ( _i x. ( sqrt ` 3 ) ) )
96 83 94 95 3eqtri 
 |-  ( * ` ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) ) = ( -u 1 - ( _i x. ( sqrt ` 3 ) ) )
97 cjre 
 |-  ( 2 e. RR -> ( * ` 2 ) = 2 )
98 3 97 ax-mp 
 |-  ( * ` 2 ) = 2
99 96 98 oveq12i 
 |-  ( ( * ` ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) ) / ( * ` 2 ) ) = ( ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) / 2 )
100 79 82 99 3eqtri 
 |-  ( * ` ( ( -u 1 ^c ( 2 / 3 ) ) ^ 1 ) ) = ( ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) / 2 )
101 3m1e2 
 |-  ( 3 - 1 ) = 2
102 101 oveq2i 
 |-  ( ( -u 1 ^c ( 2 / 3 ) ) ^ ( 3 - 1 ) ) = ( ( -u 1 ^c ( 2 / 3 ) ) ^ 2 )
103 73 100 102 3eqtr3ri 
 |-  ( ( -u 1 ^c ( 2 / 3 ) ) ^ 2 ) = ( ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) / 2 )
104 70 103 pm3.2i 
 |-  ( ( -u 1 ^c ( 2 / 3 ) ) = ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) /\ ( ( -u 1 ^c ( 2 / 3 ) ) ^ 2 ) = ( ( -u 1 - ( _i x. ( sqrt ` 3 ) ) ) / 2 ) )