Metamath Proof Explorer

Theorem goldratmolem3

Description: Lemma 3 for determining the value of golden ratio. (Contributed by Ender Ting, 23-Jul-2026)

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

Proof

Step Hyp Ref Expression
1 goldra.val 
 |-  F = ( 2 x. ( cos ` ( _pi / 5 ) ) )
2 1 goldratmolem2 
 |-  -u 1 = ( ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) ) + ( 5 x. ( F / 2 ) ) )
3 2 oveq1i 
 |-  ( -u 1 x. 2 ) = ( ( ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) ) + ( 5 x. ( F / 2 ) ) ) x. 2 )
4 2cn 
 |-  2 e. CC
5 4 mulm1i 
 |-  ( -u 1 x. 2 ) = -u 2
6 1 goldrarr 
 |-  F e. RR
7 6 recni 
 |-  F e. CC
8 5nn0 
 |-  5 e. NN0
9 expcl 
 |-  ( ( F e. CC /\ 5 e. NN0 ) -> ( F ^ 5 ) e. CC )
10 7 8 9 mp2an 
 |-  ( F ^ 5 ) e. CC
11 2ne0 
 |-  2 =/= 0
12 10 4 11 divcli 
 |-  ( ( F ^ 5 ) / 2 ) e. CC
13 5cn 
 |-  5 e. CC
14 3nn0 
 |-  3 e. NN0
15 expcl 
 |-  ( ( F e. CC /\ 3 e. NN0 ) -> ( F ^ 3 ) e. CC )
16 7 14 15 mp2an 
 |-  ( F ^ 3 ) e. CC
17 16 4 11 divcli 
 |-  ( ( F ^ 3 ) / 2 ) e. CC
18 13 17 mulcli 
 |-  ( 5 x. ( ( F ^ 3 ) / 2 ) ) e. CC
19 12 18 subcli 
 |-  ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) ) e. CC
20 7 4 11 divcli 
 |-  ( F / 2 ) e. CC
21 13 20 mulcli 
 |-  ( 5 x. ( F / 2 ) ) e. CC
22 19 21 4 adddiri 
 |-  ( ( ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) ) + ( 5 x. ( F / 2 ) ) ) x. 2 ) = ( ( ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) ) x. 2 ) + ( ( 5 x. ( F / 2 ) ) x. 2 ) )
23 12 18 4 subdiri 
 |-  ( ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) ) x. 2 ) = ( ( ( ( F ^ 5 ) / 2 ) x. 2 ) - ( ( 5 x. ( ( F ^ 3 ) / 2 ) ) x. 2 ) )
24 10 4 11 divcan1i 
 |-  ( ( ( F ^ 5 ) / 2 ) x. 2 ) = ( F ^ 5 )
25 13 17 4 mulassi 
 |-  ( ( 5 x. ( ( F ^ 3 ) / 2 ) ) x. 2 ) = ( 5 x. ( ( ( F ^ 3 ) / 2 ) x. 2 ) )
26 16 4 11 divcan1i 
 |-  ( ( ( F ^ 3 ) / 2 ) x. 2 ) = ( F ^ 3 )
27 26 oveq2i 
 |-  ( 5 x. ( ( ( F ^ 3 ) / 2 ) x. 2 ) ) = ( 5 x. ( F ^ 3 ) )
28 25 27 eqtri 
 |-  ( ( 5 x. ( ( F ^ 3 ) / 2 ) ) x. 2 ) = ( 5 x. ( F ^ 3 ) )
29 24 28 oveq12i 
 |-  ( ( ( ( F ^ 5 ) / 2 ) x. 2 ) - ( ( 5 x. ( ( F ^ 3 ) / 2 ) ) x. 2 ) ) = ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) )
30 23 29 eqtri 
 |-  ( ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) ) x. 2 ) = ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) )
31 13 20 4 mulassi 
 |-  ( ( 5 x. ( F / 2 ) ) x. 2 ) = ( 5 x. ( ( F / 2 ) x. 2 ) )
32 7 4 11 divcan1i 
 |-  ( ( F / 2 ) x. 2 ) = F
33 32 oveq2i 
 |-  ( 5 x. ( ( F / 2 ) x. 2 ) ) = ( 5 x. F )
34 31 33 eqtri 
 |-  ( ( 5 x. ( F / 2 ) ) x. 2 ) = ( 5 x. F )
35 30 34 oveq12i 
 |-  ( ( ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) ) x. 2 ) + ( ( 5 x. ( F / 2 ) ) x. 2 ) ) = ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) )
36 22 35 eqtri 
 |-  ( ( ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) ) + ( 5 x. ( F / 2 ) ) ) x. 2 ) = ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) )
37 3 5 36 3eqtr3ri 
 |-  ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) ) = -u 2
38 13 16 mulcli 
 |-  ( 5 x. ( F ^ 3 ) ) e. CC
39 10 38 subcli 
 |-  ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) e. CC
40 13 7 mulcli 
 |-  ( 5 x. F ) e. CC
41 39 40 addcli 
 |-  ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) ) e. CC
42 addeq0 
 |-  ( ( ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) ) e. CC /\ 2 e. CC ) -> ( ( ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) ) + 2 ) = 0 <-> ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) ) = -u 2 ) )
43 41 4 42 mp2an 
 |-  ( ( ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) ) + 2 ) = 0 <-> ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) ) = -u 2 )
44 37 43 mpbir 
 |-  ( ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) ) + 2 ) = 0