Theorem goldratmolem4

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

	Ref	Expression
Hypothesis	goldra.val	⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
Assertion	goldratmolem4	⊢ ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) = 0

Proof

Step	Hyp	Ref	Expression
1		goldra.val	⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
2	1	goldrarr	⊢ 𝐹 ∈ ℝ
3		2re	⊢ 2 ∈ ℝ
4	2 3	readdcli	⊢ ( 𝐹 + 2 ) ∈ ℝ
5	1	goldrapos	⊢ 0 < 𝐹
6		2pos	⊢ 0 < 2
7	2 3 5 6	addgt0ii	⊢ 0 < ( 𝐹 + 2 )
8	4 7	gt0ne0ii	⊢ ( 𝐹 + 2 ) ≠ 0
9	8	neii	⊢ ¬ ( 𝐹 + 2 ) = 0
10	2	recni	⊢ 𝐹 ∈ ℂ
11	10	goldpolyfactor	⊢ ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) · ( 𝐹 + 2 ) ) = ( ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) + 2 )
12	1	goldratmolem3	⊢ ( ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) + 2 ) = 0
13	11 12	eqtri	⊢ ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) · ( 𝐹 + 2 ) ) = 0
14	10	sqcli	⊢ ( 𝐹 ↑ 2 ) ∈ ℂ
15	14 10	subcli	⊢ ( ( 𝐹 ↑ 2 ) − 𝐹 ) ∈ ℂ
16		ax-1cn	⊢ 1 ∈ ℂ
17	15 16	subcli	⊢ ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ∈ ℂ
18	17 17	mulcli	⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) ∈ ℂ
19		2cn	⊢ 2 ∈ ℂ
20	10 19	addcli	⊢ ( 𝐹 + 2 ) ∈ ℂ
21	18 20	mul0ori	⊢ ( ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) · ( 𝐹 + 2 ) ) = 0 ↔ ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) = 0 ∨ ( 𝐹 + 2 ) = 0 ) )
22	13 21	mpbi	⊢ ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) = 0 ∨ ( 𝐹 + 2 ) = 0 )
23		orcom	⊢ ( ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) = 0 ∨ ( 𝐹 + 2 ) = 0 ) ↔ ( ( 𝐹 + 2 ) = 0 ∨ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) = 0 ) )
24	22 23	mpbi	⊢ ( ( 𝐹 + 2 ) = 0 ∨ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) = 0 )
25	9 24	mtpor	⊢ ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) = 0
26	17	msq0i	⊢ ( ( ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) · ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) ) = 0 ↔ ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) = 0 )
27	25 26	mpbi	⊢ ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) = 0