Theorem goldrarr

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

	Ref	Expression
Hypothesis	goldra.val	$$⊢F=2\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
Assertion	goldrarr	$$⊢F\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		goldra.val	$$⊢F=2\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
2		2re	$$⊢2\in ℝ$$
3		pire	$$⊢\mathrm{\pi }\in ℝ$$
4		5re	$$⊢5\in ℝ$$
5		5pos	$$⊢0<5$$
6	4 5	gt0ne0ii	$$⊢5\ne 0$$
7	3 4 6	redivcli	$$⊢\frac{\mathrm{\pi }}{5}\in ℝ$$
8		recoscl	$$⊢\frac{\mathrm{\pi }}{5}\in ℝ\to \cos \left(\frac{\mathrm{\pi }}{5}\right)\in ℝ$$
9	7 8	ax-mp	$$⊢\cos \left(\frac{\mathrm{\pi }}{5}\right)\in ℝ$$
10	2 9	remulcli	$$⊢2\cos \left(\frac{\mathrm{\pi }}{5}\right)\in ℝ$$
11	1 10	eqeltri	$$⊢F\in ℝ$$