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 ⊢ 𝑊 = ( bRoU ‘ 3 )
Assertion bru3eq ( ( ( 𝑊 ↑ 2 ) + 𝑊 ) + 1 ) = 0

Proof

Step Hyp Ref Expression
1 bru3eq.w ⊢ 𝑊 = ( bRoU ‘ 3 )
2 1 bru3sq ⊢ ( 𝑊 ↑ 2 ) = ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) )
3 1 bru3val ⊢ 𝑊 = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 )
4 2 3 oveq12i ⊢ ( ( 𝑊 ↑ 2 ) + 𝑊 ) = ( ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) ) + ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) )
5 4 oveq1i ⊢ ( ( ( 𝑊 ↑ 2 ) + 𝑊 ) + 1 ) = ( ( ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) ) + ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ) + 1 )
6 ax-1cn ⊢ 1 ∈ ℂ
7 2cn ⊢ 2 ∈ ℂ
8 2ne0 ⊢ 2 ≠ 0
9 divneg ⊢ ( ( 1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( 1 / 2 ) = ( - 1 / 2 ) )
10 6 7 8 9 mp3an ⊢ - ( 1 / 2 ) = ( - 1 / 2 )
11 10 oveq2i ⊢ ( 2 · - ( 1 / 2 ) ) = ( 2 · ( - 1 / 2 ) )
12 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
13 7 12 mulneg2i ⊢ ( 2 · - ( 1 / 2 ) ) = - ( 2 · ( 1 / 2 ) )
14 2thalfe1 ⊢ ( 2 · ( 1 / 2 ) ) = 1
15 14 negeqi ⊢ - ( 2 · ( 1 / 2 ) ) = - 1
16 13 15 eqtri ⊢ ( 2 · - ( 1 / 2 ) ) = - 1
17 neg1cn ⊢ - 1 ∈ ℂ
18 17 7 8 divcli ⊢ ( - 1 / 2 ) ∈ ℂ
19 18 2timesi ⊢ ( 2 · ( - 1 / 2 ) ) = ( ( - 1 / 2 ) + ( - 1 / 2 ) )
20 11 16 19 3eqtr3ri ⊢ ( ( - 1 / 2 ) + ( - 1 / 2 ) ) = - 1
21 20 oveq1i ⊢ ( ( ( - 1 / 2 ) + ( - 1 / 2 ) ) + 1 ) = ( - 1 + 1 )
22 ax-icn ⊢ i ∈ ℂ
23 3re ⊢ 3 ∈ ℝ
24 3pos ⊢ 0 < 3
25 23 24 sqrtpclii ⊢ ( √ ‘ 3 ) ∈ ℝ
26 25 recni ⊢ ( √ ‘ 3 ) ∈ ℂ
27 22 26 mulcli ⊢ ( i · ( √ ‘ 3 ) ) ∈ ℂ
28 17 27 7 8 divdiri ⊢ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) = ( ( - 1 / 2 ) + ( ( i · ( √ ‘ 3 ) ) / 2 ) )
29 22 26 7 8 divassi ⊢ ( ( i · ( √ ‘ 3 ) ) / 2 ) = ( i · ( ( √ ‘ 3 ) / 2 ) )
30 29 oveq2i ⊢ ( ( - 1 / 2 ) + ( ( i · ( √ ‘ 3 ) ) / 2 ) ) = ( ( - 1 / 2 ) + ( i · ( ( √ ‘ 3 ) / 2 ) ) )
31 28 30 eqtri ⊢ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) = ( ( - 1 / 2 ) + ( i · ( ( √ ‘ 3 ) / 2 ) ) )
32 31 oveq2i ⊢ ( ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) ) + ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ) = ( ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) ) + ( ( - 1 / 2 ) + ( i · ( ( √ ‘ 3 ) / 2 ) ) ) )
33 26 7 8 divcli ⊢ ( ( √ ‘ 3 ) / 2 ) ∈ ℂ
34 22 33 mulcli ⊢ ( i · ( ( √ ‘ 3 ) / 2 ) ) ∈ ℂ
35 nppcan3 ⊢ ( ( ( - 1 / 2 ) ∈ ℂ ∧ ( i · ( ( √ ‘ 3 ) / 2 ) ) ∈ ℂ ∧ ( - 1 / 2 ) ∈ ℂ ) → ( ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) ) + ( ( - 1 / 2 ) + ( i · ( ( √ ‘ 3 ) / 2 ) ) ) ) = ( ( - 1 / 2 ) + ( - 1 / 2 ) ) )
36 18 34 18 35 mp3an ⊢ ( ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) ) + ( ( - 1 / 2 ) + ( i · ( ( √ ‘ 3 ) / 2 ) ) ) ) = ( ( - 1 / 2 ) + ( - 1 / 2 ) )
37 32 36 eqtri ⊢ ( ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) ) + ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ) = ( ( - 1 / 2 ) + ( - 1 / 2 ) )
38 37 oveq1i ⊢ ( ( ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) ) + ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ) + 1 ) = ( ( ( - 1 / 2 ) + ( - 1 / 2 ) ) + 1 )
39 6 6 negsubdii ⊢ - ( 1 − 1 ) = ( - 1 + 1 )
40 21 38 39 3eqtr4i ⊢ ( ( ( ( - 1 / 2 ) − ( i · ( ( √ ‘ 3 ) / 2 ) ) ) + ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) ) + 1 ) = - ( 1 − 1 )
41 1m1e0 ⊢ ( 1 − 1 ) = 0
42 41 negeqi ⊢ - ( 1 − 1 ) = - 0
43 neg0 ⊢ - 0 = 0
44 42 43 eqtri ⊢ - ( 1 − 1 ) = 0
45 5 40 44 3eqtri ⊢ ( ( ( 𝑊 ↑ 2 ) + 𝑊 ) + 1 ) = 0