Theorem goldrarp

Description: The golden ratio is a positive real. (Contributed by Ender Ting, 16-Apr-2026)

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

Proof

Step	Hyp	Ref	Expression
1		goldra.val	$$⊢F=2\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
2	1	goldrarr	$$⊢F\in ℝ$$
3	1	goldrapos	$$⊢0<F$$
4	2 3	elrpii	$$⊢F\in {ℝ}^{+}$$