Theorem goldrarp

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

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

Proof

Step	Hyp	Ref	Expression
1		goldra.val	⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
2	1	goldrarr	⊢ 𝐹 ∈ ℝ
3	1	goldrapos	⊢ 0 < 𝐹
4	2 3	elrpii	⊢ 𝐹 ∈ ℝ+