Metamath Proof Explorer

Theorem goldracos5teq

Description: Lemma 1 for determining the value of golden ratio. (Contributed by Ender Ting, 9-May-2026)

Ref Expression
Hypothesis goldra.val 
|- F = ( 2 x. ( cos ` ( _pi / 5 ) ) )
Assertion goldracos5teq 
|- ( cos ` _pi ) = ( ( ( ; 1 6 x. ( ( F / 2 ) ^ 5 ) ) - ( ; 2 0 x. ( ( F / 2 ) ^ 3 ) ) ) + ( 5 x. ( F / 2 ) ) )

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 divcli 
 |-  ( _pi / 5 ) e. CC
8 2 3 6 divcan2i 
 |-  ( 5 x. ( _pi / 5 ) ) = _pi
9 8 eqcomi 
 |-  _pi = ( 5 x. ( _pi / 5 ) )
10 2cn 
 |-  2 e. CC
11 coscl 
 |-  ( ( _pi / 5 ) e. CC -> ( cos ` ( _pi / 5 ) ) e. CC )
12 7 11 ax-mp 
 |-  ( cos ` ( _pi / 5 ) ) e. CC
13 2ne0 
 |-  2 =/= 0
14 1 eqcomi 
 |-  ( 2 x. ( cos ` ( _pi / 5 ) ) ) = F
15 10 12 13 14 mvllmuli 
 |-  ( cos ` ( _pi / 5 ) ) = ( F / 2 )
16 15 eqcomi 
 |-  ( F / 2 ) = ( cos ` ( _pi / 5 ) )
17 cos5teq 
 |-  ( ( ( _pi / 5 ) e. CC /\ _pi = ( 5 x. ( _pi / 5 ) ) /\ ( F / 2 ) = ( cos ` ( _pi / 5 ) ) ) -> ( cos ` _pi ) = ( ( ( ; 1 6 x. ( ( F / 2 ) ^ 5 ) ) - ( ; 2 0 x. ( ( F / 2 ) ^ 3 ) ) ) + ( 5 x. ( F / 2 ) ) ) )
18 7 9 16 17 mp3an 
 |-  ( cos ` _pi ) = ( ( ( ; 1 6 x. ( ( F / 2 ) ^ 5 ) ) - ( ; 2 0 x. ( ( F / 2 ) ^ 3 ) ) ) + ( 5 x. ( F / 2 ) ) )