Metamath Proof Explorer

Theorem bru3val

Description: An alternate way to express the basic 3rd root of unity. (Contributed by AV, 24-Oct-2026)

Ref Expression
Hypothesis bru3eq.w 
|- W = ( bRoU ` 3 )
Assertion bru3val 
|- W = ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 )

Proof

Step Hyp Ref Expression
1 bru3eq.w 
 |-  W = ( bRoU ` 3 )
2 3nn 
 |-  3 e. NN
3 bruval3 
 |-  ( 3 e. NN -> ( bRoU ` 3 ) = ( ( cos ` ( ( 2 x. _pi ) / 3 ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / 3 ) ) ) ) )
4 2 3 ax-mp 
 |-  ( bRoU ` 3 ) = ( ( cos ` ( ( 2 x. _pi ) / 3 ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / 3 ) ) ) )
5 ax-icn 
 |-  _i e. CC
6 3re 
 |-  3 e. RR
7 3pos 
 |-  0 < 3
8 6 7 sqrtpclii 
 |-  ( sqrt ` 3 ) e. RR
9 8 recni 
 |-  ( sqrt ` 3 ) e. CC
10 2cn 
 |-  2 e. CC
11 2ne0 
 |-  2 =/= 0
12 5 9 10 11 divassi 
 |-  ( ( _i x. ( sqrt ` 3 ) ) / 2 ) = ( _i x. ( ( sqrt ` 3 ) / 2 ) )
13 12 oveq2i 
 |-  ( ( -u 1 / 2 ) + ( ( _i x. ( sqrt ` 3 ) ) / 2 ) ) = ( ( -u 1 / 2 ) + ( _i x. ( ( sqrt ` 3 ) / 2 ) ) )
14 neg1cn 
 |-  -u 1 e. CC
15 5 9 mulcli 
 |-  ( _i x. ( sqrt ` 3 ) ) e. CC
16 14 15 10 11 divdiri 
 |-  ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) = ( ( -u 1 / 2 ) + ( ( _i x. ( sqrt ` 3 ) ) / 2 ) )
17 picn 
 |-  _pi e. CC
18 3cn 
 |-  3 e. CC
19 3ne0 
 |-  3 =/= 0
20 10 17 18 19 divassi 
 |-  ( ( 2 x. _pi ) / 3 ) = ( 2 x. ( _pi / 3 ) )
21 20 fveq2i 
 |-  ( cos ` ( ( 2 x. _pi ) / 3 ) ) = ( cos ` ( 2 x. ( _pi / 3 ) ) )
22 17 18 19 divcli 
 |-  ( _pi / 3 ) e. CC
23 cos2t 
 |-  ( ( _pi / 3 ) e. CC -> ( cos ` ( 2 x. ( _pi / 3 ) ) ) = ( ( 2 x. ( ( cos ` ( _pi / 3 ) ) ^ 2 ) ) - 1 ) )
24 22 23 ax-mp 
 |-  ( cos ` ( 2 x. ( _pi / 3 ) ) ) = ( ( 2 x. ( ( cos ` ( _pi / 3 ) ) ^ 2 ) ) - 1 )
25 sincos3rdpi 
 |-  ( ( sin ` ( _pi / 3 ) ) = ( ( sqrt ` 3 ) / 2 ) /\ ( cos ` ( _pi / 3 ) ) = ( 1 / 2 ) )
26 25 simpri 
 |-  ( cos ` ( _pi / 3 ) ) = ( 1 / 2 )
27 26 oveq1i 
 |-  ( ( cos ` ( _pi / 3 ) ) ^ 2 ) = ( ( 1 / 2 ) ^ 2 )
28 10 11 sqrecii 
 |-  ( ( 1 / 2 ) ^ 2 ) = ( 1 / ( 2 ^ 2 ) )
29 27 28 eqtri 
 |-  ( ( cos ` ( _pi / 3 ) ) ^ 2 ) = ( 1 / ( 2 ^ 2 ) )
30 29 oveq2i 
 |-  ( 2 x. ( ( cos ` ( _pi / 3 ) ) ^ 2 ) ) = ( 2 x. ( 1 / ( 2 ^ 2 ) ) )
31 30 oveq1i 
 |-  ( ( 2 x. ( ( cos ` ( _pi / 3 ) ) ^ 2 ) ) - 1 ) = ( ( 2 x. ( 1 / ( 2 ^ 2 ) ) ) - 1 )
32 24 31 eqtri 
 |-  ( cos ` ( 2 x. ( _pi / 3 ) ) ) = ( ( 2 x. ( 1 / ( 2 ^ 2 ) ) ) - 1 )
33 10 sqvali 
 |-  ( 2 ^ 2 ) = ( 2 x. 2 )
34 33 oveq2i 
 |-  ( 1 / ( 2 ^ 2 ) ) = ( 1 / ( 2 x. 2 ) )
35 34 oveq2i 
 |-  ( 2 x. ( 1 / ( 2 ^ 2 ) ) ) = ( 2 x. ( 1 / ( 2 x. 2 ) ) )
36 ax-1cn 
 |-  1 e. CC
37 10 10 mulcli 
 |-  ( 2 x. 2 ) e. CC
38 2t2e4 
 |-  ( 2 x. 2 ) = 4
39 4ne0 
 |-  4 =/= 0
40 38 39 eqnetri 
 |-  ( 2 x. 2 ) =/= 0
41 10 36 37 40 divassi 
 |-  ( ( 2 x. 1 ) / ( 2 x. 2 ) ) = ( 2 x. ( 1 / ( 2 x. 2 ) ) )
42 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
43 divcan5 
 |-  ( ( 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 2 x. 1 ) / ( 2 x. 2 ) ) = ( 1 / 2 ) )
44 36 42 42 43 mp3an 
 |-  ( ( 2 x. 1 ) / ( 2 x. 2 ) ) = ( 1 / 2 )
45 41 44 eqtr3i 
 |-  ( 2 x. ( 1 / ( 2 x. 2 ) ) ) = ( 1 / 2 )
46 35 45 eqtri 
 |-  ( 2 x. ( 1 / ( 2 ^ 2 ) ) ) = ( 1 / 2 )
47 46 oveq1i 
 |-  ( ( 2 x. ( 1 / ( 2 ^ 2 ) ) ) - 1 ) = ( ( 1 / 2 ) - 1 )
48 2div2e1 
 |-  ( 2 / 2 ) = 1
49 48 eqcomi 
 |-  1 = ( 2 / 2 )
50 49 oveq2i 
 |-  ( ( 1 / 2 ) - 1 ) = ( ( 1 / 2 ) - ( 2 / 2 ) )
51 divsubdir 
 |-  ( ( 1 e. CC /\ 2 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 1 - 2 ) / 2 ) = ( ( 1 / 2 ) - ( 2 / 2 ) ) )
52 36 10 42 51 mp3an 
 |-  ( ( 1 - 2 ) / 2 ) = ( ( 1 / 2 ) - ( 2 / 2 ) )
53 50 52 eqtr4i 
 |-  ( ( 1 / 2 ) - 1 ) = ( ( 1 - 2 ) / 2 )
54 10 36 negsubdi2i 
 |-  -u ( 2 - 1 ) = ( 1 - 2 )
55 2m1e1 
 |-  ( 2 - 1 ) = 1
56 55 negeqi 
 |-  -u ( 2 - 1 ) = -u 1
57 54 56 eqtr3i 
 |-  ( 1 - 2 ) = -u 1
58 57 oveq1i 
 |-  ( ( 1 - 2 ) / 2 ) = ( -u 1 / 2 )
59 47 53 58 3eqtri 
 |-  ( ( 2 x. ( 1 / ( 2 ^ 2 ) ) ) - 1 ) = ( -u 1 / 2 )
60 21 32 59 3eqtri 
 |-  ( cos ` ( ( 2 x. _pi ) / 3 ) ) = ( -u 1 / 2 )
61 20 fveq2i 
 |-  ( sin ` ( ( 2 x. _pi ) / 3 ) ) = ( sin ` ( 2 x. ( _pi / 3 ) ) )
62 sin2t 
 |-  ( ( _pi / 3 ) e. CC -> ( sin ` ( 2 x. ( _pi / 3 ) ) ) = ( 2 x. ( ( sin ` ( _pi / 3 ) ) x. ( cos ` ( _pi / 3 ) ) ) ) )
63 22 62 ax-mp 
 |-  ( sin ` ( 2 x. ( _pi / 3 ) ) ) = ( 2 x. ( ( sin ` ( _pi / 3 ) ) x. ( cos ` ( _pi / 3 ) ) ) )
64 oveq12 
 |-  ( ( ( sin ` ( _pi / 3 ) ) = ( ( sqrt ` 3 ) / 2 ) /\ ( cos ` ( _pi / 3 ) ) = ( 1 / 2 ) ) -> ( ( sin ` ( _pi / 3 ) ) x. ( cos ` ( _pi / 3 ) ) ) = ( ( ( sqrt ` 3 ) / 2 ) x. ( 1 / 2 ) ) )
65 25 64 ax-mp 
 |-  ( ( sin ` ( _pi / 3 ) ) x. ( cos ` ( _pi / 3 ) ) ) = ( ( ( sqrt ` 3 ) / 2 ) x. ( 1 / 2 ) )
66 65 oveq2i 
 |-  ( 2 x. ( ( sin ` ( _pi / 3 ) ) x. ( cos ` ( _pi / 3 ) ) ) ) = ( 2 x. ( ( ( sqrt ` 3 ) / 2 ) x. ( 1 / 2 ) ) )
67 9 10 11 divcli 
 |-  ( ( sqrt ` 3 ) / 2 ) e. CC
68 67 10 11 divreci 
 |-  ( ( ( sqrt ` 3 ) / 2 ) / 2 ) = ( ( ( sqrt ` 3 ) / 2 ) x. ( 1 / 2 ) )
69 68 eqcomi 
 |-  ( ( ( sqrt ` 3 ) / 2 ) x. ( 1 / 2 ) ) = ( ( ( sqrt ` 3 ) / 2 ) / 2 )
70 69 oveq2i 
 |-  ( 2 x. ( ( ( sqrt ` 3 ) / 2 ) x. ( 1 / 2 ) ) ) = ( 2 x. ( ( ( sqrt ` 3 ) / 2 ) / 2 ) )
71 67 10 11 divcan2i 
 |-  ( 2 x. ( ( ( sqrt ` 3 ) / 2 ) / 2 ) ) = ( ( sqrt ` 3 ) / 2 )
72 66 70 71 3eqtri 
 |-  ( 2 x. ( ( sin ` ( _pi / 3 ) ) x. ( cos ` ( _pi / 3 ) ) ) ) = ( ( sqrt ` 3 ) / 2 )
73 61 63 72 3eqtri 
 |-  ( sin ` ( ( 2 x. _pi ) / 3 ) ) = ( ( sqrt ` 3 ) / 2 )
74 73 oveq2i 
 |-  ( _i x. ( sin ` ( ( 2 x. _pi ) / 3 ) ) ) = ( _i x. ( ( sqrt ` 3 ) / 2 ) )
75 60 74 oveq12i 
 |-  ( ( cos ` ( ( 2 x. _pi ) / 3 ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / 3 ) ) ) ) = ( ( -u 1 / 2 ) + ( _i x. ( ( sqrt ` 3 ) / 2 ) ) )
76 13 16 75 3eqtr4ri 
 |-  ( ( cos ` ( ( 2 x. _pi ) / 3 ) ) + ( _i x. ( sin ` ( ( 2 x. _pi ) / 3 ) ) ) ) = ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 )
77 1 4 76 3eqtri 
 |-  W = ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 )