Metamath Proof Explorer

Theorem bru3sq

Description: The square of the basic 3rd root of unity. (Contributed by AV, 24-Oct-2026)

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

Proof

Step Hyp Ref Expression
1 bru3eq.w 
 |-  W = ( bRoU ` 3 )
2 1 bru3cj 
 |-  ( * ` W ) = ( W ^ 2 )
3 1 bru3val 
 |-  W = ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 )
4 3 fveq2i 
 |-  ( * ` W ) = ( * ` ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) )
5 neg1cn 
 |-  -u 1 e. CC
6 ax-icn 
 |-  _i e. CC
7 3re 
 |-  3 e. RR
8 3pos 
 |-  0 < 3
9 7 8 sqrtpclii 
 |-  ( sqrt ` 3 ) e. RR
10 9 recni 
 |-  ( sqrt ` 3 ) e. CC
11 6 10 mulcli 
 |-  ( _i x. ( sqrt ` 3 ) ) e. CC
12 2cn 
 |-  2 e. CC
13 2ne0 
 |-  2 =/= 0
14 5 11 12 13 divdiri 
 |-  ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) = ( ( -u 1 / 2 ) + ( ( _i x. ( sqrt ` 3 ) ) / 2 ) )
15 6 10 12 13 divassi 
 |-  ( ( _i x. ( sqrt ` 3 ) ) / 2 ) = ( _i x. ( ( sqrt ` 3 ) / 2 ) )
16 15 oveq2i 
 |-  ( ( -u 1 / 2 ) + ( ( _i x. ( sqrt ` 3 ) ) / 2 ) ) = ( ( -u 1 / 2 ) + ( _i x. ( ( sqrt ` 3 ) / 2 ) ) )
17 14 16 eqtri 
 |-  ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) = ( ( -u 1 / 2 ) + ( _i x. ( ( sqrt ` 3 ) / 2 ) ) )
18 17 fveq2i 
 |-  ( * ` ( ( -u 1 + ( _i x. ( sqrt ` 3 ) ) ) / 2 ) ) = ( * ` ( ( -u 1 / 2 ) + ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) )
19 neg1rr 
 |-  -u 1 e. RR
20 19 rehalfcli 
 |-  ( -u 1 / 2 ) e. RR
21 9 rehalfcli 
 |-  ( ( sqrt ` 3 ) / 2 ) e. RR
22 cjreim 
 |-  ( ( ( -u 1 / 2 ) e. RR /\ ( ( sqrt ` 3 ) / 2 ) e. RR ) -> ( * ` ( ( -u 1 / 2 ) + ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) ) = ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) )
23 20 21 22 mp2an 
 |-  ( * ` ( ( -u 1 / 2 ) + ( _i x. ( ( sqrt ` 3 ) / 2 ) ) ) ) = ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) )
24 4 18 23 3eqtri 
 |-  ( * ` W ) = ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) )
25 2 24 eqtr3i 
 |-  ( W ^ 2 ) = ( ( -u 1 / 2 ) - ( _i x. ( ( sqrt ` 3 ) / 2 ) ) )