Theorem goldrarr

Description: The golden ratio is a real value. (Contributed by Ender Ting, 15-Mar-2026)

	Ref	Expression
Hypothesis	goldra.val	⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
Assertion	goldrarr	⊢ 𝐹 ∈ ℝ

Proof

Step	Hyp	Ref	Expression
1		goldra.val	⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
2		2re	⊢ 2 ∈ ℝ
3		pire	⊢ π ∈ ℝ
4		5re	⊢ 5 ∈ ℝ
5		5pos	⊢ 0 < 5
6	4 5	gt0ne0ii	⊢ 5 ≠ 0
7	3 4 6	redivcli	⊢ ( π / 5 ) ∈ ℝ
8		recoscl	⊢ ( ( π / 5 ) ∈ ℝ → ( cos ‘ ( π / 5 ) ) ∈ ℝ )
9	7 8	ax-mp	⊢ ( cos ‘ ( π / 5 ) ) ∈ ℝ
10	2 9	remulcli	⊢ ( 2 · ( cos ‘ ( π / 5 ) ) ) ∈ ℝ
11	1 10	eqeltri	⊢ 𝐹 ∈ ℝ