Metamath Proof Explorer

Theorem goldrasin

Description: Alternative trigonometric formula for the golden ratio. (Contributed by Ender Ting, 15-Mar-2026)

Ref Expression
Hypothesis goldra.val ⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
Assertion goldrasin 𝐹 = ( 2 · ( sin ‘ ( π · ( 3 / 1 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 goldra.val ⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
2 picn ⊢ π ∈ ℂ
3 5cn ⊢ 5 ∈ ℂ
4 5re ⊢ 5 ∈ ℝ
5 5pos ⊢ 0 < 5
6 4 5 gt0ne0ii ⊢ 5 ≠ 0
7 2 3 6 divreci ⊢ ( π / 5 ) = ( π · ( 1 / 5 ) )
8 2cn ⊢ 2 ∈ ℂ
9 2ne0 ⊢ 2 ≠ 0
10 8 3 9 6 subreci ⊢ ( ( 1 / 2 ) − ( 1 / 5 ) ) = ( ( 5 − 2 ) / ( 2 · 5 ) )
11 3cn ⊢ 3 ∈ ℂ
12 3p2e5 ⊢ ( 3 + 2 ) = 5
13 12 eqcomi ⊢ 5 = ( 3 + 2 )
14 11 8 13 mvrraddi ⊢ ( 5 − 2 ) = 3
15 5t2e10 ⊢ ( 5 · 2 ) = 1 0
16 3 8 15 mulcomli ⊢ ( 2 · 5 ) = 1 0
17 14 16 oveq12i ⊢ ( ( 5 − 2 ) / ( 2 · 5 ) ) = ( 3 / 1 0 )
18 10 17 eqtri ⊢ ( ( 1 / 2 ) − ( 1 / 5 ) ) = ( 3 / 1 0 )
19 18 eqcomi ⊢ ( 3 / 1 0 ) = ( ( 1 / 2 ) − ( 1 / 5 ) )
20 10re ⊢ 1 0 ∈ ℝ
21 20 recni ⊢ 1 0 ∈ ℂ
22 10pos ⊢ 0 < 1 0
23 20 22 gt0ne0ii ⊢ 1 0 ≠ 0
24 11 21 23 divcli ⊢ ( 3 / 1 0 ) ∈ ℂ
25 24 a1i ⊢ ( ⊤ → ( 3 / 1 0 ) ∈ ℂ )
26 3 6 reccli ⊢ ( 1 / 5 ) ∈ ℂ
27 26 a1i ⊢ ( ⊤ → ( 1 / 5 ) ∈ ℂ )
28 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
29 28 a1i ⊢ ( ⊤ → ( 1 / 2 ) ∈ ℂ )
30 25 27 29 subexsub ⊢ ( ⊤ → ( ( 3 / 1 0 ) = ( ( 1 / 2 ) − ( 1 / 5 ) ) ↔ ( 1 / 5 ) = ( ( 1 / 2 ) − ( 3 / 1 0 ) ) ) )
31 30 mptru ⊢ ( ( 3 / 1 0 ) = ( ( 1 / 2 ) − ( 1 / 5 ) ) ↔ ( 1 / 5 ) = ( ( 1 / 2 ) − ( 3 / 1 0 ) ) )
32 19 31 mpbi ⊢ ( 1 / 5 ) = ( ( 1 / 2 ) − ( 3 / 1 0 ) )
33 32 oveq2i ⊢ ( π · ( 1 / 5 ) ) = ( π · ( ( 1 / 2 ) − ( 3 / 1 0 ) ) )
34 2 28 24 subdii ⊢ ( π · ( ( 1 / 2 ) − ( 3 / 1 0 ) ) ) = ( ( π · ( 1 / 2 ) ) − ( π · ( 3 / 1 0 ) ) )
35 33 34 eqtri ⊢ ( π · ( 1 / 5 ) ) = ( ( π · ( 1 / 2 ) ) − ( π · ( 3 / 1 0 ) ) )
36 7 35 eqtri ⊢ ( π / 5 ) = ( ( π · ( 1 / 2 ) ) − ( π · ( 3 / 1 0 ) ) )
37 2 8 9 divreci ⊢ ( π / 2 ) = ( π · ( 1 / 2 ) )
38 37 eqcomi ⊢ ( π · ( 1 / 2 ) ) = ( π / 2 )
39 38 oveq1i ⊢ ( ( π · ( 1 / 2 ) ) − ( π · ( 3 / 1 0 ) ) ) = ( ( π / 2 ) − ( π · ( 3 / 1 0 ) ) )
40 36 39 eqtri ⊢ ( π / 5 ) = ( ( π / 2 ) − ( π · ( 3 / 1 0 ) ) )
41 40 fveq2i ⊢ ( cos ‘ ( π / 5 ) ) = ( cos ‘ ( ( π / 2 ) − ( π · ( 3 / 1 0 ) ) ) )
42 2 24 mulcli ⊢ ( π · ( 3 / 1 0 ) ) ∈ ℂ
43 coshalfpim ⊢ ( ( π · ( 3 / 1 0 ) ) ∈ ℂ → ( cos ‘ ( ( π / 2 ) − ( π · ( 3 / 1 0 ) ) ) ) = ( sin ‘ ( π · ( 3 / 1 0 ) ) ) )
44 42 43 ax-mp ⊢ ( cos ‘ ( ( π / 2 ) − ( π · ( 3 / 1 0 ) ) ) ) = ( sin ‘ ( π · ( 3 / 1 0 ) ) )
45 41 44 eqtri ⊢ ( cos ‘ ( π / 5 ) ) = ( sin ‘ ( π · ( 3 / 1 0 ) ) )
46 45 oveq2i ⊢ ( 2 · ( cos ‘ ( π / 5 ) ) ) = ( 2 · ( sin ‘ ( π · ( 3 / 1 0 ) ) ) )
47 1 46 eqtri ⊢ 𝐹 = ( 2 · ( sin ‘ ( π · ( 3 / 1 0 ) ) ) )