Theorem goldratmolem4

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

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

Proof

Step	Hyp	Ref	Expression
1		goldra.val	|- F = ( 2 x. ( cos ` ( _pi / 5 ) ) )
2	1	goldrarr	|- F e. RR
3		2re	|- 2 e. RR
4	2 3	readdcli	|- ( F + 2 ) e. RR
5	1	goldrapos	|- 0 < F
6		2pos	|- 0 < 2
7	2 3 5 6	addgt0ii	|- 0 < ( F + 2 )
8	4 7	gt0ne0ii	|- ( F + 2 ) =/= 0
9	8	neii	|- -. ( F + 2 ) = 0
10	2	recni	|- F e. CC
11	10	goldpolyfactor	|- ( ( ( ( ( F ^ 2 ) - F ) - 1 ) x. ( ( ( F ^ 2 ) - F ) - 1 ) ) x. ( F + 2 ) ) = ( ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) ) + 2 )
12	1	goldratmolem3	|- ( ( ( ( F ^ 5 ) - ( 5 x. ( F ^ 3 ) ) ) + ( 5 x. F ) ) + 2 ) = 0
13	11 12	eqtri	|- ( ( ( ( ( F ^ 2 ) - F ) - 1 ) x. ( ( ( F ^ 2 ) - F ) - 1 ) ) x. ( F + 2 ) ) = 0
14	10	sqcli	|- ( F ^ 2 ) e. CC
15	14 10	subcli	|- ( ( F ^ 2 ) - F ) e. CC
16		ax-1cn	|- 1 e. CC
17	15 16	subcli	|- ( ( ( F ^ 2 ) - F ) - 1 ) e. CC
18	17 17	mulcli	|- ( ( ( ( F ^ 2 ) - F ) - 1 ) x. ( ( ( F ^ 2 ) - F ) - 1 ) ) e. CC
19		2cn	|- 2 e. CC
20	10 19	addcli	|- ( F + 2 ) e. CC
21	18 20	mul0ori	|- ( ( ( ( ( ( F ^ 2 ) - F ) - 1 ) x. ( ( ( F ^ 2 ) - F ) - 1 ) ) x. ( F + 2 ) ) = 0 <-> ( ( ( ( ( F ^ 2 ) - F ) - 1 ) x. ( ( ( F ^ 2 ) - F ) - 1 ) ) = 0 \/ ( F + 2 ) = 0 ) )
22	13 21	mpbi	|- ( ( ( ( ( F ^ 2 ) - F ) - 1 ) x. ( ( ( F ^ 2 ) - F ) - 1 ) ) = 0 \/ ( F + 2 ) = 0 )
23		orcom	|- ( ( ( ( ( ( F ^ 2 ) - F ) - 1 ) x. ( ( ( F ^ 2 ) - F ) - 1 ) ) = 0 \/ ( F + 2 ) = 0 ) <-> ( ( F + 2 ) = 0 \/ ( ( ( ( F ^ 2 ) - F ) - 1 ) x. ( ( ( F ^ 2 ) - F ) - 1 ) ) = 0 ) )
24	22 23	mpbi	|- ( ( F + 2 ) = 0 \/ ( ( ( ( F ^ 2 ) - F ) - 1 ) x. ( ( ( F ^ 2 ) - F ) - 1 ) ) = 0 )
25	9 24	mtpor	|- ( ( ( ( F ^ 2 ) - F ) - 1 ) x. ( ( ( F ^ 2 ) - F ) - 1 ) ) = 0
26	17	msq0i	|- ( ( ( ( ( F ^ 2 ) - F ) - 1 ) x. ( ( ( F ^ 2 ) - F ) - 1 ) ) = 0 <-> ( ( ( F ^ 2 ) - F ) - 1 ) = 0 )
27	25 26	mpbi	|- ( ( ( F ^ 2 ) - F ) - 1 ) = 0