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 
|- F = ( 2 x. ( cos ` ( _pi / 5 ) ) )
Assertion goldrasin 
|- F = ( 2 x. ( sin ` ( _pi x. ( 3 / ; 1 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 goldra.val 
 |-  F = ( 2 x. ( cos ` ( _pi / 5 ) ) )
2 picn 
 |-  _pi e. CC
3 5cn 
 |-  5 e. CC
4 5re 
 |-  5 e. RR
5 5pos 
 |-  0 < 5
6 4 5 gt0ne0ii 
 |-  5 =/= 0
7 2 3 6 divreci 
 |-  ( _pi / 5 ) = ( _pi x. ( 1 / 5 ) )
8 2cn 
 |-  2 e. CC
9 2ne0 
 |-  2 =/= 0
10 8 3 9 6 subreci 
 |-  ( ( 1 / 2 ) - ( 1 / 5 ) ) = ( ( 5 - 2 ) / ( 2 x. 5 ) )
11 3cn 
 |-  3 e. CC
12 3p2e5 
 |-  ( 3 + 2 ) = 5
13 12 eqcomi 
 |-  5 = ( 3 + 2 )
14 11 8 13 mvrraddi 
 |-  ( 5 - 2 ) = 3
15 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
16 3 8 15 mulcomli 
 |-  ( 2 x. 5 ) = ; 1 0
17 14 16 oveq12i 
 |-  ( ( 5 - 2 ) / ( 2 x. 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 e. RR
21 20 recni 
 |-  ; 1 0 e. CC
22 10pos 
 |-  0 < ; 1 0
23 20 22 gt0ne0ii 
 |-  ; 1 0 =/= 0
24 11 21 23 divcli 
 |-  ( 3 / ; 1 0 ) e. CC
25 24 a1i 
 |-  ( T. -> ( 3 / ; 1 0 ) e. CC )
26 3 6 reccli 
 |-  ( 1 / 5 ) e. CC
27 26 a1i 
 |-  ( T. -> ( 1 / 5 ) e. CC )
28 halfcn 
 |-  ( 1 / 2 ) e. CC
29 28 a1i 
 |-  ( T. -> ( 1 / 2 ) e. CC )
30 25 27 29 subexsub 
 |-  ( T. -> ( ( 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 
 |-  ( _pi x. ( 1 / 5 ) ) = ( _pi x. ( ( 1 / 2 ) - ( 3 / ; 1 0 ) ) )
34 2 28 24 subdii 
 |-  ( _pi x. ( ( 1 / 2 ) - ( 3 / ; 1 0 ) ) ) = ( ( _pi x. ( 1 / 2 ) ) - ( _pi x. ( 3 / ; 1 0 ) ) )
35 33 34 eqtri 
 |-  ( _pi x. ( 1 / 5 ) ) = ( ( _pi x. ( 1 / 2 ) ) - ( _pi x. ( 3 / ; 1 0 ) ) )
36 7 35 eqtri 
 |-  ( _pi / 5 ) = ( ( _pi x. ( 1 / 2 ) ) - ( _pi x. ( 3 / ; 1 0 ) ) )
37 2 8 9 divreci 
 |-  ( _pi / 2 ) = ( _pi x. ( 1 / 2 ) )
38 37 eqcomi 
 |-  ( _pi x. ( 1 / 2 ) ) = ( _pi / 2 )
39 38 oveq1i 
 |-  ( ( _pi x. ( 1 / 2 ) ) - ( _pi x. ( 3 / ; 1 0 ) ) ) = ( ( _pi / 2 ) - ( _pi x. ( 3 / ; 1 0 ) ) )
40 36 39 eqtri 
 |-  ( _pi / 5 ) = ( ( _pi / 2 ) - ( _pi x. ( 3 / ; 1 0 ) ) )
41 40 fveq2i 
 |-  ( cos ` ( _pi / 5 ) ) = ( cos ` ( ( _pi / 2 ) - ( _pi x. ( 3 / ; 1 0 ) ) ) )
42 2 24 mulcli 
 |-  ( _pi x. ( 3 / ; 1 0 ) ) e. CC
43 coshalfpim 
 |-  ( ( _pi x. ( 3 / ; 1 0 ) ) e. CC -> ( cos ` ( ( _pi / 2 ) - ( _pi x. ( 3 / ; 1 0 ) ) ) ) = ( sin ` ( _pi x. ( 3 / ; 1 0 ) ) ) )
44 42 43 ax-mp 
 |-  ( cos ` ( ( _pi / 2 ) - ( _pi x. ( 3 / ; 1 0 ) ) ) ) = ( sin ` ( _pi x. ( 3 / ; 1 0 ) ) )
45 41 44 eqtri 
 |-  ( cos ` ( _pi / 5 ) ) = ( sin ` ( _pi x. ( 3 / ; 1 0 ) ) )
46 45 oveq2i 
 |-  ( 2 x. ( cos ` ( _pi / 5 ) ) ) = ( 2 x. ( sin ` ( _pi x. ( 3 / ; 1 0 ) ) ) )
47 1 46 eqtri 
 |-  F = ( 2 x. ( sin ` ( _pi x. ( 3 / ; 1 0 ) ) ) )