Metamath Proof Explorer

Theorem bru3eq

Description: The basic 3rd root of unity _om satisfies the equation _om ^ 2 + _om + 1 = 0 . (Contributed by AV, 24-Oct-2026)

Ref Expression
Hypothesis bru3eq.w 
|- W = ( bRoU ` 3 )
Assertion bru3eq 
|- ( ( ( W ^ 2 ) + W ) + 1 ) = 0

Proof

Step Hyp Ref Expression
1 bru3eq.w 
 |-  W = ( bRoU ` 3 )
2 1 bru3sq 
 |-  ( W ^ 2 ) = ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) )
3 1 bru3val 
 |-  W = ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 )
4 2 3 oveq12i 
 |-  ( ( W ^ 2 ) + W ) = ( ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) + ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) )
5 4 oveq1i 
 |-  ( ( ( W ^ 2 ) + W ) + 1 ) = ( ( ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) + ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) ) + 1 )
6 ax-1cn 
 |-  1 e. CC
7 2cn 
 |-  2 e. CC
8 2ne0 
 |-  2 =/= 0
9 divneg 
 |-  ( ( 1 e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( 1 / 2 ) = ( -u 1 / 2 ) )
10 6 7 8 9 mp3an 
 |-  -u ( 1 / 2 ) = ( -u 1 / 2 )
11 10 oveq2i 
 |-  ( 2 x. -u ( 1 / 2 ) ) = ( 2 x. ( -u 1 / 2 ) )
12 halfcn 
 |-  ( 1 / 2 ) e. CC
13 7 12 mulneg2i 
 |-  ( 2 x. -u ( 1 / 2 ) ) = -u ( 2 x. ( 1 / 2 ) )
14 2thalfe1 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
15 14 negeqi 
 |-  -u ( 2 x. ( 1 / 2 ) ) = -u 1
16 13 15 eqtri 
 |-  ( 2 x. -u ( 1 / 2 ) ) = -u 1
17 neg1cn 
 |-  -u 1 e. CC
18 17 7 8 divcli 
 |-  ( -u 1 / 2 ) e. CC
19 18 2timesi 
 |-  ( 2 x. ( -u 1 / 2 ) ) = ( ( -u 1 / 2 ) + ( -u 1 / 2 ) )
20 11 16 19 3eqtr3ri 
 |-  ( ( -u 1 / 2 ) + ( -u 1 / 2 ) ) = -u 1
21 20 oveq1i 
 |-  ( ( ( -u 1 / 2 ) + ( -u 1 / 2 ) ) + 1 ) = ( -u 1 + 1 )
22 ax-icn 
 |-  _i e. CC
23 3re 
 |-  3 e. RR
24 3pos 
 |-  0 < 3
25 23 24 sqrtpclii 
 |-  ( sqrt ` 3 ) e. RR
26 25 recni 
 |-  ( sqrt ` 3 ) e. CC
27 22 26 mulcli 
 |-  ( _i x. ( sqrt ` 3 ) ) e. CC
28 17 27 7 8 divdiri 
 |-  ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) = ( ( -u 1 / 2 ) + ( ( _i x. ( sqrt ` 3 ) ) / 2 ) )
29 22 26 7 8 divassi 
 |-  ( ( _i x. ( sqrt ` 3 ) ) / 2 ) = ( _i x. ( ( sqrt ` 3 ) / 2 ) )
30 29 oveq2i 
 |-  ( ( -u 1 / 2 ) + ( ( _i x. ( sqrt ` 3 ) ) / 2 ) ) = ( ( -u 1 / 2 ) + ( _i x. ( ( sqrt ` 3 ) / 2 ) ) )
31 28 30 eqtri 
 |-  ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) = ( ( -u 1 / 2 ) + ( _i x. ( ( sqrt ` 3 ) / 2 ) ) )
32 31 oveq2i 
 |-  ( ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) + ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) ) = ( ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) + ( ( -u 1 / 2 ) + ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) )
33 26 7 8 divcli 
 |-  ( ( sqrt ` 3 ) / 2 ) e. CC
34 22 33 mulcli 
 |-  ( _i x. ( ( sqrt ` 3 ) / 2 ) ) e. CC
35 nppcan3 
 |-  ( ( ( -u 1 / 2 ) e. CC /\ ( _i x. ( ( sqrt ` 3 ) / 2 ) ) e. CC /\ ( -u 1 / 2 ) e. CC ) -> ( ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) + ( ( -u 1 / 2 ) + ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) ) = ( ( -u 1 / 2 ) + ( -u 1 / 2 ) ) )
36 18 34 18 35 mp3an 
 |-  ( ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) + ( ( -u 1 / 2 ) + ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) ) = ( ( -u 1 / 2 ) + ( -u 1 / 2 ) )
37 32 36 eqtri 
 |-  ( ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) + ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) ) = ( ( -u 1 / 2 ) + ( -u 1 / 2 ) )
38 37 oveq1i 
 |-  ( ( ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) + ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) ) + 1 ) = ( ( ( -u 1 / 2 ) + ( -u 1 / 2 ) ) + 1 )
39 6 6 negsubdii 
 |-  -u ( 1 - 1 ) = ( -u 1 + 1 )
40 21 38 39 3eqtr4i 
 |-  ( ( ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) + ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) ) + 1 ) = -u ( 1 - 1 )
41 1m1e0 
 |-  ( 1 - 1 ) = 0
42 41 negeqi 
 |-  -u ( 1 - 1 ) = -u 0
43 neg0 
 |-  -u 0 = 0
44 42 43 eqtri 
 |-  -u ( 1 - 1 ) = 0
45 5 40 44 3eqtri 
 |-  ( ( ( W ^ 2 ) + W ) + 1 ) = 0