Theorem goldrasin

Description: Alternative trigonometric formula for the golden ratio. (Contributed by Ender Ting, 15-Mar-2026)

	Ref	Expression
Hypothesis	goldra.val	$$⊢F=2\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
Assertion	goldrasin	$$⊢F=2\sin \mathrm{\pi }\left(\frac{3}{10}\right)$$

Proof

Step	Hyp	Ref	Expression
1		goldra.val	$$⊢F=2\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
2		picn	$$⊢\mathrm{\pi }\in ℂ$$
3		5cn	$$⊢5\in ℂ$$
4		5re	$$⊢5\in ℝ$$
5		5pos	$$⊢0<5$$
6	4 5	gt0ne0ii	$$⊢5\ne 0$$
7	2 3 6	divreci	$$⊢\frac{\mathrm{\pi }}{5}=\mathrm{\pi }\left(\frac{1}{5}\right)$$
8		2cn	$$⊢2\in ℂ$$
9		2ne0	$$⊢2\ne 0$$
10	8 3 9 6	subreci	$$⊢\left(\frac{1}{2}\right)-\left(\frac{1}{5}\right)=\frac{5-2}{2\cdot 5}$$
11		3cn	$$⊢3\in ℂ$$
12		3p2e5	$$⊢3+2=5$$
13	12	eqcomi	$$⊢5=3+2$$
14	11 8 13	mvrraddi	$$⊢5-2=3$$
15		5t2e10	$$⊢5\cdot 2=10$$
16	3 8 15	mulcomli	$$⊢2\cdot 5=10$$
17	14 16	oveq12i	$$⊢\frac{5-2}{2\cdot 5}=\frac{3}{10}$$
18	10 17	eqtri	$$⊢\left(\frac{1}{2}\right)-\left(\frac{1}{5}\right)=\frac{3}{10}$$
19	18	eqcomi	$$⊢\frac{3}{10}=\left(\frac{1}{2}\right)-\left(\frac{1}{5}\right)$$
20		10re	$$⊢10\in ℝ$$
21	20	recni	$$⊢10\in ℂ$$
22		10pos	$$⊢0<10$$
23	20 22	gt0ne0ii	$$⊢10\ne 0$$
24	11 21 23	divcli	$$⊢\frac{3}{10}\in ℂ$$
25	24	a1i	$$⊢\top \to \frac{3}{10}\in ℂ$$
26	3 6	reccli	$$⊢\frac{1}{5}\in ℂ$$
27	26	a1i	$$⊢\top \to \frac{1}{5}\in ℂ$$
28		halfcn	$$⊢\frac{1}{2}\in ℂ$$
29	28	a1i	$$⊢\top \to \frac{1}{2}\in ℂ$$
30	25 27 29	subexsub	$$⊢\top \to \left(\frac{3}{10}=\left(\frac{1}{2}\right)-\left(\frac{1}{5}\right)\leftrightarrow \frac{1}{5}=\left(\frac{1}{2}\right)-\left(\frac{3}{10}\right)\right)$$
31	30	mptru	$$⊢\frac{3}{10}=\left(\frac{1}{2}\right)-\left(\frac{1}{5}\right)\leftrightarrow \frac{1}{5}=\left(\frac{1}{2}\right)-\left(\frac{3}{10}\right)$$
32	19 31	mpbi	$$⊢\frac{1}{5}=\left(\frac{1}{2}\right)-\left(\frac{3}{10}\right)$$
33	32	oveq2i	$$⊢\mathrm{\pi }\left(\frac{1}{5}\right)=\mathrm{\pi }\left(\left(\frac{1}{2}\right)-\left(\frac{3}{10}\right)\right)$$
34	2 28 24	subdii	$$⊢\mathrm{\pi }\left(\left(\frac{1}{2}\right)-\left(\frac{3}{10}\right)\right)=\mathrm{\pi }\left(\frac{1}{2}\right)-\mathrm{\pi }\left(\frac{3}{10}\right)$$
35	33 34	eqtri	$$⊢\mathrm{\pi }\left(\frac{1}{5}\right)=\mathrm{\pi }\left(\frac{1}{2}\right)-\mathrm{\pi }\left(\frac{3}{10}\right)$$
36	7 35	eqtri	$$⊢\frac{\mathrm{\pi }}{5}=\mathrm{\pi }\left(\frac{1}{2}\right)-\mathrm{\pi }\left(\frac{3}{10}\right)$$
37	2 8 9	divreci	$$⊢\frac{\mathrm{\pi }}{2}=\mathrm{\pi }\left(\frac{1}{2}\right)$$
38	37	eqcomi	$$⊢\mathrm{\pi }\left(\frac{1}{2}\right)=\frac{\mathrm{\pi }}{2}$$
39	38	oveq1i	$$⊢\mathrm{\pi }\left(\frac{1}{2}\right)-\mathrm{\pi }\left(\frac{3}{10}\right)=\left(\frac{\mathrm{\pi }}{2}\right)-\mathrm{\pi }\left(\frac{3}{10}\right)$$
40	36 39	eqtri	$$⊢\frac{\mathrm{\pi }}{5}=\left(\frac{\mathrm{\pi }}{2}\right)-\mathrm{\pi }\left(\frac{3}{10}\right)$$
41	40	fveq2i	$$⊢\cos \left(\frac{\mathrm{\pi }}{5}\right)=\cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-\mathrm{\pi }\left(\frac{3}{10}\right)\right)$$
42	2 24	mulcli	$$⊢\mathrm{\pi }\left(\frac{3}{10}\right)\in ℂ$$
43		coshalfpim	$$⊢\mathrm{\pi }\left(\frac{3}{10}\right)\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-\mathrm{\pi }\left(\frac{3}{10}\right)\right)=\sin \mathrm{\pi }\left(\frac{3}{10}\right)$$
44	42 43	ax-mp	$$⊢\cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-\mathrm{\pi }\left(\frac{3}{10}\right)\right)=\sin \mathrm{\pi }\left(\frac{3}{10}\right)$$
45	41 44	eqtri	$$⊢\cos \left(\frac{\mathrm{\pi }}{5}\right)=\sin \mathrm{\pi }\left(\frac{3}{10}\right)$$
46	45	oveq2i	$$⊢2\cos \left(\frac{\mathrm{\pi }}{5}\right)=2\sin \mathrm{\pi }\left(\frac{3}{10}\right)$$
47	1 46	eqtri	$$⊢F=2\sin \mathrm{\pi }\left(\frac{3}{10}\right)$$