Theorem goldracos5teq

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

	Ref	Expression
Hypothesis	goldra.val	⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
Assertion	goldracos5teq	⊢ ( cos ‘ π ) = ( ( ( ; 1 6 · ( ( 𝐹 / 2 ) ↑ 5 ) ) − ( ; 2 0 · ( ( 𝐹 / 2 ) ↑ 3 ) ) ) + ( 5 · ( 𝐹 / 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		goldra.val	⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
2		picn	⊢ π ∈ ℂ
3		5cn	⊢ 5 ∈ ℂ
4		5re	⊢ 5 ∈ ℝ
5		5pos	⊢ 0 < 5
6	4 5	gt0ne0ii	⊢ 5 ≠ 0
7	2 3 6	divcli	⊢ ( π / 5 ) ∈ ℂ
8	2 3 6	divcan2i	⊢ ( 5 · ( π / 5 ) ) = π
9	8	eqcomi	⊢ π = ( 5 · ( π / 5 ) )
10		2cn	⊢ 2 ∈ ℂ
11		coscl	⊢ ( ( π / 5 ) ∈ ℂ → ( cos ‘ ( π / 5 ) ) ∈ ℂ )
12	7 11	ax-mp	⊢ ( cos ‘ ( π / 5 ) ) ∈ ℂ
13		2ne0	⊢ 2 ≠ 0
14	1	eqcomi	⊢ ( 2 · ( cos ‘ ( π / 5 ) ) ) = 𝐹
15	10 12 13 14	mvllmuli	⊢ ( cos ‘ ( π / 5 ) ) = ( 𝐹 / 2 )
16	15	eqcomi	⊢ ( 𝐹 / 2 ) = ( cos ‘ ( π / 5 ) )
17		cos5teq	⊢ ( ( ( π / 5 ) ∈ ℂ ∧ π = ( 5 · ( π / 5 ) ) ∧ ( 𝐹 / 2 ) = ( cos ‘ ( π / 5 ) ) ) → ( cos ‘ π ) = ( ( ( ; 1 6 · ( ( 𝐹 / 2 ) ↑ 5 ) ) − ( ; 2 0 · ( ( 𝐹 / 2 ) ↑ 3 ) ) ) + ( 5 · ( 𝐹 / 2 ) ) ) )
18	7 9 16 17	mp3an	⊢ ( cos ‘ π ) = ( ( ( ; 1 6 · ( ( 𝐹 / 2 ) ↑ 5 ) ) − ( ; 2 0 · ( ( 𝐹 / 2 ) ↑ 3 ) ) ) + ( 5 · ( 𝐹 / 2 ) ) )