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 ⊢ 𝑊 = ( bRoU ‘ 3 )
Assertion bru3val 𝑊 = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 )

Proof

Step Hyp Ref Expression
1 bru3eq.w ⊢ 𝑊 = ( bRoU ‘ 3 )
2 3nn ⊢ 3 ∈ ℕ
3 bruval3 ⊢ ( 3 ∈ ℕ → ( bRoU ‘ 3 ) = ( ( cos ‘ ( ( 2 · π ) / 3 ) ) + ( i · ( sin ‘ ( ( 2 · π ) / 3 ) ) ) ) )
4 2 3 ax-mp ⊢ ( bRoU ‘ 3 ) = ( ( cos ‘ ( ( 2 · π ) / 3 ) ) + ( i · ( sin ‘ ( ( 2 · π ) / 3 ) ) ) )
5 ax-icn ⊢ i ∈ ℂ
6 3re ⊢ 3 ∈ ℝ
7 3pos ⊢ 0 < 3
8 6 7 sqrtpclii ⊢ ( √ ‘ 3 ) ∈ ℝ
9 8 recni ⊢ ( √ ‘ 3 ) ∈ ℂ
10 2cn ⊢ 2 ∈ ℂ
11 2ne0 ⊢ 2 ≠ 0
12 5 9 10 11 divassi ⊢ ( ( i · ( √ ‘ 3 ) ) / 2 ) = ( i · ( ( √ ‘ 3 ) / 2 ) )
13 12 oveq2i ⊢ ( ( - 1 / 2 ) + ( ( i · ( √ ‘ 3 ) ) / 2 ) ) = ( ( - 1 / 2 ) + ( i · ( ( √ ‘ 3 ) / 2 ) ) )
14 neg1cn ⊢ - 1 ∈ ℂ
15 5 9 mulcli ⊢ ( i · ( √ ‘ 3 ) ) ∈ ℂ
16 14 15 10 11 divdiri ⊢ ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 ) = ( ( - 1 / 2 ) + ( ( i · ( √ ‘ 3 ) ) / 2 ) )
17 picn ⊢ π ∈ ℂ
18 3cn ⊢ 3 ∈ ℂ
19 3ne0 ⊢ 3 ≠ 0
20 10 17 18 19 divassi ⊢ ( ( 2 · π ) / 3 ) = ( 2 · ( π / 3 ) )
21 20 fveq2i ⊢ ( cos ‘ ( ( 2 · π ) / 3 ) ) = ( cos ‘ ( 2 · ( π / 3 ) ) )
22 17 18 19 divcli ⊢ ( π / 3 ) ∈ ℂ
23 cos2t ⊢ ( ( π / 3 ) ∈ ℂ → ( cos ‘ ( 2 · ( π / 3 ) ) ) = ( ( 2 · ( ( cos ‘ ( π / 3 ) ) ↑ 2 ) ) − 1 ) )
24 22 23 ax-mp ⊢ ( cos ‘ ( 2 · ( π / 3 ) ) ) = ( ( 2 · ( ( cos ‘ ( π / 3 ) ) ↑ 2 ) ) − 1 )
25 sincos3rdpi ⊢ ( ( sin ‘ ( π / 3 ) ) = ( ( √ ‘ 3 ) / 2 ) ∧ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 ) )
26 25 simpri ⊢ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 )
27 26 oveq1i ⊢ ( ( cos ‘ ( π / 3 ) ) ↑ 2 ) = ( ( 1 / 2 ) ↑ 2 )
28 10 11 sqrecii ⊢ ( ( 1 / 2 ) ↑ 2 ) = ( 1 / ( 2 ↑ 2 ) )
29 27 28 eqtri ⊢ ( ( cos ‘ ( π / 3 ) ) ↑ 2 ) = ( 1 / ( 2 ↑ 2 ) )
30 29 oveq2i ⊢ ( 2 · ( ( cos ‘ ( π / 3 ) ) ↑ 2 ) ) = ( 2 · ( 1 / ( 2 ↑ 2 ) ) )
31 30 oveq1i ⊢ ( ( 2 · ( ( cos ‘ ( π / 3 ) ) ↑ 2 ) ) − 1 ) = ( ( 2 · ( 1 / ( 2 ↑ 2 ) ) ) − 1 )
32 24 31 eqtri ⊢ ( cos ‘ ( 2 · ( π / 3 ) ) ) = ( ( 2 · ( 1 / ( 2 ↑ 2 ) ) ) − 1 )
33 10 sqvali ⊢ ( 2 ↑ 2 ) = ( 2 · 2 )
34 33 oveq2i ⊢ ( 1 / ( 2 ↑ 2 ) ) = ( 1 / ( 2 · 2 ) )
35 34 oveq2i ⊢ ( 2 · ( 1 / ( 2 ↑ 2 ) ) ) = ( 2 · ( 1 / ( 2 · 2 ) ) )
36 ax-1cn ⊢ 1 ∈ ℂ
37 10 10 mulcli ⊢ ( 2 · 2 ) ∈ ℂ
38 2t2e4 ⊢ ( 2 · 2 ) = 4
39 4ne0 ⊢ 4 ≠ 0
40 38 39 eqnetri ⊢ ( 2 · 2 ) ≠ 0
41 10 36 37 40 divassi ⊢ ( ( 2 · 1 ) / ( 2 · 2 ) ) = ( 2 · ( 1 / ( 2 · 2 ) ) )
42 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
43 divcan5 ⊢ ( ( 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 · 1 ) / ( 2 · 2 ) ) = ( 1 / 2 ) )
44 36 42 42 43 mp3an ⊢ ( ( 2 · 1 ) / ( 2 · 2 ) ) = ( 1 / 2 )
45 41 44 eqtr3i ⊢ ( 2 · ( 1 / ( 2 · 2 ) ) ) = ( 1 / 2 )
46 35 45 eqtri ⊢ ( 2 · ( 1 / ( 2 ↑ 2 ) ) ) = ( 1 / 2 )
47 46 oveq1i ⊢ ( ( 2 · ( 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 ∈ ℂ ∧ 2 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 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 ⊢ - ( 2 − 1 ) = ( 1 − 2 )
55 2m1e1 ⊢ ( 2 − 1 ) = 1
56 55 negeqi ⊢ - ( 2 − 1 ) = - 1
57 54 56 eqtr3i ⊢ ( 1 − 2 ) = - 1
58 57 oveq1i ⊢ ( ( 1 − 2 ) / 2 ) = ( - 1 / 2 )
59 47 53 58 3eqtri ⊢ ( ( 2 · ( 1 / ( 2 ↑ 2 ) ) ) − 1 ) = ( - 1 / 2 )
60 21 32 59 3eqtri ⊢ ( cos ‘ ( ( 2 · π ) / 3 ) ) = ( - 1 / 2 )
61 20 fveq2i ⊢ ( sin ‘ ( ( 2 · π ) / 3 ) ) = ( sin ‘ ( 2 · ( π / 3 ) ) )
62 sin2t ⊢ ( ( π / 3 ) ∈ ℂ → ( sin ‘ ( 2 · ( π / 3 ) ) ) = ( 2 · ( ( sin ‘ ( π / 3 ) ) · ( cos ‘ ( π / 3 ) ) ) ) )
63 22 62 ax-mp ⊢ ( sin ‘ ( 2 · ( π / 3 ) ) ) = ( 2 · ( ( sin ‘ ( π / 3 ) ) · ( cos ‘ ( π / 3 ) ) ) )
64 oveq12 ⊢ ( ( ( sin ‘ ( π / 3 ) ) = ( ( √ ‘ 3 ) / 2 ) ∧ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 ) ) → ( ( sin ‘ ( π / 3 ) ) · ( cos ‘ ( π / 3 ) ) ) = ( ( ( √ ‘ 3 ) / 2 ) · ( 1 / 2 ) ) )
65 25 64 ax-mp ⊢ ( ( sin ‘ ( π / 3 ) ) · ( cos ‘ ( π / 3 ) ) ) = ( ( ( √ ‘ 3 ) / 2 ) · ( 1 / 2 ) )
66 65 oveq2i ⊢ ( 2 · ( ( sin ‘ ( π / 3 ) ) · ( cos ‘ ( π / 3 ) ) ) ) = ( 2 · ( ( ( √ ‘ 3 ) / 2 ) · ( 1 / 2 ) ) )
67 9 10 11 divcli ⊢ ( ( √ ‘ 3 ) / 2 ) ∈ ℂ
68 67 10 11 divreci ⊢ ( ( ( √ ‘ 3 ) / 2 ) / 2 ) = ( ( ( √ ‘ 3 ) / 2 ) · ( 1 / 2 ) )
69 68 eqcomi ⊢ ( ( ( √ ‘ 3 ) / 2 ) · ( 1 / 2 ) ) = ( ( ( √ ‘ 3 ) / 2 ) / 2 )
70 69 oveq2i ⊢ ( 2 · ( ( ( √ ‘ 3 ) / 2 ) · ( 1 / 2 ) ) ) = ( 2 · ( ( ( √ ‘ 3 ) / 2 ) / 2 ) )
71 67 10 11 divcan2i ⊢ ( 2 · ( ( ( √ ‘ 3 ) / 2 ) / 2 ) ) = ( ( √ ‘ 3 ) / 2 )
72 66 70 71 3eqtri ⊢ ( 2 · ( ( sin ‘ ( π / 3 ) ) · ( cos ‘ ( π / 3 ) ) ) ) = ( ( √ ‘ 3 ) / 2 )
73 61 63 72 3eqtri ⊢ ( sin ‘ ( ( 2 · π ) / 3 ) ) = ( ( √ ‘ 3 ) / 2 )
74 73 oveq2i ⊢ ( i · ( sin ‘ ( ( 2 · π ) / 3 ) ) ) = ( i · ( ( √ ‘ 3 ) / 2 ) )
75 60 74 oveq12i ⊢ ( ( cos ‘ ( ( 2 · π ) / 3 ) ) + ( i · ( sin ‘ ( ( 2 · π ) / 3 ) ) ) ) = ( ( - 1 / 2 ) + ( i · ( ( √ ‘ 3 ) / 2 ) ) )
76 13 16 75 3eqtr4ri ⊢ ( ( cos ‘ ( ( 2 · π ) / 3 ) ) + ( i · ( sin ‘ ( ( 2 · π ) / 3 ) ) ) ) = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 )
77 1 4 76 3eqtri ⊢ 𝑊 = ( ( - 1 + ( i · ( √ ‘ 3 ) ) ) / 2 )