20200219.langley-adventitious-angles.sage

## Let FBCD be a quadrilateral, angle(DBF)=a, angle(DBC)=b,
## angle(FCB)=c, angle(FCD)=d, angle(FDB)=e.  Show that if a=20deg,
## b=60deg, c=50deg, d=30deg then e=30deg.

## We call ta = tan(a/2), tb = tan(b/2), etc.
## B=(0,0), C=(1,0), F=(u,v) and D=(x,y).

R.<ta,tb,tc,td,te,x,y,u,v> = PolynomialRing(QQ,9)

def ratcos(t):
    return (1-t^2)/(1+t^2)
def ratsin(t):
    return 2*t/(1+t^2)
def rattan(t):
    return 2*t/(1-t^2)
def ratadd(t,tt):
    return (t+tt)/(1-t*tt)

eqn1 = numerator((y/x) - rattan(tb))
eqn2 = numerator((y/(1-x)) - rattan(ratadd(tc,td)))
eqn3 = numerator((v/u) - rattan(ratadd(ta,tb)))
eqn4 = numerator((v/(1-u)) - rattan(tc))
## eqn5 = factor(numerator(ratcos(te)^2*(x^2+y^2)*((x-u)^2+(y-v)^2) - (x*(x-u) + y*(y-v))^2))[1][0]
eqn5 = te^2*y*u - te^2*x*v - 2*te*x^2 - 2*te*y^2 + 2*te*x*u + 2*te*y*v - y*u + x*v

eqnangles = factor((R.ideal([eqn1,eqn2,eqn3,eqn4,eqn5]).elimination_ideal([u,v,x,y])).gens()[0])
## We get: -ta^2*tb*tc^4*td*te - ta*tb^2*tc^4*td*te - ta*tb^2*tc^3*td^2*te + ta*tb^2*tc^3*td*te^2 + ta*tb^2*tc^2*td^2*te^2 + ta*tb*tc^3*td^2*te^2 - ta*tb^2*tc^3*td - ta*tb^2*tc^2*td^2 - ta*tb*tc^3*td^2 + ta*tb^2*tc^3*te - 2*ta^2*tb*tc^2*td*te + 2*ta*tb^2*tc^2*td*te + 4*ta*tb*tc^3*td*te + ta*tc^4*td*te + tb*tc^4*td*te + ta*tb^2*tc*td^2*te + 4*ta*tb*tc^2*td^2*te + ta*tc^3*td^2*te - ta*tb^2*tc^2*te^2 - ta*tb*tc^3*te^2 - ta*tb^2*tc*td*te^2 - 4*ta*tb*tc^2*td*te^2 - ta*tc^3*td*te^2 - ta*tb*tc*td^2*te^2 - ta*tc^2*td^2*te^2 + ta*tb^2*tc^2 + ta*tb*tc^3 + ta*tb^2*tc*td + 4*ta*tb*tc^2*td + ta*tc^3*td + ta*tb*tc*td^2 + ta*tc^2*td^2 - ta*tb^2*tc*te - 4*ta*tb*tc^2*te - ta*tc^3*te - ta^2*tb*td*te - ta*tb^2*td*te - 4*ta*tb*tc*td*te - 2*ta*tc^2*td*te + 2*tb*tc^2*td*te - ta*tc*td^2*te + ta*tb*tc*te^2 + ta*tc^2*te^2 + ta*tc*td*te^2 - ta*tb*tc - ta*tc^2 - ta*tc*td + ta*tc*te + ta*td*te + tb*td*te

eqnangles.subs({ta:QQbar(tan(pi/18)), tb:QQbar(tan(pi/6)), tc:QQbar(tan(5*pi/36)), td:QQbar(tan(pi/12)), te:QQbar(tan(pi/12))}) == 0