---
tags: Euclidean_Geometry
---

Regular Pentagon with a Right Triangle Inside
===

See the picture.
Let $ABCDE$ be a regular pentagon. And let $F$ and $G$ be two points on $\overline{BC}$ and $\overline{CD}$ respectively such that $\angle FAG =36^{\circ}$ and $\overline{AF}\bot\overline{FG}$. Show the following.
* $\overline{EG}$ bisects $\angle CED$; that is $\angle GED =18^{\circ}$.
* $A,F,G,E$ are cocyclic.
* $\overline{BF}=\overline{FC}$.

__A Computational Proof__

## Use SageMath to execute the following code.

computational_proof = r"""
Without loss of generality, we may assume that the length
of one side of the regular pentagon is 1.
Let θ=∠BAF, δ=∠GED, x=BF and z=CG.
By applying the law of sines on these triangles, ΔABF,
ΔCGF, and ΔGDE, we obtain the following equations.
    x=sinθ/sin(72°-θ) ............................(1)
    tan(36°)=FG/AF=(1-x)sinθ/(x*sin(54°-θ)) ......(2)
    z=(1-x)sin(18°+θ)/sin(54°-θ) .................(3)
    sin(δ)/sin(72°-δ)=1-z ........................(4)
There are four equations to solve four variables.
Note that θ and δ belong to (0,3π/5).
In equation (2), we replace x via equation (1) and get
    sin(54°-θ)tan(36°)=2cos(36°)sin(36°-θ) .......(5)

Let α=18°+θ. By (5), we have that
    tan(θ)=(tan(36°)sin(54°)-2cos(36°)sin(36°))/(tan(36°)cos(54°)-2cos^2(36°))
    tan(α)=(tan(36°)sin(72°)-2cos(36°)sin(54°))/(tan(36°)cos(72°)-2cos(36°)cos(54°))
From (1), (2) and (3), we can derive that z=tan(α)tan(36°),
and by substitute it in equation (4), we get 
    sin(δ)/sin(72°-δ)=1-tan(α)tan(36°)
Let r := 1-tan(α)tan(36°). Then
    tan(δ)=r*sin(72°)/(1+r*cos(72°)) ..............(6)

In the following code, we will check these equations
    tan(θ)=sin(72°)/(2+cos(72°)) ..................(7)
    r*sin(72°)/(1+r*cos(72°))=sin(18°)/cos(18°) ...(8)
"""

## s{number} means sin(number°) and c{number} means cos(number°)
var("s18 c18")
s36 = 2*s18*c18
c36 = c18^2-s18^2
s54 = 3*s18-4*s18^3
c54 = 4*c18^3 - 3*c18
s72 = 2*s36*c36
c72 = c36^2-s36^2

## Check equation (7)
tan_theta=(s36*s54/c36-2*c36*s36)/(s36*c54/c36-2*c36^2)

cross1 = (tan_theta.numerator())*(2+c72) - (tan_theta.denominator())*s72
show(cross1.substitute({s18:sin(pi/10),c18:cos(pi/10)}).factor()) ## print 0

## Check equation (8)
tan_alpha = (s36*s72/c36-2*c36*s54)/(s36*c72/c36-2*c36*c54)
r = 1-tan_alpha*s36/c36
tan_delta = (r*s72/(1+r*c72)).factor()

cross2 = (tan_delta.numerator())*c18 - (tan_delta.denominator())*s18
show(cross2.substitute({s18:sin(pi/10),c18:cos(pi/10)}).factor()) ## print 0

computational_proof_continued = r"""
Now by (7), we have that
    2sin(θ)=sin(72°)cos(θ)-cos(72°)sin(θ)=sin(72°-θ),
whence
    x=sinθ/sin(72°-θ)=1/2.
    
By (6) and (8), we have that δ=18°. So ∠GEA=90° and thus ∠GEA+∠GFA=180°, 
which infers that A,F,G,E are cocyclic.
"""

__A Geometric Proof__
Let $H$ be the midpoint of $\overline{AG}$. Extend $\overline{CH}$, and let $P$ be the intersection point of $\overleftrightarrow{CH}$ and $\overline{AE}$.
Since $\angle FHG+\angle FCG=180^{\circ}$, $F,C,G,H$ must be cocyclic. So $\angle HCF=\angle FGH=54^{\circ}$, and hence $\overline{CP}$ bisects $\angle BCD$. Therefore $P$ is the midpoint of $\overline{AE}$ and $\overline{CP}\bot\overline{AE}$.
Now consider $\triangle{AGE}$. Since $\overline{AH}/\overline{AG}=1/2=\overline{AP}/\overline{AE}$, we have $\overline{PH}/\!/\overline{EG}$. Thus $\angle AEG=90^{\circ}$ and $\angle GED=18^{\circ}$.
Since $\angle AEG+\angle AFG=180^{\circ}$, $A,F,G,E$ are cocyclic. Furthermore, we have that $\angle AEF=\angle AGF=54^{\circ}$, and hence that $\overline{EF}$ bisects $\angle AED$, wherefore $F$ is the midpoint of $\overline{BC}$.$\blacksquare$