Theorem goldrapos

Description: Golden ratio is positive. (Contributed by Ender Ting, 16-Apr-2026)

	Ref	Expression
Hypothesis	goldra.val	⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
Assertion	goldrapos	⊢ 0 < 𝐹

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		2pos	⊢ 0 < 2
11		pipos	⊢ 0 < π
12	3 2 11 10	divgt0ii	⊢ 0 < ( π / 2 )
13		halfpire	⊢ ( π / 2 ) ∈ ℝ
14		lt0neg2	⊢ ( ( π / 2 ) ∈ ℝ → ( 0 < ( π / 2 ) ↔ - ( π / 2 ) < 0 ) )
15	13 14	ax-mp	⊢ ( 0 < ( π / 2 ) ↔ - ( π / 2 ) < 0 )
16	12 15	mpbi	⊢ - ( π / 2 ) < 0
17	3 4 11 5	divgt0ii	⊢ 0 < ( π / 5 )
18		neghalfpire	⊢ - ( π / 2 ) ∈ ℝ
19		0re	⊢ 0 ∈ ℝ
20	18 19 7	lttri	⊢ ( ( - ( π / 2 ) < 0 ∧ 0 < ( π / 5 ) ) → - ( π / 2 ) < ( π / 5 ) )
21	16 17 20	mp2an	⊢ - ( π / 2 ) < ( π / 5 )
22		2lt5	⊢ 2 < 5
23		2rp	⊢ 2 ∈ ℝ+
24	23	a1i	⊢ ( ⊤ → 2 ∈ ℝ+ )
25		5rp	⊢ 5 ∈ ℝ+
26	25	a1i	⊢ ( ⊤ → 5 ∈ ℝ+ )
27		pirp	⊢ π ∈ ℝ+
28	27	a1i	⊢ ( ⊤ → π ∈ ℝ+ )
29	24 26 28	ltdiv2d	⊢ ( ⊤ → ( 2 < 5 ↔ ( π / 5 ) < ( π / 2 ) ) )
30	29	mptru	⊢ ( 2 < 5 ↔ ( π / 5 ) < ( π / 2 ) )
31	22 30	mpbi	⊢ ( π / 5 ) < ( π / 2 )
32		neghalfpirx	⊢ - ( π / 2 ) ∈ ℝ*
33	13	rexri	⊢ ( π / 2 ) ∈ ℝ*
34		elioo2	⊢ ( ( - ( π / 2 ) ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( ( π / 5 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ ( ( π / 5 ) ∈ ℝ ∧ - ( π / 2 ) < ( π / 5 ) ∧ ( π / 5 ) < ( π / 2 ) ) ) )
35	32 33 34	mp2an	⊢ ( ( π / 5 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ ( ( π / 5 ) ∈ ℝ ∧ - ( π / 2 ) < ( π / 5 ) ∧ ( π / 5 ) < ( π / 2 ) ) )
36	7 21 31 35	mpbir3an	⊢ ( π / 5 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) )
37		cosq14gt0	⊢ ( ( π / 5 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( cos ‘ ( π / 5 ) ) )
38	36 37	ax-mp	⊢ 0 < ( cos ‘ ( π / 5 ) )
39	2 9 10 38	mulgt0ii	⊢ 0 < ( 2 · ( cos ‘ ( π / 5 ) ) )
40	39 1	breqtrri	⊢ 0 < 𝐹