########################################################### #RENE.txt: A MAPLE PACKAGE FOR STATING AND PROVING # #THEOREMS IN GEOMETRY; Save as RENE.txt , go into # # Maple, and type: read `RENE.txt`: # ########################################################### #Written by Doron Zeilberger, Rutgers University #DoronZeil at gmail dot com #Version of April 27, 2021: adding Isogonal Conjuate and Leversha's Theorem #Version of June 14, 2020: Thanks to Andrea Previtali (adding procedure LehmusConverse(m,n)) type: LehmusConverse(m,n), #Previous update: #Version of May 21, 2019 (To add (degree 3) Siebeck's theorem) # May 3, 2019 (To add van Aubel and Berendonk's theorems) # Sept. 9, 2018 (To add Miquel's Five Circle Theorem) # March 28, 2018 (To add Monthly problem P12027,March 2018, contrubuted by Dr. Z.'s Experimental Mathematics class) # Feb. 6, 2012 (To add Monthly problem P11615,contributed by Matthew Russel, Rutgers University) #Feb. 10, 2011 (To add Monthly problem 11544, P11554) #Oct. 14, 2004 (To add Sadov's theorem) #May 5, 2001 (To add Monthly Problem P10874) #Sept. 19, 2000 (TO adapt to Maple 6) #Tested (1998) on Maple V, ver. 5 and below #Thanks to Wolfram Koepf for pointing out that the previous version #did not work on Maple V, ver. 5 #First Version Written: May 8, 1998 #Thanks: May 31, 1998 (thanks to Michael Somos for spotting a bug) #The most current version is available from #http://www.math.temple.edu/~zeilberg/ print(`RENE.txt: A PACKAGE THAT USES RENE DESCARTES's`): print(`Revolutionary Approach to Geometry,`): print(`to state and prove 55 theorems in Plane Geometry`): print(``): print(`First Version Written: May 7, 1998`): print(`This version: Oct. 14, 2004 (to add Sadov's theorem)`): print(`Tested on Maple 9, ver. 5 and Maple 8`): print(`We benefited from a comment made by Wolfram Koepf and Michael Somos`): print(``): print(`written by Doron Zeilberger(zeilberg@math.temple.edu).`): print(`The most current version is always available from`): print(`http://www.math.temple.edu/~zeilberg/`): print(`For a list of the theorems type Theorems; `): print(`For a list of the definitions type : Definitions;`): print(`For a list of Monthly Problems type : MonthlyProblems;`): print(`For a list of IMO Problems type : IMO;`): print(`To see a statment of a theorem, type:`): print(` op(Name_Of_Theorem);`): print(`To see a statment of a defin., type:`): print( `op(Name_Of_Definition);`): print(`To prove a theorem, type: `): print(`Name_Of_Theorem();`); print(): print(`For example, to see the statement of Napoleon's theorem type:`): print(`op(Napoleon); `): print(`To PROVE Napoleon's theorem, type: `): print(`Napoleon(); `): print(``): print(`Common abbreviations used in naming: Pt: Point; Le: Line;`): print(`Ce:Circle ; Te: Triangle ; De: Distance; Sq: Square; `): print(``): print(`Te(m,n): Gives the three vertices of the "standard trinagle",`): print(`whose vertices are A(0,0), B(1,0) and such that`): print(` m=tan((Angle CAB)/2), and n=tan((Angle CBA)/2) `): print(``): print(`Definition TS([A_1,A_2, ...])`): print(` expresses tan(arctan(A_1)+arctan(A_2)+...)`): print(` as a rational function of A_1,A_2, ...`): print(`Everything else is self-explanatory`): print(``): print(`TO SEE BEAUTIFUL DESCRIPTIONS, IN HUMANESE, OF MANY OF THE THEOREMS`): print(`PROVED HERE, CONSULT ERIC's TREASURE TROVE OF MATH`): print(``): print(`WARNING: x and y are GLOBAL VARIABLES DENOTING THE VARIABLES`): print(`DO NOT USE THEM FOR ANY OTHER PURPOSES, AND DO NOT ASSIGN THEM`): print(` Once Again:`): print(`For the list of Theorems type:`): print(`Theorems;`): print(`For the list of Definitions type:`): print(`Definitions;`): print(`For the list of Monthly Problems Solved type:MonthlyProblems;`): print(`For the list of International Math Olympiad Problems type:IMO;`): print(`To get a completely self-contained statement AND proof of a theorem`): print(` Type "SelfContained(TheoremName);"; For example`): print(` e.g.: "SelfContained(Napoleon);" `): Theorems:=[AreaFormula,Berendonk, Bretschneider,Brianchon,Butterfly,Carnot,Casey, CentroidExists,Ceva,Clifford,deLongchamps,Desargues,EightPointCircleExists, Ekhad, EulerLineExists,EulerTetrahedronVolumeFormula,EulerTriangleFormula, Feuerbach,FeuerbachConic,FinslerHadwiger,FoxTalbot,Fregier,Fuhrmann,Gergonne, Griffiths,Herron,Hoehn,IncenterExists,IsogonalConjugateExists, Johnson,Lehmus, Lemoine,LeonAnne,Leversha, MarionMorgan, MedianTriangleLocus,Menelaus,MiquelFiveCircle, MiquelRandom,Monge,Morley,Napoleon, NinePointCircleExists,Nobbs,OrthocenterExists,Pappus,Pascal,Pivot,Poncelet, Ptolemy,Purser,RadicalCenterExists, Sadov, Siebeck, Simson,Soddy,Thebault, vanAubel, Varignon,Viviani,vonAubel, Wittenbauer]: Definitions:=[Altitude,AntiMedial,AREA,Billiard, BilliardSym,Ce,Center, Centroid,CentroidQ,CET,Circumcenter,Circumradius,Colinear,ComTangLgt, Concyclic,Concurrency,Concurrent,Contact,De,DePtLeSq,DeSq,DeSqG,EulerLine,Ft, GegonnePt,Incenter,Incircle,Inradius,IsogonalConjuate,ItIsEqui,ItIsZero,Kiss,Le, LevershaPoints, LevershaRadius,MDOS,MidPt, MirRefPtLe,MirRfPtPt,MirRefOf0,NinePointCircle,NormalToEllipse,Orthocenter, OtherCeCe,ParamCircle,ParamLine,ParEllipse,Pedal,PerpMid,PerpPQ, pmidpt, Powe, Pt,PtLeCe,Quad,RadicalCenter, RadicalLine, Radius,Slope,Sqabc,SqRtABCD, SSR,SSR1,Symmedian, Te,TS,Tangent,TangentToEllipse,TanMt,TouchCe,TouchCe1,TouchCeLe, TouchCeLe1,TcCesOut]: MonthlyProblems:=[P10637,P10673, P10678, P10693, P10703,P10710,P10734, P10749,P10780,P10783,P10796,P10804,P10810,P10845,P10874,P11554, P11615, P12027]: IMO:=[I78_4, I79_3, I82_2, I82_5]: ##########################Part I: THEOREMS############ AreaFormula:=proc() local A,B,C: ItIsZero(DeSq(A,B)*DeSq(C,Ft(C,Le(A,B)))/4-AREA(A,B,C)^2):end: Bretschneider:=proc() local A,B,C,D: ItIsZero(16*(AREA(A,B,C)+AREA(A,C,D))^2- 4*DeSq(A,C)*DeSq(B,D)+(DeSq(B,C)+DeSq(D,A)-DeSq(A,B)-DeSq(C,D))^2):end: Brianchon:=proc() local Li,t,i,c,d,P: for i from 0 to 5 do Li[i]:=TangentToEllipse(c,d,t[i]): od: for i from 0 to 5 do P[i]:=Pt(Li[i],Li[i+1 mod 6]): od: Concurrent(Le(P[0],P[3]),Le(P[1],P[4]),Le(P[2],P[5])):end: Butterfly:=proc() local P,t,i,R,Li,M,X,Y:for i from 1 to 4 do P[i]:=ParamCircle([0,0],R,t[i]) od:M:=Pt(Le(P[1],P[3]),Le(P[2],P[4])): Li:=PerpPQ([0,0],M):X:=Pt(Le(P[1],P[4]),Li):Y:=Pt(Le(P[2],P[3]),Li): ItIsZero(DeSq(M,X)-DeSq(M,Y)):end: Carnot:=proc() local m,n,T,O,O1,O2,O3,gu:T:=Te(m,n):O:=Circumcenter(T): O1:=Ft(O,Le(T[2],T[3])):O2:=Ft(O,Le(T[1],T[3])):O3:=Ft(O,Le(T[1],T[2])): SSR1([DeSq(O,O1),DeSq(O,O2),DeSq(O,O3)],Circumradius(T)-Inradius(m,n)):end: Casey:=proc() local t,P,C,R,i,j:t[1]:=1: for i from 1 to 4 do P[i]:=ParamCircle([0,0],1,t[i]): od: for i from 1 to 4 do C[i]:=[(1-R[i])*P[i][1],(1-R[i])*P[i][2]]:od: for i from 1 to 4 do for j from i+1 to 4 do t[i,j]:=simplify( ComTangLgtSq(C[i],R[i],C[j],R[j])^2,symbolic): od:od: SSR1([t[1,2]*t[3,4],t[1,3]*t[2,4],t[1,4]*t[2,3]],0):end: CentroidExists:=proc() local A,B,C: Concurrent(Le(MidPt(A,B),C),Le(MidPt(A,C),B),Le(MidPt(B,C),A)):end: Ceva:=proc() local A,B,C,O,D,E,F: A:=[0,0]: B:=[1,0]: D:=Pt(Le(B,C),Le(A,O)):E:=Pt(Le(A,C),Le(B,O)):F:=Pt(Le(A,B),Le(C,O)):ItIsZero( DeSq(B,D)*DeSq(C,E)*DeSq(A,F)-DeSq(D,C)*DeSq(E,A)*DeSq(F,B)): end: #The Contact Triangle of the Standard Triangle Te(m,n) Contact:=proc(m,n) local T,C:T:=Te(m,n):C:=Incenter(m,n): Ft(C,Le(T[1],T[2])),Ft(C,Le(T[2],T[3])),Ft(C,Le(T[3],T[1])):end: Clifford:=proc()local a,b,C,i,j,P,k: a[1]:=-2: b[1]:=0: for i from 1 to 4 do C[i]:=x^2+y^2+a[i]*x+b[i]*y: od: for i from 1 to 4 do for j from i+1 to 4 do P[i,j]:=OtherCeCe(C[i],C[j],[0,0]):od:od: for i from 1 to 4 do for j from i+1 to 4 do for k from j+1 to 4 do C[i,j,k]:= Ce(P[i,j],P[i,k],P[j,k]):od:od:od:evalb(solve({C[1,2,3]-C[1,2,4], C[1,2,3]-C[1,3,4],C[1,2,3]-C[2,3,4]},{x,y})<>NULL):end: deLongchamps:=proc() local A,B,C,O,O1,O2,l: A:=[0,0]: B:=[1,0]: O:=Circumcenter(A,B,C): O1:=Orthocenter(A,B,C):O2:=[O[1]-(O1[1]-O[1]), O[2]-(O1[2]-O[2])]:l:=EulerLine(A,B,C):ItIsZero(subs({x=O2[1],y=O2[2]},l)):end: Desargues:=proc() local A,B,i,m,t,s: for i from 1 to 3 do A[i]:=ParamLine(m[i],0,t[i]): B[i]:=ParamLine(m[i],0,s[i]):od: Colinear(Pt(Le(A[1],A[2]),Le(B[1],B[2])),Pt(Le(A[1],A[3]),Le(B[1],B[3])), Pt(Le(A[2],A[3]),Le(B[2],B[3]))):end: EightPointCircleExists:=proc() local A,B,C,D,e,f,g,h,a,b,c,d: A:=[0,-e]:B:=[f,0]:C:=[0,g]:D:=[-h,0]: a:=MidPt(A,B):b:=MidPt(B,C):c:=MidPt(C,D):d:=MidPt(D,A):Concyclic( a,b,c,d,Ft(a,Le(C,D)),Ft(b,Le(D,A)),Ft(c,Le(A,B)),Ft(d,Le(B,C))):end: EulerLineExists:=proc() local A,B,C: Colinear(Orthocenter(A,B,C),Circumcenter(A,B,C),Centroid(A,B,C)):end: with(linalg): EulerTetrahedronVolumeFormula:=proc() local P1,P2,P3,P4,P,Q,R,A,B,C,Vol, p31,p32,p41,p42,p43: P1:=[0,0,0]: P2:=[1,0,0]:P3:=[p31,p32,0]: P4:=[p41,p42,p43]:P:=DeSqG(P1,P4,3):Q:=DeSqG(P2,P4,3):R:=DeSqG(P3,P4,3): A:=DeSqG(P2,P3,3):B:=DeSqG(P3,P1,3):C:=DeSqG(P1,P2,3): Vol:=AREA([p31,p32],[1,0],[0,0])*p43/3:evalb(normal(det(array([[0,P,Q,R,1], [P,0,C,B,1],[Q,C,0,A,1],[R,B,A,0,1],[1,1,1,1,0]]))/Vol^2/288)=1):end: EulerTriangleFormula:=proc() local T,m,n,A,B,C,d,R,r,O,I1: T:=Te(m,n):A:=T[1]:B:=T[2]:C:=T[3]:O:=Incenter(m,n): I1:=Circumcenter(A,B,C):r:=Inradius(m,n):R:=Circumradius(A,B,C): d:=sqrt(DeSq(O,I1)): ItIsZero((d^2-R^2)^2-4*r^2*R^2):end: Feuerbach:=proc() local m,n:TouchCe(NinePointCircle(Te(m,n)),Incircle(m,n)):end: FeuerbachConic:=proc() local O,B,C,D,E,F,Conic,c,d: O:=Orthocenter([0,0],[1,0], [c,d]):Conic:=x^2+B*x*y+C*y^2+D*x+E*y+F:Conic:=subs(solve({subs({x=0,y=0}, Conic),subs({x=1,y=0},Conic),subs({x=c,y=d},Conic),subs({x=O[1],y=O[2]},Conic)}, {B,C,D,E,F}),Conic):ItIsZero(subs(solve({diff(Conic,x),diff(Conic,y)},{x,y}), NinePointCircle([0,0],[1,0],[c,d]))):end: FinslerHadwiger:=proc() local a,b,A,B,C,D,B1,C1,D1,Q,R,S,T:A:=[0,0]:B:=[-1,0]: C:=[-1,1]:D:=[0,1]:B1:=[a,b]:C1:=[B1[1]+b,B1[2]-a]:D1:=[b,-a]:Q:=MidPt(D,B1): S:=MidPt(B,D1):R:=Pt(Le(B,D),Le(A,C)):T:=Pt(Le(B1,D1),Le(A,C1)):evalb( ItIsZero(DeSq(Q,T)-DeSq(T,S)) and ItIsZero(DeSq(Q,T)-DeSq(Q,R)) and ItIsZero(DeSq(Q,T)-DeSq(R,S)) and ItIsZero(Slope(Q,R)*Slope(Q,T)+1)):end: FoxTalbot:=proc() local q,L,i,a,b,c,j,M: L[1]:=x: for i from 2 to 5 do L[i]:= a[i]*x+b[i]*y+c[i]: od: for i from 1 to 5 do q:=Quad(seq(L[j],j=1..i-1),seq(L[j],j=i+1..5)):M[i]:=Le(MidPt(q[1],q[3]), MidPt(q[2],q[4])):od: Concurrent(seq(M[i],i=1..5)):end: Fregier:=proc()local d,t,P,i,X,P2:for i from 0 to 2 do P[i]:= ParEllipse([0,0],d,t[i]): od: P[2]:=subs(t[2]=solve(Slope(P[0],P[1])* Slope(P[0],P[2])= -1,t[2]),P[2]):X:=Pt(NormalToEllipse([0,0],d,t[0]),Le(P[1],P[2])): ItIsZero(normal(diff(X[1],t[1]))) and ItIsZero(normal(diff(X[1],t[2]))): end: Fuhrmann:=proc() local P,Q,R,L,M,N,a,b,c,a1,b1,c1,e,f,g,t2,t3,t4,t5,t6,A,B,gu: P:=ParamCircle([0,0],1,1):Q:=ParamCircle([0,0],1,t2): R:=ParamCircle([0,0],1,t3):L:=ParamCircle([0,0],1,t4): M:=ParamCircle([0,0],1,t5):N:=ParamCircle([0,0],1,t6): a:=DeSq(L,M):b:=DeSq(R,Q):c:=DeSq(N,P):a1:=DeSq(P,Q):b1:=DeSq(M,N): c1:=DeSq(L,R): e:=DeSq(R,N):f:=DeSq(L,P):g:=DeSq(M,Q): SSR1([a*a1*e,b*b1*f,c*c1*g,a*b*c,a1*b1*c1,e*f*g],0):end: Gergonne:=proc() local m,n,T,C1:T:=Te(m,n):C1:=Incircle(m,n): Concurrent(Le(T[1],PtLeCe(Le(T[2],T[3]),C1)),Le(T[2],PtLeCe(Le(T[1],T[3]),C1)), Le(T[3],PtLeCe(Le(T[1],T[2]),C1))):end: Griffiths:=proc() local a,b,A,B,C,D,P,m,x1,c1,c2,g:A:=[0,0]:B:=[1,0]:C:=[a,b]: D:=Circumcenter(A,B,C):P:=[D[1]+x1,D[2]+m*x1]:c1:=Ce(Pedal(A,B,C,P)): c2:=NinePointCircle(A,B,C): g:=numer(factor(subs(y=solve(c1-c2,y),c2))): evalb(type(g,`*`) and (diff(op(1,g),x1)=0 or diff(op(2,g),x1)=0)):end: Herron:=proc() local q,a,b,c,s,A,B,C,b1,a2,b2,Area:A:=[0,0]:B:=[0,b1]: C:=[a2,b2]:a:=sqrt(DeSq(B,C)):b:=sqrt(DeSq(A,C)):c:=sqrt(DeSq(A,B)): s:=(a+b+c)/2: ItIsZero(AREA(A,B,C)^2-s*(s-a)*(s-b)*(s-c)):end: Hoehn:=proc() local V1,V2,V3,V4,V5,W1,W2,W3,W4,W5:V1:=[0,0]:V2:=[1,0]: W1:=Pt(Le(V1,V3),Le(V2,V5)):W2:=Pt(Le(V1,V3),Le(V2,V4)):W3:=Pt(Le(V3,V5), Le(V2,V4)):W4:=Pt(Le(V1,V4),Le(V3,V5)):W5:=Pt(Le(V1,V4),Le(V2,V5)): ItIsZero(DeSq(V1,W1)*DeSq(V2,W2)*DeSq(V3,W3)*DeSq(V4,W4)*DeSq(V5,W5)- DeSq(V1,W5)*DeSq(V2,W1)*DeSq(V3,W2)*DeSq(V4,W3)*DeSq(V5,W4)):end: IncenterExists:=proc() local m,n,A,B,C,T:T:=Te(m,n):A:=T[1]:B:=T[2]: C:=T[3]:Concurrent(y-m*x,y+n*x-n,y-C[2]-(x-C[1])*TS(m,1/n)):end: Johnson:=proc() local C,t,i,R,P: for i from 0 to 2 do C[i]:=ParamCircle( [0,0],R,t[i]): od: for i from 0 to 2 do P[i]:=MirRefOf0(C[i],C[i+1 mod 3]) : od: ItIsZero(Radius(Ce(P[0],P[1],P[2]))^2-R^2): end: Lehmus:=proc() local N,M,m,n:N:=Pt(y-TS(m,m)*x,y+n*(x-1)): M:=Pt(y-m*x,y+TS(n,n)*(x-1)): ItIsZero(subs(m=n,factor(DeSq([1,0],N)-DeSq([0,0],M)))):end: LehmusConverse:=proc(m,n) local N,M:N:=Pt(y-TS(m,m)*x,y+n*(x-1)): M:=Pt(y-m*x,y+TS(n,n)*(x-1)): factor(DeSq([1,0],N)-DeSq([0,0],M)): end: Lemoine:=proc() local m,n,T,A,B,C,G:T:=Te(m,n):A:=T[1]:B:=T[2]:C:=T[3]:G:= Centroid(T):Concurrent(MirRefLeLe(Le(A,G),y-m*x),MirRefLeLe(Le(B,G),y+n*x-n), MirRefLeLe(Le(C,G),y-C[2]-expand((x-C[1])*TS(m,1/n)))):end: LeonAnne:=proc() local A,B,C,D,O1,l,x1: l:=Le(MidPt(A,C),MidPt(B,D)):O1:=[x1,subs(x=x1,solve(l,y))]: ItIsZero(1/2-(AREA(A,B,O1)+AREA(C,D,O1))/(AREA(A,B,C)+AREA(A,C,D) )):end: #The Morgan generalization of Marion Walter's Theorem MarionMorgan:=proc() local a,b,n,A,B,C,A1,A2,B1,B2,C1,C2,P1,P2,P3,P4,P5,P6: A:=[0,0]: B:=[1,0]: C:=[a,b]: C1:=pmidpt(A,B,n/(2*n+1)):C2:=pmidpt(A,B,(n+1)/(2*n+1)): A1:=pmidpt(B,C,n/(2*n+1)):A2:=pmidpt(B,C,(n+1)/(2*n+1)): B1:=pmidpt(C,A,n/(2*n+1)):B2:=pmidpt(C,A,(n+1)/(2*n+1)): P1:= Pt(Le(A,A1),Le(B,B2)):P2:= Pt(Le(A,A1),Le(C,C2)):P3:=Pt(Le(B,B1),Le(C,C2)): P4:=Pt(Le(B,B1),Le(A,A2)):P5:=Pt(Le(C,C1),Le(A,A2)):P6:=Pt(Le(C,C1),Le(B,B2)): ItIsZero((AREA(P1,P2,P3)+AREA(P1,P3,P4)+AREA(P1,P4,P5)+ AREA(P1,P5,P6))/AREA(A,B,C)-2/(3*n+1)/(3*n+2)): end: MedianTriangleLocus:=proc() local s,p,A,B,C,T,R,P,Q,a,b,c,m,n,gu: T:=AntiMedial(Te(m,n)):A:=T[1]:B:=T[2]:C:=T[3]:R:=Pedal(Te(m,n),Incenter(m,n)): c:=-sqrt(factor(DeSq(A,B))):b:=-sqrt(factor(DeSq(A,C))): a:=sqrt(factor(DeSq(C,B))):s:=normal((a+b+c)/2): P:=[A[1]+(p/c)*(B[1]-A[1]),A[2]+(p/c)*(B[2]-A[2])]:Q:=[A[1]+((s-p)/b)* (C[1]-A[1]),A[2]+((s-p)/b)*(C[2]-A[2])]: gu:=AREA(R[2],R[3],MidPt(P,Q)):gu:=simplify(gu,symbolic):gu:=simplify(gu): ItIsZero(gu):end: Menelaus:=proc() local A,B,C,X,Y,Z,L,m,b: L:=y-m*x-b: X:=Pt(Le(B,C),L): Y:=Pt(Le(A,C),L):Z:=Pt(Le(A,B),L):ItIsZero( DeSq(B,X)*DeSq(C,Y)*DeSq(A,Z)-DeSq(C,X)*DeSq(A,Y)*DeSq(B,Z)): end: Miquel:=proc() local r,A,P,C,t,i,s: print(`This is too big for Maple, so it is here for the future versions`): print(`Meanwhile try MiquelRandom();`): for i from 0 to 3 do A[i]:=ParamCircle([0,0],1,t[i]): od: for i from 0 to 3 do C[i]:=ParPtPerBisect(A[i],A[(i+1) mod 4],s[i]): od: for i from 0 to 3 do P[i]:=MirRefPtLe(A[i],Le(C[(i-1) mod 4],C[i])):od: Concyclic(P[0],P[1],P[2],P[3]):end: MiquelRandom:=proc() local r,A,P,C,t,i,s:print(`This is too big for Maple`): print(`Hence, let's pick random values, giving an empirical proof`): r:=rand(1..1000): for i from 0 to 3 do t[i]:=r():s[i]:=r():od: for i from 0 to 3 do A[i]:=ParamCircle([0,0],1,t[i]): od: for i from 0 to 3 do C[i]:=ParPtPerBisect(A[i],A[(i+1) mod 4],s[i]): od: for i from 0 to 3 do P[i]:=MirRefPtLe(A[i],Le(C[(i-1) mod 4],C[i])):od: print(`Miquel's theorem is (empirically)`):Concyclic(P[0],P[1],P[2],P[3]):end: Monge:=proc() local d1,d2,C1,C3,R1,R2,R3,a,b:d1:=sin1(b)/sin1(a*b): d2:=sin1(a)/sin1(a*b): C1:=[0,0]: C3:=[d1*cos1(a),d1*sin1(a)]: Colinear(TanMt(C1,R1,a,d1,R3),TanMt(C3,R3,1/b,d2,R2),TanMt(C1,R1,1,1,R2)):end: Morley:=proc() local m,n,A,B,C,D,E,F:A:=[0,0]:B:=[1,0]: C:=Pt(y-TS(m,m,m)*x,y+TS(n,n,n)*(x-1)):D:=Pt(y-m*x,y+n*x-n): E:=Pt(y-TS(m,m)*x,y-C[2]-(x-C[1])*TS(m,m,-n,sqrt(3))): F:=Pt(y+TS(n,n)*(x-1),y-C[2]+(x-C[1])*TS(n,n,-m,sqrt(3))):ItIsEqui(D,E,F):end: Nagel:=proc() local m,n,T:T:=Te(m,n):Concurrent( Le(T[1],PtLeCe(Le(T[2],T[3]),Incircle(m,-1/n))), Le(T[2],PtLeCe(Le(T[1],T[3]),Incircle(-1/m,n))), Le(T[3],PtLeCe(Le(T[1],T[2]),Incircle(-1/m,-1/n)))):end: Napoleon:=proc() local A,B,C: ItIsEqui(CET(A,B),CET(B,C),CET(C,A)): end: NinePointCircleExists:=proc() local A,B,C,O,D,E,F,G,H,I1,K,L,M: D:=Ft(A,Le(B,C)):E:=Ft(B,Le(A,C)):F:=Ft(C,Le(A,B)): G:=MidPt(A,B):H:=MidPt(A,C):I1:=MidPt(B,C):O:=Orthocenter(A,B,C): K:=MidPt(O,A):L:=MidPt(O,B):M:=MidPt(O,C):Concyclic(D,E,F,G,H,I1,K,L,M):end: Nobbs:=proc() local m,n,T,S:T:=Te(m,n):S:=Contact(m,n): Colinear(Pt(Le(T[1],T[2]),Le(S[2],S[3])),Pt(Le(T[2],T[3]),Le(S[3],S[1])), Pt(Le(T[3],T[1]),Le(S[1],S[2]))):end: OrthocenterExists:=proc() local A,B,C: Concurrent(Altitude(A,Le(B,C)),Altitude(B,Le(A,C)),Altitude(C,Le(A,B))):end: Pappus:=proc() local t,s,m,b,m1,b1,i,P,Q: for i from 1 to 3 do P[i]:=ParamLine(m,b,t[i]): Q[i]:=ParamLine(m1,b1,s[i]): od: Colinear(Pt(Le(P[1],Q[2]),Le(P[2],Q[1])),Pt(Le(P[1],Q[3]),Le(P[3],Q[1])), Pt(Le(P[2],Q[3]),Le(P[3],Q[2]))):end: Pascal:=proc() local c,d,s,t,i,P,Q: for i from 1 to 3 do P[i]:=ParEllipse( c,d,t[i]):Q[i]:=ParEllipse(c,d,s[i]):od:Colinear(Pt(Le(P[1],Q[2]),Le(P[2],Q[1])), Pt(Le(P[1],Q[3]),Le(P[3],Q[1])),Pt(Le(P[2],Q[3]),Le(P[3],Q[2]))):end: Pivot:=proc() local A,B,C,A1,B1,C1,t1,t2,t3,P1,P2: A:=[0,0]: B:=[1,0]: A1:=[t1*B[1]+(1-t1)*C[1],t1*B[2]+(1-t1)*C[2]]: B1:=[t2*C[1]+(1-t2)*A[1],t2*C[2]+(1-t2)*A[2]]: C1:=[t3*A[1]+(1-t3)*B[1],t3*A[2]+(1-t3)*B[2]]: P1:=OtherCeCe(Ce(A,B1,C1),Ce(B,A1,C1),C1): P2:=OtherCeCe(Ce(B,A1,C1),Ce(C,A1,B1),A1): evalb(normal([expand(P1[1]-P2[1]),expand(P1[2]-P2[2])])=[0,0]): end: Poncelet:=proc() local t0,t1,t2,t3,A,B,C,t,R,Q,Q1,Q2,P,c,L1,L2,L3,eq: L1:=TangentToEllipse([0,0],[1,1],t1):L2:=TangentToEllipse([0,0],[1,1],t2): L3:=TangentToEllipse([0,0],[1,1],t3):L1:=subs(t1=1,L1):A:=Pt(L1,L2): B:=Pt(L1,L3):C:=Pt(L2,L3):R:=Circumradius(A,B,C):c:=Circumcenter(A,B,C): R:=simplify(R,symbolic): P:=ParamCircle(c,R,t0):Q:=ParamCircle(c,R,t): eq:=solve(TouchCeLe1(x^2+y^2-1,Le(P,Q)),t):Q1:=subs(t=eq[1],Q): Q2:=subs(t=eq[2],Q):TouchCeLe(x^2+y^2-1,Le(Q1,Q2)):end: Ptolemy:=proc() local P,i,t,R: for i from 1 to 4 do P[i]:=ParamCircle([0,0],R,t[i]): od: Sqabc(DeSq(P[1],P[2])*DeSq(P[3],P[4]), DeSq(P[2],P[3])*DeSq(P[4],P[1]),DeSq(P[1],P[3])*DeSq(P[2],P[4])):end: Purser:=proc() local r,t1,t2,t3,A,B,C,a,b,c,u,v,t,M,f,X,Y: A:=ParamCircle([0,0],1,t1):B:=ParamCircle([0,0],1,t2): C:=ParamCircle([0,0],1,t3):M:=[1+r,0]:a:=DeSq(B,C):b:=DeSq(A,C):c:=DeSq(A,B): v:=DeSq(C,M)-r^2:u:=DeSq(B,M)-r^2: t:=DeSq(A,M)-r^2: f:=SSR(X,3,Y): evalb(expand(subs({X[1]=a*t,X[2]=b*u,X[3]=c*v,Y=0},f))=0):end: RadicalCenterExists:=proc() local C,R: Concurrent(RadicalLine(C[1],R[1],C[2],R[2]),RadicalLine(C[1],R[1],C[2],R[2]), RadicalLine(C[3],R[3],C[3],R[3])):end: #Sadov's Cubic analog of Ptolemy: (arXiv:math.GM/0410234 v1, 8 Oct. 2004) #if a,b,c,d are the side- #lentghs of a quadrilateral inscribed in a circle, and p,q #are the diagonal lengths, then abp+cdp=bcq+adq Sadov:=proc() local t1,t2,t3,t4,A,B,C,D,a,b,c,d,p,q: A:=ParamCircle([0,0],1,t1): B:=ParamCircle([0,0],1,t2): C:=ParamCircle([0,0],1,t3): D:=ParamCircle([0,0],1,t4): a:=DeSq(A,B):b:=DeSq(B,C):c:=DeSq(C,D): d:=DeSq(D,A):p:=DeSq(A,C):q:=DeSq(B,D): SqRtABCD(a*b*p,c*d*p,b*c*q,a*d*q): end: Simson:=proc() local t,i,P,R:for i from 1 to 4 do P[i]:=ParamCircle([0,0],R,t[i]): od: Colinear(Ft(P[4],Le(P[1],P[2])), Ft(P[4],Le(P[2],P[3])),Ft(P[4],Le(P[3],P[1]))):end: with(grobner): Soddy:=proc() local q,e1,e2,e3,e4,c,d,e,TC,R,r,s,t,p: R:=1:TC:=TcCesOut:c:=[r+R,0]:q:=gbasis({TC(c,r,d,s),TC(c,r,e,t),TC(d,s,e,t), TC([0,0],R,c,r),TC([0,0],R,d,s),TC([0,0],R,e,t)},[d[1],e[1],d[2],e[2],r,s,t], tdeg):e4:=1/R:e1:=1/r:e2:=1/s:e3:=1/t: p:=-2*(e1^2+e2^2+e3^2+e4^2)+(e1+e2+e3+e4)^2:p:=numer(normal(p)): ItIsZero(normalf(p,q,[d[1],e[1],d[2],e[2],r,s,t],tdeg)):end: Thebault:=proc() local m,n,t,p1,p2, I1,T,A,M,eq1,eq2,lu,Ci,Ci1,i,j,SOL,lua: T:=Te(m,n):A:=T[3]:I1:=Incenter(m,n):M:=[t,0]: Ci:=Ce(T): Ci1:=(x-p1)^2+(y-p2)^2-p2^2: eq1:=TouchCe1(Ci1,Ci): lu:=solve(eq1,p2): if subs({m=1/3,n=1/3,t=1/2,p1=1/2},lu[1])>0 then lu:=lu[1]: else lu:=lu[2]: fi: eq2:=TouchCeLe1(Ci1,Le(A,M)): eq2:=numer(normal(subs(p2=lu,eq2))): lua:=solve(eq2,p1): SOL:=[seq([lua[i], subs(p1=lua[i],lu)],i=1..nops([lua]))]: for i from 1 to nops(SOL) do for j from i+1 to nops(SOL) do if Colinear(I1,SOL[i],SOL[j]) then RETURN(true): fi: od: od: false: end: Varignon:=proc() local A,M,i: for i from 0 to 3 do M[i]:= MidPt(A[i],A[i+1 mod 4]) od:ItIsZero(Slope(M[0],M[1])-Slope(M[2],M[3])) and ItIsZero(Slope(M[1],M[2])-Slope(M[3],M[0])):end: Viviani:=proc() local A,B,C,T,P,f,X,Y: T:=Te(1/sqrt(3),1/sqrt(3)): A:=T[1]:B:=T[2]:C:=T[3]:f:=SSR(X,3,Y): ItIsZero(subs({X[1]=DeSq(P,Ft(P,Le(A,B))),X[2]=DeSq(P,Ft(P,Le(A,C))), X[3]=DeSq(P,Ft(P,Le(B,C))),Y=sqrt(DeSq(C,Ft(C,Le(A,B))))},f)):end: vonAubel:=proc() local A,B,C,D,P,Q,R,S: P:=MDOS(A,B):Q:=MDOS(B,C):R:=MDOS(C,D):S:=MDOS(D,A): ItIsZero(Slope(P,R)*Slope(Q,S)+1) and ItIsZero(DeSq(P,R)-DeSq(Q,S)):end: Wittenbauer:=proc() local A,P,l,i: for i from 0 to 3 do l[i]:=Le([(2/3)*A[i][1]+1/3*A[i+1 mod 4][1],(2/3)*A[i][2]+1/3*A[i+1 mod 4][2]], [(2/3)*A[i][1]+1/3*A[i-1 mod 4][1],(2/3)*A[i][2]+1/3*A[i-1 mod 4][2]]):od: for i from 0 to 3 do P[i]:=Pt(l[i],l[i+1 mod 4]): od:evalb(normal( Pt(Le(P[0],P[2]),Le(P[1],P[3])))=normal(CentroidQ(A[0],A[1],A[2],A[3]))):end: ########################PART II:DEFINITIONS########################## #Def (The perpendicular to line Le1 that passes through point Pt1 Altitude:=proc(Pt1,Le1): expand(coeff(expand(Le1),x,1)*(y-Pt1[2])- coeff(expand(Le1),y,1)*(x-Pt1[1])): end: #The triangle whose medial triangle is DEF AntiMedial:=proc(D,E,F) local A,B,C,eq,var:eq:={D[1]=(A[1]+B[1])/2,D[2]= (A[2]+B[2])/2,E[1]=(A[1]+C[1])/2,E[2]=(A[2]+C[2])/2,F[1]=(B[1]+C[1])/2,F[2]= (B[2]+C[2])/2}:var:={A[1],B[1],C[1],A[2],B[2],C[2]}: var:=solve(eq,var): subs(var,[A[1],A[2]]),subs(var,[B[1],B[2]]),subs(var,[C[1],C[2]]):end: #Def(Area of triangle ABC) AREA:=proc(A,B,C):normal(expand((B[1]*C[2]-B[2]*C[1]-A[1]*C[2]+A[2]*C[1] -B[1]*A[2]+B[2]*A[1])/2)):end: #Def The refl. of line L1 through line L2 Billiard:=proc(L1,L2) local gu,L1a,L2a,a,b,c,d,e,f: L1a:=a*x+b*y+c:L2a:=d*x+e*y+f:gu:=BilliardSym(L1a,L2a): subs({a=coeff(expand(L1),x,1),b=coeff(expand(L1),y,1),c=subs(y=0,subs(x=0,L1)), d=coeff(expand(L2),x,1),e=coeff(expand(L2),y,1),f=subs(y=0,subs(x=0,L2))},gu): end: #Def (The refl. of gen. line L1 through gen. line L2) BilliardSym:=proc(L1,L2) local P,m,n,sl: m:=-coeff(L1,x,1)/coeff(L1,y,1):n:=-coeff(L2,x,1)/coeff(L2,y,1): P:=Pt(L1,L2): sl:=TS(n,n,-m):numer(normal((y-P[2])-sl*(x-P[1]))):end: #Def (The Circumcircle of the inputed Points) Ce:=proc() local eq,a,b,c,i,q:eq:=x^2+y^2+a*x+b*y+c:q:=solve({seq(subs( {x=args[i][1],y=args[i][2]},eq),i=1..nargs)} ,{a,b,c}):expand(subs(q,eq)):end: #Def(The Center of a Circle Circ) Center:=proc(Circ): normal([-coeff(expand(Circ),x,1)/2,-coeff(expand(Circ),y,1)/2]):end: #Def (The intersection of the three medians) Centroid:=proc(A,B,C):Concurrency(Le(MidPt(A,B),C),Le(MidPt(A,C),B), Le(MidPt(B,C),A)):end: #The centroid of the quadrilateral ABCD CentroidQ:=proc(A,B,C,D) local P,Q,a,b:P:=Centroid(A,B,C):Q:=Centroid(A,C,D): a:=AREA(A,B,C): b:=AREA(A,C,D): [a/(a+b)*P[1]+b/(a+b)*Q[1],a/(a+b)*P[2]+b/(a+b)*Q[2]]:end: #Def(Circumcenter of the equilateral triangle two of whose vertices are A and B) CET:=proc(A,B):Circumcenter(A, B, [(B[1]+A[1])/2-(A[2]-B[2])*3^(1/2)/2, B[2]/2+(A[1]-B[1])*3^(1/2)/2+A[2]/2]):end: #Def (The Circumcenter of the triangle ABC) Circumcenter:=proc(A,B,C):Center(Ce(A,B,C)):end: #Def (Circumradius of the triangle ABC) Circumradius:=proc(A,B,C):radsimp(Radius(Ce(A,B,C))):end: #Def (The inputed points all on the same line?) Colinear:=proc() local i: if nargs<2 then ERROR(`Need at least two Pts`): fi: for i from 3 to nargs do if AREA(args[1],args[2],args[i])<>0 then RETURN(false):fi:od:true:end: #Length of a common tangent to the circles centered C1(C2) with radius R1(R2) ComTangLgtSq:=proc(C1,R1,C2,R2) local a,d:d:=sqrt(DeSq(C1,C2)):a:=d*R2/(R1-R2): sqrt((d+a)^2-R1^2)-sqrt(a^2-R2^2):end: #Def (Are the inputed points all on the same circle?) Concyclic:=proc() local i,C1:C1:=Ce(args[1],args[2],args[3]): for i from 4 to nargs do if not ItIsZero(C1-Ce(args[1],args[2],args[i])) then RETURN(false): fi: od: true: end: #Def (The common point of the inputed lines) Concurrency:=proc() local q: q:=solve({args},{x,y}):[subs(q,x),subs(q,y)]: end: #Def (Are the inputed lines concurrent?) Concurrent:=proc(): not evalb(solve({args},{x,y})=NULL): end: #Def (the distance between point A and point B) (use with caution) De:=proc(A,B):sqrt(DeSq(A,B)):end: #Def (Square of Distance of point P to line L) DePtLeSq:=proc(P,L):DeSq(Pt(Altitude(P,L),L),P):end: #Def (The square of the distance of points A and B) DeSq:=proc(A,B):(A[1]-B[1])^2+(A[2]-B[2])^2: end: #Def (The square of the distance of points A and B, in dim-dimensional space) DeSqG:=proc(A,B,dim) local i :sum((A[i]-B[i])^2,i=1..dim): end: #Def(Excircles of standard triangle Te(m,n) Excircles:=proc(m,n) local C,T,a,b,c,gu,i: T:=Te(m,n):C:=x^2+y^2+a*x+b*y+c: gu:=solve({TouchCeLe1(C,Le(T[1],T[2])),TouchCeLe1(C,Le(T[1],T[3])), TouchCeLe1(C,Le(T[2],T[3]))},{a,b,c}): {seq(subs(gu[i],C),i=1..nops([gu]))} minus {Incircle(m,n)}:end: #Def (The line through Circumcenter, Orthocenter, and Centroid) EulerLine:=proc(A,B,C):Le(Orthocenter(A,B,C),Circumcenter(A,B,C)):end: #Def (Projection of point Pt1 on line Le1) Ft:=proc(Pt1,Le1) :Pt(Altitude(Pt1,Le1),Le1):end: #Def (Gergonne Point of Standard Triangle Te(m,n)) GergonnePt:=proc(m,n) local T,C1:T:=Te(m,n):C1:=Incircle(m,n): Pt(Le(T[1],PtLeCe(Le(T[2],T[3]),C1)),Le(T[2],PtLeCe(Le(T[1],T[3]),C1))):end: #Def(The incenter of the triangle whose vertices are A(0,0), B(1,0), #and the slopes of AB and BC are TS(m,m),TS(n,n),resp.) Incenter:=proc(m,n) local C: C:=Te(m,n)[3]: if m=n then [1/2,m/2] :else Concurrency(y-m*x,y+n*x-n,y-C[2]-expand((x-C[1])*TS(m,1/n))) fi:end: #Def: The eq. of the incircle through the standard triangle Incircle:=proc(m,n) local C,R:R:=Inradius(m,n):C:=Incenter(m,n): expand((x-C[1])^2+(y-C[2])^2-R^2):end: #Def(The inradius of the standard triangle ) Inradius:=proc(m,n) local A,B,C,T,O: T:=Te(m,n):A:=T[1]:B:=T[2]:C:=T[3]:O:=Incenter(m,n): radsimp(sqrt(normal({DePtLeSq(O,Le(A,B)),DePtLeSq(O,Le(A,C)),DePtLeSq(O,Le(B,C))})[1])): end: #Def(Is the triangle ABC equilateral?) ItIsEqui:=proc(A,B,C):evalb(normal ({DeSq(A,B)-DeSq(A,C),DeSq(B,C)-DeSq(C,A)})={0}):end: #Def(Is it zero?) ItIsZero:=proc(a):evalb(normal(a)=0):end: #Kiss(Pt1,Pt2,Ce1): The point P, that lies on Ce1, and such that #the Circle through Pt1,Pt2,P touches Ce1 at P Kiss:=proc(Pt1,Pt2,Ce1) local x1,y1,gu1,gu2,lu,Pt3: gu1:=Tangent(Ce1,[x1,y1]):gu2:=Tangent(Ce(Pt1,Pt2,[x1,y1]),[x1,y1]): lu:=solve({subs({x=x1,y=y1},Ce1),coeff(gu2,x,1)*coeff(gu1,y,1)- coeff(gu1,x,1)*coeff(gu2,y,1)},{x1,y1}): Pt3:=subs(lu[1],[x1,y1]): if not Colinear(Pt1,Pt2,Pt3) then RETURN(Pt3): else RETURN(subs(lu[2],[x1,y1])): fi: end: #Def (The eq. of the line joining A and B) Le:=proc(A,B) AREA(A,B,[x,y]):end: #MDOS(A,B): The point where the diagonals of the Outside Square on AB meet MDOS:=proc(A,B) local a,b: a:=B[1]-A[1]:b:=B[2]-A[2]: Pt(Le(A,[A[1]+a+b,A[2]+b-a]),Le(B,[A[1]+b,A[2]-a])):end: #Def (The midpoint between A and B) MidPt:=proc(A,B):[(A[1]+B[1])/2,(A[2]+B[2])/2]:end: #Def (Mirror reflection of line l1 w.r.t. line l MirRefLeLe:=proc(l1,l) local O,P: O:=Pt(l,l1):P:=[1,solve(subs(x=1,l1),y)]: Le(O,MirRefPtLe(P,l)):end: #Def (Mirror reflection of the origin w.r.t. to the line AB) MirRefOf0:=proc(A,B) local q: q:=Ft([0,0],Le(A,B)): [2*q[1],2*q[2]]:end: #Def (Mirror reflection of the point P w.r.t. to the line l) MirRefPtLe:=proc(P,l) local q: q:=Ft([0,0],subs({x=x+P[1],y=y+P[2]},l)): [2*q[1]+P[1],2*q[2]+P[2]]:end: #Def (the reflection of the point P1 w.r.t. the point P2 MirRefPtPt:=proc(P1,P2): normal([P2[1]-(P1[1]-P2[1]),P2[2]-(P1[2]-P2[2])]):end: #Def(Nagel Point of the standard triangle Te(m,n)) NagelPt:=proc(m,n) local T:T:=Te(m,n):Pt(Le(T[1],PtLeCe(Le(T[2],T[3]), Incircle(m,-1/n))),Le(T[2],PtLeCe(Le(T[1],T[3]),Incircle(-1/m,n)))):end: #Def (Euler's Nine-point circle for triangle ABC) NinePointCircle:=proc(A,B,C): Ce(MidPt(A,B),MidPt(A,C),MidPt(B,C)):end: #Def(Normal to the parametric ellipse at the parametric point NormalToEllipse:=proc(c,d,t) local P: P:=ParEllipse(c,d,t): diff(P[2],t)*(y-P[2])+diff(P[1],t)*(x-P[1]):end: #Def (The intersection of the three perpendicular projections) Orthocenter:=proc(A,B,C):Concurrency(Altitude(A,Le(B,C)),Altitude(B,Le(A,C)), Altitude(C,Le(A,B))):end: #OtherCeCe(C1,C2,P): The other meeting Pt of two circles C1,C2 meet at the P OtherCeCe:=proc(C1,C2,P) if normal(subs({x=P[1],y=P[2]},C1))<>0 or normal(subs({x=P[1],y=P[2]},C2))<>0 then ERROR(`The circles do not meet at`, P) : fi: MirRefPtLe(P,Le(Center(C1),Center(C2))):end: #Def (Generic point on a Parametric circle center [c[1],c[2]] and radius R) ParamCircle:=proc(c,R,t):[c[1]+R*(t+1/t)/2,c[2]+R*(t-1/t)/2/I]:end: #Def (Generic point on a parametric line) ParamLine:=proc(m,b,t):[t,m*t+b]:end: #Def (Generic point on a Parametric ellipse, center [c[1],c[2]]) ParEllipse:=proc(c,d,t):[c[1]+d[1]*(t+1/t)/2,c[2]+d[2]*(t-1/t)/2/I]:end: #Parametric Point on the Perpendicular Bisector of AB ParPtPerBisect:=proc(A,B,s)local M:M:=MidPt(A,B):[M[1]+s,M[2]-s/Slope(A,B)]:end: #The Pedal Triangle of the Triangle ABC w.r.t to pt P Pedal:=proc(A,B,C,P) Ft(P,Le(A,B)),Ft(P,Le(A,C)),Ft(P,Le(B,C)): end: #Def(Line through Midpoint of PQ perpendicular to PQ) PerpMid:=proc(P,Q):PerpPQ(P,MidPt(P,Q)):end: #Def(Line through Q perpendicular to PQ) PerpPQ:=proc(P,Q):expand((y-Q[2])*(P[2]-Q[2])+(x-Q[1])*(P[1]-Q[1])):end: #Def(Point between A and B that is the `p-point') pmidpt:=proc(A,B,p): normal([A[1]+p*(B[1]-A[1]),A[2]+p*(B[2]-A[2])]):end: #Def( Power of pt Pt w.r.t. circle with Center C and radius R) Powe:=proc(C,R,Pt):DeSq(C,Pt)-R^2:end: #Def (The point of intersection of lines Le1 and Le2) Pt:=proc(Le1,Le2) local q:q:=solve( {numer(normal(Le1)),numer(normal(Le2))},{x,y}): [normal(simplify(subs(q,x))),normal(simplify(subs(q,y)))]:end: #Def(The common point of a circle and a line that touches it) PtLeCe:=proc(L1,C1):normal(subs(solve({L1,C1},{x,y}),[x,y])):end: #Def(Quadrilateral through four lines L1,L2,L3,L4) Quad:=proc(L1,L2,L3,L4):Pt(L1,L2),Pt(L2,L3),Pt(L3,L4),Pt(L4,L1):end: #Def (the radical center of circles with centers (radiii) C1,C2,C3,R1,R2,R3 RadicalCenter:=proc(C1,R1,C2,R2,C3,R3) local C,R: Pt(RadicalLine(C1,R1,C2,R2),RadicalLine(C1,R1,C3,R3)):end: #Def( Radical line of circles with Centers C1,C2 and Radii R1, R2 RadicalLine:=proc(C1,R1,C2,R2):expand(Powe(C1,R1,[x,y])-Powe(C2,R2,[x,y])): end: #Def(The Radius of a circle Circ) Radius:=proc(Circ) local q: q:=Center(Circ):radsimp(sqrt(normal(subs({x=q[1],y=q[2]},-Circ)))):end: #Def (The slope of the line joining points A and B) Slope:=proc(A,B):normal((B[2]-A[2])/(B[1]-A[1])):end: #Def( Is it true that sqrt(a)+sqrt(b)=sqrt(c) ?) Sqabc:=proc(a,b,c):ItIsZero((c-a-b)^2-4*a*b):end: #is it true that sqrt(A)+sqrt(B)=sqrt(C)+sqrt(D) SqRtABCD:=proc(A,B,C,D): evalb(expand(expand(((A+B-C-D)^2-4*(A*B+C*D))^2-64*A*B*C*D))=0): end: #SSR(A,n,B): the polynomial in A[1], ..., A[n], B #whose vanishing is equivalent to B equaling the sum #of the square roots of A[1],..., A[n] SSR:=proc(A,n,B) local gu,x,i,d:if n=1 then RETURN(B^2-A[1]): fi:gu:= expand(subs(B=B-x,SSR(A,n-1,B))):d:=degree(gu,x)/2:expand(sum(coeff(gu,x,2*i)* A[n]^i,i=0..d)^2-A[n]*sum(coeff(gu,x,2*i+1)*A[n]^i,i=0..d)^2):end: #SSR1(A,B): given a list A returns true if B is the sum #(of one of the possibilities of sums of square roots of #the elements of A SSR1:=proc(A,B) local gu,i,j,mu,lu: gu:={0}: for i from 1 to nops(A) do mu:={}: lu:=simplify(sqrt(A[i])): for j from 1 to nops(gu) do mu:=mu union {gu[j]+lu,gu[j]-lu}: od:gu:=mu:od: for i from 1 to nops(gu) do if expand(simplify(simplify(expand(gu[i]^2-B^2),symbolic)))= 0 then RETURN(true):fi:od:false:end: #Tangent(Ce1,Pt1): Given a circle Ce1, and a point Pt1 #on it, finds the equation of the tangent Tangent:=proc(Ce1,Pt1) local A,x0,y0: A:=coeff(Ce1,x,2):x0:=Pt1[1]: y0:=Pt1[2]: numer(normal((y-y0)*(2*A*y0+coeff(Ce1,y,1))+(x-x0)*(2*A*x0+coeff(Ce1,x,1)))): end: #Def(Tangent to the parametric ellipse at the parametric point TangentToEllipse:=proc(c,d,t) local P: P:=ParEllipse(c,d,t): diff(P[1],t)*(y-P[2])-(x-P[1])*diff(P[2],t):end: #TanMt(C1,R1,m,d,R2): Intersection of common Tangents of Circle1 #with center C1 and radius R1 and Cirlce2 with center C2,distance d from C1 #such that slope(C1,C2) is tan1(b) TanMt:=proc(C1,R1,b,d,R2) local a: a:=d/(R2/R1-1):[C1[1]-a*cos1(b),C1[2]-a*sin1(b)]:end: #Def: The condition that two circles, with given centers and radii touch TcCesOut:= proc(C1,R1,C2,R2):expand((R1+R2)^2-(C1[1]-C2[1])^2-(C1[2]-C2[2])^2):end: #Def(Standard Triangle whose vertices are A(0,0),B(1,0) and angles #CAB and CBA are 2*arctan(m) and 2*arctan(-n) resp. Te:=proc(m,n):[0,0],[1,0],Pt(y-TS(m,m)*x,y+TS(n,n)*(x-1)):end: #Def(Given two circles C1,C2, decides whether they touch) TouchCe:=proc(C1,C2) local gu: gu:=expand(subs(y=solve(C1-C2,y),C1)): ItIsZero(4*coeff(gu,x,2)*coeff(gu,x,0)-coeff(gu,x,1)^2): end: #Def(The expression whose vanishing guarantess that the symbolic #circles touch) TouchCe1:=proc(C1,C2) local gu: gu:=expand(subs(y=solve(C1-C2,y),C1)): numer(normal(4*coeff(gu,x,2)*coeff(gu,x,0)-coeff(gu,x,1)^2)): end: #Def(Given a circle C1, and a line L1, decides whether they touch) TouchCeLe:=proc(C1,L1) local gu: gu:=expand(subs(y=solve(L1,y),C1)): ItIsZero(4*coeff(gu,x,2)*coeff(gu,x,0)-coeff(gu,x,1)^2): end: #Def(The expression whose vanishing guarantess that the symbolic #circle C1 and Line L1 touch) TouchCeLe1:=proc(C1,L1) local gu: gu:=expand(subs(y=solve(L1,y),C1)): numer(normal(4*coeff(gu,x,2)*coeff(gu,x,0)-coeff(gu,x,1)^2)): end: #Def:tan(a_1+a_2+...) expressed in terms li[1]:=tan(a_1), li[2]:=tan(a_2) .. TS:=proc(li) local i,t:if nargs=1 then RETURN(args[1]) else t:=TS(seq(args[i],i=2..nargs)): RETURN((args[1]+t)/(1-t*args[1])):fi:end: ###################MONTHLY PROBLEMS############################ #Monthly Problem Problem 10637 by C.F. Parry P10637:=proc() local A,B,C,a,b,O1,H,alp,bet,gam,alp1,bet1,gam1,EL,m,P: A:=[0,0]: B:=[1,0]: C:=[a,b]: O1:=Circumcenter(A,B,C):H:=Orthocenter(A,B,C): m:=Slope(O1,H):alp:=y-A[2]-m*(x-A[1]):bet:=y-B[2]-m*(x-B[1]): gam:=y-C[2]-m*(x-C[1]): alp1:=Billiard(alp,Le(B,C)):bet1:=Billiard(bet,Le(C,A)): gam1:=Billiard(gam,Le(A,B)):Concurrent(alp1,bet1,gam1):P:=Concurrency (alp1,bet1,gam1):Concurrent(alp1,bet1,gam1) and ItIsZero(DeSq(O1,P)-4*Circumradius(A,B,C)^2):end: #Monthly Problem Problem 10673 by Mazur P10673:=proc() local m,n,C,s1,s2,T,t1,t2,t3,A1,A2,A3,F1,F2,F3,P1,P2,P3,F1a,F2a,F3a: T:=Te(m,n):C:=Incenter(m,n):A1:=T[1]:A2:=T[2]:A3:=T[3]: F3:=Ft(C,Le(A1,A2)):F2:=Ft(C,Le(A1,A3)):F1:=Ft(C,Le(A2,A3)): P1:=[A2[1]+s1*(A2[1]-A3[1]),A2[2]+s1*(A2[2]-A3[2])]: P2:=[A1[1]+s2*(A3[1]-A1[1]),A1[2]+s2*(A3[2]-A1[2])]: P3:=Pt(Le(Pt(Le(P1,A1),Le(P2,A2)),A3),Le(A1,A2)): F3a:=MirRefPtLe(F3,expand(Le(C,P3))): F2a:=MirRefPtLe(F2,expand(Le(C,P2))): F1a:=MirRefPtLe(F1,expand(Le(C,P1))): t1:=Le(P1,F1a):t2:=Le(P2,F2a):t3:=Le(P3,F3a): Colinear(Pt(t1,Le(P2,P3)),Pt(t2,Le(P3,P1)),Pt(t3,Le(P1,P2))): end: #Monthly Problem P10678, Aug./Sep. 1998, proposed by Clark #Kimberling and Peter Yff P10678:=proc() local m,n,T,Ce1,A1,A2,A3,B1,B2,B3: T:=Te(m,n): Ce1:=Incircle(m,n):A1:=T[1]:A2:=T[2]:A3:=T[3]: B3:=Kiss(A1,A2,Ce1):B2:=Kiss(A1,A3,Ce1):B1:=Kiss(A2,A3,Ce1): Concurrent(Le(A1,B1),Le(A2,B2),Le(A3,B3)): end: sin1:=proc(a):(a-1/a)/I/2:end:cos1:=proc(a):(a+1/a)/2:end: tan1:=proc(a):sin1(a)/cos1(a):end: #Monthly Problem P10693, Nov. 1998, proposed by Wu Wei Chao P10693:=proc() local a,b,c, AB,BP,Q,R,D,PC,D1,Q1,R1: AB:=sin1(b^2)/sin1(a^2*b^2):BP:=sin1(a^2*c^2)*AB/sin1(c^2):PC:=1-BP: D:=[Incenter(tan1(a),tan1(b))[1],0]:Q:=Incenter(tan1(a),tan1(c)): Q:=[BP*Q[1],BP*Q[2]]:R:=Incenter(1/tan1(c),tan1(b)):R:=[BP+PC*R[1],PC*R[2]]: D1:=[Incenter(-1/tan1(a),-1/tan1(b))[1],0]:Q1:=Incenter(-1/tan1(a),-1/tan1(c)): Q1:=[BP*Q1[1],BP*Q1[2]]:R1:=Incenter(-tan1(c),-1/tan1(b)): R1:=[BP+PC*R1[1],PC*R1[2]]:evalb(normal(Slope(R,D)*Slope(Q,D))=-1 and nops(normal({DeSq(Q,D)/DeSq(R1,D1),DeSq(D,R)/DeSq(D1,Q1), DeSq(R,Q)/DeSq(Q1,R1)}))=1 and Concurrent(y,Le(Q,R),Le(Q1,R1))): end: #Monthly Problem P10703, Dec. 1998, proposed by Jean Anglesio P10703:=proc() local m,n,T,I1,C1,O1,H1,W1,G1,N1,S1,T1,U1,V1: T:=Te(m,n):I1:=Incenter(m,n):C1:=Centroid(T):O1:=Circumcenter(T): H1:=Orthocenter(T):W1:=Center(NinePointCircle(T)):G1:=GergonnePt(m,n): N1:=NagelPt(m,n):S1:=Pt(Le(I1,G1),Le(O1,C1)):T1:=Pt(Le(I1,G1),Le(O1,N1)): U1:=Pt(Le(I1,G1),Le(W1,N1)):V1:=Pt(Le(I1,G1),Le(H1,N1)): [ItIsZero(normal(DeSq(C1,H1)/DeSq(H1,S1)-1/9)), [ItIsZero(normal(DeSq(S1,T1)/DeSq(S1,I1)-(10/15)^2)), ItIsZero(normal(DeSq(S1,T1)/DeSq(S1,U1)-(10/18)^2)), ItIsZero(normal(DeSq(S1,T1)/DeSq(S1,V1)-(10/30)^2))], [ItIsZero(normal(DeSq(N1,O1)/DeSq(T1,O1)-(3/1)^2)), ItIsZero(normal(DeSq(N1,W1)/DeSq(U1,W1)-(5/3)^2)), ItIsZero(normal(DeSq(N1,H1)/DeSq(V1,H1)-1))]]:end: #Monthly Problem P10710, Jan. 1999, proposed by Bogdan Suceava P10710:=proc() local m,n,T,A,B,C,D,E,F,I1,M,N,P,Q:T:=Te(m,n):A:=T[1]: B:=T[2]: C:=T[3]:I1:=Incenter(m,n):D:=Ft(I1,Le(B,C)):E:=Ft(I1,Le(A,C)): F:=Ft(I1,Le(A,B)): M:=Pt((y-A[1])-Slope(B,C)*(x-A[2]),Le(D,E)):N:=Pt((y-A[1])-Slope(B,C)*(x-A[2]), Le(D,F)):P:=MidPt(D,M):Q:=MidPt(D,N):Concyclic(A,E,F,I1,P,Q):end: #Monthly Problem 10734, proposed by Floor van Lamoen, May 1999 P10734:=proc() local m,n,T,SL,A,B,C,H,I1,O,AB,AC,BC: T:=Te(m,n):A:=T[1]: B:=T[2]: C:=T[3]: AB:=sqrt(DeSq(A,B)):AC:=-simplify(sqrt(DeSq(A,C)),symbolic): BC:=-simplify(sqrt(DeSq(B,C)),symbolic): H:=Orthocenter(T):I1:=Incenter(m,n): O:=Circumcenter(T): evalb(RadicalCenter(A,AC+AB,B,AB+BC,C,BC+AC)= MirRefPtPt(MirRefPtPt(H,O),I1)):end: #Monthly Problem 10749, proposed by Alain Grigis, Aug.-Sep. 1999 P10749:=proc() local A,B,C,p,P,Q,R,S,X,p0: B:=[0,0]: A:=[sqrt(3),0]: C:=[0,1]: P:=[0,p]: Q:=Pt(Billiard(Le(A,P),Le(B,C)),Le(A,C)): R:=Pt(Billiard(Le(P,Q),Le(A,C)),Le(A,B)): S:=Pt(Billiard(Le(Q,R),Le(A,B)),Le(A,C)): p0:=solve(normal(subs({x=0,y=0},Billiard(Le(R,S),Le(A,C)))/p),p): P:=subs(p=p0,P):Q:=subs(p=p0,Q):R:=subs(p=p0,R):S:=subs(p=p0,S): X:=Concurrency(Le(A,P),Le(Q,R),Le(S,B) ): evalb( Concurrent(Le(A,P),Le(Q,R),Le(S,B)) and Slope(B,X)=sqrt(3)/2 and Slope(X,S)=sqrt(3)/2 and simplify(De(A,X)-De(X,P)-De(P,Q)-De(Q,X))=0 and simplify(De(A,X)-De(X,R)-De(R,S)-De(S,X))=0 and simplify(De(A,X)-2*De(X,B))=0) end: # P10780a(m,n,r,Base): Proves that # The radius of the partner of the circle # of radius r touching the sides CA and AB in the triangle # ABC where length(AB)=Base, and angle CAB=2*arctan(m) # and angle ABC=2*arctan(n) equals # R:=(-n/m)*r+(n/(1-n*m))*Base: P10780a:=proc() local m,n,r,P1,P2,C,Cir1,Cir2,Li,gu1,gu2,m1,R: R:=(-n/m)*r+n/(1-n*m): P1:=[r/m,r]: P2:=[1-R/n, R]:C:=Te(m,n)[3]: Li:=(y-C[2])-(x-C[1])*m1: Cir1:=expand((x-P1[1])^2+(y-P1[2])^2-P1[2]^2): Cir2:=expand((x-P2[1])^2+(y-P2[2])^2-P2[2]^2): evalb(solve(TouchCeLe1(Cir1,Li)/(m1-TS(m,m)),m1)= solve(TouchCeLe1(Cir2,Li)/(m1-TS(-n,-n)),m1)); end: #Monthly Problem 10780*, proposed by Kiran Kedlaya, Jan. 2000 P10780:=proc() local f,m,n,k,r,T,BC,CA,lu: print(`This solution is dedicated to the memory of Rodica Simion`): lprint(``): lprint(``): #The line below is verified by P10780a(); f:=(m,n,r,C)->normal((-n/m)*r+(n/(1-n*m))*C): T:=Te(m,n): k:=1/TS(m,n): BC:=sqrt(factor(DeSq(T[2],T[3]))):CA:=sqrt(factor(DeSq(T[3],T[1]))): lu:=f(m,n,r,1);lu:=f(n,k,lu,BC);lu:=f(k,m,lu,CA);lu:=f(m,n,lu,1); lu:=f(n,k,lu,BC);lu:=f(k,m,lu,CA);evalb(lu=r):end: #Monthly Problem 10783, proposed by Wu Wei Chao, Feb. 2000 P10783:=proc() local t2,t3,t4,A,B,C,D,E,F,G,H,m,n: A:=ParamCircle([0,0],1,1):B:=ParamCircle([0,0],1,t2): C:=ParamCircle([0,0],1,t3):D:=ParamCircle([0,0],1,t4): E:=[m*C[1]+(1-m)*D[1],m*C[2]+(1-m)*D[2]]: F:=[n*C[1]+(1-n)*D[1],n*C[2]+(1-n)*D[2]]: G:=Circumcenter(B,C,E):H:=Circumcenter(A,D,F): F:=subs(n=solve(AREA(Pt(Le(A,B),Le(C,D)),G,H),n),F): evalb(Ce(A,B,E)=Ce(A,B,F)):end: #Monthly Problem 10796, proposed by Floor van Lamoen, April 1999 P10796:=proc() local A,B,C,D,A1,B1,C1: A:=[0,0]:B:=[1,0]: A1:=Ft(A,Le(B,C)):B1:=Ft(B,Le(A,C)):C1:=Ft(C,Le(A,B)): D:=Concurrency(EulerLine(A,B1,C1),EulerLine(A1,B,C1),EulerLine(A1,B1,C)): ItIsZero(subs({x=D[1],y=D[2]},NinePointCircle(A,B,C))): end: #Monthly Problem 10804, proposed by Achilleas Sinefakopoulos, May 2000 P10804:=proc() local A,B,C,D,t,L,P,E,F,i,lu1,lu2: for i from 1 to 4 do P[i]:=ParEllipse([0,0],[1,1],t[i]): L[i]:=TangentToEllipse([0,0],[1,1],t[i]):od: A:=Pt(L[1],L[2]):B:=Pt(L[2],L[3]): C:=Pt(L[3],L[4]):D:=Pt(L[4],L[1]): E:=P[2]:F:=P[4]: lu1:=factor(numer(normal(Ce(A,B,C)-Ce(A,B,D)))): lu2:=factor(numer(normal(DeSq(A,E)/DeSq(E,B)-DeSq(D,F)/DeSq(F,C)))): evalb({solve(lu1,t[3])} intersect {solve(lu2,t[3])} minus {t[1]}<>{}):end: #Monthly Problem 10810 (June-July 2000), proposed by J.-B. Romero Marquez P10810:=proc()local A,B,C,D,JB: JB:=proc(A,B,C,D) local A1,B1: A1:=Pt((y-B[2])-Slope(C,D)*(x-B[1]),Le(A,D)): B1:=Pt((y-A[2])-Slope(D,C)*(x-A[1]),Le(B,C)): Pt(Le(A,B),Le(A1,B1)): end: A:=[0,0]: B:=[1,0]: evalb(Slope(JB(A,B,C,D),JB(B,C,D,A))=Slope(JB(C,D,A,B),JB(D,A,B,C))): end: #Monthly Problem 10845, Jan. 2001,proposed by Ciprian Demeter P10845:=proc() local A,B,C,a,b,c,T,T1,IntBisA,ExtBisA,m,n,E,F,G: m:=TS(a,c): n:=TS(b,c):T:=Te(m,n):T1:=Te(a,b): B:=T[1]: A:=T[2]:C:=T[3]:E:=T1[2]: IntBisA:=y-A[2]-expand((x-A[1])*TS(m,1/n)): ExtBisA:=x-A[1]+expand((y-A[2])*TS(m,1/n)): F:=Ft(E,IntBisA):G:=Ft(E,ExtBisA): Colinear(F,G,MidPt(B,C)): end: #Montly Problem 10874, May 2001, proposed by Wu Wei Chao P10874:=proc() local a,b,c,d,A,B,C,D1,P,U,V: A:=ParEllipse([0,0],[1,1],a): B:=ParEllipse([0,0],[1,1],b): C:=ParEllipse([0,0],[1,1],c):D1:=ParEllipse([0,0],[1,1],d): P:=Pt(Le(A,C),Le(B,D1)):U:=Circumcenter(A,P,B):V:=Circumcenter(C,P,D1): evalb(Slope([0,0],U)=Slope(P,V) and Slope([0,0],V)=Slope(U,P)), factor(AREA([0,0],U,V))=0: end: #Montly Problem 11554, Feb. 2011, proposed by Zhang Yun P11554:=proc() local T,I1,m,n: T:=Te(m,n): I1:=Incenter(m,n): Concurrent( Le(MirRefPtLe(I1,Le(T[2],T[3])),T[1]), Le(MirRefPtLe(I1,Le(T[1],T[3])),T[2]), Le(MirRefPtLe(I1,Le(T[1],T[2])),T[3]) ): end: ############END OF MONTHLY PROBLEMS##################################### #############IMO PROBLEMS############################## I78_4:=proc() local m,T,B,C,A,D,P,Q,Ce1,Ce2,t,lu,M,J,i: T:=Te(m,m):B:=T[1]: C:=T[2]:A:=T[3]:P:=[B[1]+t*(A[1]-B[1]),B[2]+t*(A[2]-B[2])]: Q:=[C[1]+t*(A[1]-C[1]),B[2]+t*(A[2]-C[2])]:D:=Pt(PerpPQ(A,P),PerpPQ(A,Q)): J:=Incenter(m,m):Ce1:=Ce(A,B,C):Ce2:=expand((x-D[1])^2+(y-D[2])^2-DeSq(D,P)): lu:={solve(TouchCe1(Ce1,Ce2),t)}: M:=MidPt(P,Q): member(J,{seq(normal(subs(t=lu[i],M)),i=1..nops(lu))}):end: I79_3:=proc() local t,P,Q,lu,t1,t2: P:=t->[cos(t),sin(t)]: Q:=proc(t):evalc(1-R*exp(-t0*I)+R*exp(I*(t-t0))):[coeff(",I,0),coeff(",I,1)]: end:evalb(diff(Pt(PerpMid(P(t1),Q(t1)),PerpMid(P(t2),Q(t2))),t1)=0):end: I82_2:=proc() local m,n,T,A1,A2,A3,D,M1,M2,M3,T1,T2,T3,S1,S2,S3: T:=Te(m,n): A1:=T[1]:A2:=T[2]:A3:=T[3]: D:=Incenter(m,n):M1:=MidPt(A2,A3):M2:=MidPt(A1,A3):M3:=MidPt(A1,A2): T1:=Ft(D,Le(A2,A3)):T2:=Ft(D,Le(A1,A3)):T3:=Ft(D,Le(A1,A2)): S1:=MirRefPtLe(T1,y-m*x):S2:=MirRefPtLe(T2,y+n*x-n): S3:=MirRefPtLe(T3,y-A3[2]-expand((x-A3[1])*TS(m,1/n))): Concurrent(Le(M1,S1),Le(M2,S2),Le(M3,S3)):end: I82_5:=proc() local A,B,C,D,E,F,P,i,gu,M,N,r: for i from 0 to 5 do gu:=evalc(exp(i*2*Pi*I/6)): P[i]:=[coeff(gu,I,0),coeff(gu,I,1)]: od: A:=P[0]:B:=P[1]:C:=P[2]:D:=P[3]:E:=P[4]:F:=P[5]: M:=[A[1]+r*(C[1]-A[1]),A[2]+r*(C[2]-A[2])]: N:=[C[1]+r*(E[1]-C[1]),C[2]+r*(E[2]-C[2])]:solve(AREA(B,M,N),r):end: #######################END#################### #####Ancestors ##Fathers of Theorems ABBA[AreaFormula]:={ItIsZero,DeSq,AREA}: ABBA[Bretschneider]:={ItIsZero,DeSq,AREA}: ABBA[Brianchon]:={ TangentToEllipse,Pt,Concurrent,Le}: ABBA[Butterfly]:={ParamCircle,Pt,Le,PerpPQ,DeSq,ItIsZero}: ABBA[Carnot]:={Te,SSR1,Circumcenter,Ft,Le,ItIsZero,DeSq,Circumradius,Inradius}: ABBA[Casey]:={ParamCircle,ComTangLgtSq,ItIsZero}: ABBA[CentroidExists]:={Concurrent,Le,MidPt,Le}: ABBA[Ceva]:={Pt,Le,ItIsZero,DeSq}: ABBA[Clifford]:={OtherCeCe}: ABBA[deLongchamps]:={Circumcenter,Orthocenter,EulerLine,ItIsZero}: ABBA[Desargues]:={ParamLine,Colinear,Pt,Le}: ABBA[EightPointCircleExists]:={MidPt,Concyclic,Ft,Le}: ABBA[EulerLineExists]:={Colinear,Orthocenter,Circumcenter,Centroid}: ABBA[EulerTetrahedronVolumeFormula]:={DeSqG,AREA}: ABBA[EulerTriangleFormula]:= {Te,Incenter,Circumcenter,Inradius,Circumradius,DeSq,ItIsZero}: ABBA[Feuerbach]:={TouchCe,NinePointCircle,Te,Incircle}: ABBA[FeuerbachConic]:={NinePointCircle,Te,Orthocenter,ItIsZero}: ABBA[FinslerHadwiger]:={Pt,MidPt,Le,ItIsZero,DeSq,Slope}: ABBA[FoxTalbot]:={Quad,Le,MidPt,Concurrent}: ABBA[Fregier]:={ParEllipse,NormalToEllipse}: ABBA[Fuhrmann]:={SSR1,ParamCircle,DeSq,ItIsZero}: ABBA[Gergonne]:={Te,Incircle,Concurrent,Le,PtLeCe}: ABBA[Griffiths]:={Circumcenter,Ce,Pedal,NinePointCircle}: ABBA[Herron]:={DeSq,ItIsZero,AREA}: ABBA[Hoehn]:={DeSq,Le,Pt,ItIsZero}: ABBA[IncenterExists]:={Concurrent,TS}: ABBA[Johnson]:={ParamCircle,MirRefOf0,ItIsZero,Radius,Ce}: ABBA[Lehmus]:={Pt,TS,DeSq}: ABBA[Lemoine]:={Te,Centroid,Concurrent,MirRefLeLe,Le}: ABBA[LeonAnne]:={Le,MidPt,AREA,ItIsZero}: ABBA[MarionMorgan]:={pmidpt,Le,Pt,AREA,ItIsZero}: ABBA[MedianTriangleLocus]:={AntiMedial,Te,Pedal,Incenter,DeSq,MidPt,Colinear}: ABBA[Menelaus]:={Pt,Le,ItIsZero,DeSq}: ABBA[Miquel]:={ParamCircle,ParPtPerBisect,MirRefPtLe,Concyclic}: ABBA[Monge]:={sin1,cos1,Colinear,TanMt}: ABBA[Morley]:={Pt,TS,ItIsEqui}: ABBA[Nagel]:={Te,Incircle,Concurrent,Le,PtLeCe}: ABBA[Napoleon]:={ItIsEqui,CET}: ABBA[NinePointCircleExists]:={Ft,Le,MidPt,Orthocenter,Concyclic}: ABBA[Nobbs]:={Contact,Colinear,Pt,Le}: ABBA[OrthocenterExists]:={Concurrent,Altitude,Le}: ABBA[Pappus]:={ParamLine,Colinear,Pt,Le}: ABBA[Pascal]:={ParEllipse,Colinear,Pt,Le}: ABBA[Pivot]:={Ce,OtherCeCe}: ABBA[Poncelet]:={TangentToEllipse,Pt,Circumradius,Circumcenter,ParamCircle, TouchCeLe1,TouchCeLe}: ABBA[Ptolemy]:={ParamCircle,Sqabc,DeSq}: ABBA[Purser]:={ParamCircle,DeSq,SSR}: ABBA[RadicalCenterExists]:={Concurrent, RadicalLine}: ABBA[Sadov]:={DeSq,ParamCircle,SqRtABCD}: ABBA[Simson]:={ParamCircle,Colinear,Ft,Le}: ABBA[Soddy]:={TcCesOut,ItIsZero}: ABBA[Varignon]:={MidPt,ItIsZero,Slope}: ABBA[Viviani]:={SSR,Te,ItIsZero,DeSq,Ft,Le}: ABBA[vonAubel]:={MDOS,ItIsZero,Slope,DeSq}: ABBA[Wittenbauer]:={Pt,Le,CentroidQ}: ##End of Fathers of Theorems ##Fathers of Definitions ABBA[Altitude]:={}: ABBA[AntiMedial]:={}: ABBA[AREA]:={}: ABBA[Billard]:={BilliardSym}: ABBA[BillardSym]:={Pt,Sym}: ABBA[Ce]:={}: ABBA[Center]:={}: ABBA[Centroid]:={Concurrency,Le,MidPt}: ABBA[CentroidQ]:={AREA,Centroid}: ABBA[CET]:={Circumcenter}: ABBA[Circumcenter]:={Center,Ce}: ABBA[Circumradius]:={Radius,Ce}: ABBA[Colinear]:={AREA}: ABBA[ComTangLgtSq]:={DeSq}: ABBA[Concyclic]:={Ce}: ABBA[Concurrency]:={}: ABBA[Concurrent]:={}: ABBA[Contact]:={Te,Incenter,Ft,Le}: ABBA[De]:={DeSq}: ABBA[DePtLeSq]:={DeSq,Pt,Altitude}: ABBA[DeSq]:={}: ABBA[DeSqG]:={}: ABBA[Excircles]:={Te,Incircle,TouchCeLe,Le}: ABBA[EulerLine]:={Le,Orthocenter,Circumcenter}: ABBA[Ft]:={Pt,Altitude}: ABBA[GergonnePt]:={Te,Incircle,Pt,Le,PtLeCe}: ABBA[Incenter]:={Te,Concurrency,TS}: ABBA[Incircle]:={Inradius,Incenter}: ABBA[Inradius]:={Te,Incenter,DePtLeSq,Le,DePtLeSq}: ABBA[ItIsEqui]:={DeSq}: ABBA[ItIsZero]:={}: ABBA[Kiss]:={Tangent,Colinear}: ABBA[Le]:={AREA}: ABBA[MDOS]:={Pt,Le}: ABBA[MidPt]:={}: ABBA[MirRefLeLe]:={Pt,Le,MirRefPtLe}: ABBA[MirRefPtLe]:={Ft,Le}: ABBA[MirRefOf0]:={Ft,Le}: ABBA[NagelPt]:={Te,Incircle,Pt,Le,PtLeCe}: ABBA[NinePointCircle]:={Ce,MidPt}: ABBA[NormalToEllipse]:={ParEllipse}: ABBA[Orthocenter]:={Concurrency,Altitude,Le}: ABBA[OtherCeCe]:={}: ABBA[ParamCircle]:={}: ABBA[ParamLine]:={}: ABBA[ParEllipse]:={}: ABBA[ParPtPerBisect]:={MidPt,Slope}: ABBA[Pedal]:={Ft,Le}: ABBA[PerpMid]:={PerpPQ,MidPt}: ABBA[PerpPQ]:={}: ABBA[pmidpt]:={}: ABBA[Powe]:={DeSq}: ABBA[Pt]:={}: ABBA[PtLeCe]:={}: ABBA[Quad]:={Pt}: ABBA[RadicalLine]:={Powe}: ABBA[Radius]:={Center}: ABBA[sin1]:={}: ABBA[cos1]:={}: ABBA[tan1]:={sin1,cos1}: ABBA[Slope]:={}: ABBA[Sqabc]:={ItIsZero}: ABBA[SqRtABCD]:={}: ABBA[SSR]:={}: ABBA[Te]:={Pt,TS}: ABBA[TS]:={}: ABBA[Tangent]:={}: ABBA[TangentToEllipse]:={ParEllipse}: ABBA[TanMt]:={sin1,cos1}: ABBA[Thebault]:={Incenter,TouchCe1,TouchCeLe1,Le,Colinear}: ABBA[TouchCe]:={ItIsZero}: ABBA[TouchCe1]:={}: ABBA[TouchCeLe]:={ItIsZero}: ABBA[TouchCeLe1]:={}: ABBA[TcCesOut]:={}: ##End of Fathers of Definitions #IterAbba(Set1): Given a set of definitions #joins to them the definitions that depend on #them IterAbba:=proc(Set1) local i,gu: gu:={}: for i from 1 to nops(Set1) do gu:=gu union ABBA[op(i,Set1)]: od: gu union Set1: end: #ANCESTORS(Set1): the set of all ancestors of the #definitions in the set Set1, including themselves ANCESTORS:=proc(Set1) local gu,mu,mun: gu:=Set1: mu:=IterAbba(gu): while mu<>gu do mun:=IterAbba(mu): gu:=mu: mu:=mun: od: mu: end: #SelfContained(Theorem): given a theorem, prints its #statment, plus all the required definitions SelfContained:=proc(Theorem1) local gu,i,t0: gu:=ABBA[Theorem1]: gu:=ANCESTORS(gu): lprint(``): lprint(`The definitions needed for the`,Theorem1,`Theorem are `): print(``): for i from 1 to nops(gu) do lprint(gu[i],`:=`): print(gu[i]): od: lprint(`The statement of the`,Theorem1, ` Theorem is `): print(``): print(Theorem1): print(``): lprint(`Now let Maple prove it; The theorem is`): t0:=time(): print(Theorem1()); print(``): lprint(`The whole proof took`, time() -t0, ` seconds of CPU time `): end: #Contributed by Matthew Russell (Amer. Math. Monthly Problem #11615, Feb. 2012) P11615:=proc() local T,m,n,A,B,C,D,E,F,K,M,N,P,MK,NK,PK,MN,MP,NP,SAK,SBK,SCK,ParD,ParE,ParF: print(`Contributed by Matthew Russell (Amer. Math. Monthly Problem #11615, Feb. 2012)`): T:=Te(m,n): A:=T[1]: B:=T[2]: C:=T[3]: K:=[K1,K2]: M:=MidPt(B,C): N:=MidPt(A,C): P:=MidPt(A,B): MK:=Le(M,K): NK:=Le(N,K): PK:=Le(P,K): MN:=Le(M,N): MP:=Le(M,P): NP:=Le(N,P): D:=Pt(MK,NP): E:=Pt(NK,MP): F:=Pt(PK,MN): SAK:=Slope(A,K): SBK:=Slope(B,K): SCK:=Slope(C,K): ParD:=LePtSlope(D,SAK): ParE:=LePtSlope(E,SBK): ParF:=LePtSlope(F,SCK): evalb(Concurrent(ParD,ParE,ParF) or evalb(subs(x=K[1],y=K[2],Le(A,B))=0) or evalb(subs(x=K[1],y=K[2],Le(A,C))=0) or evalb(subs(x=K[1],y=K[2],Le(B,C))=0)): end: LePtSlope:=proc(P,m): expand((y-P[2])-m*(x-P[1])): end: Ekhad:=proc() local i,P,s,t: for i from 1 to 4 do P[i]:=[s[i],t[i]]: od: Colinear( Pt(Le(P[1],P[2]),Le(Pt(Le(P[1],P[3]), Le(P[2],P[4])), Pt(Le(P[1],P[4]), Le(P[2],P[3])))), Pt(Le(P[1],P[3]),Le(Pt(Le(P[1],P[2]), Le(P[3],P[4])), Pt(Le(P[1],P[4]), Le(P[2],P[3])))), Pt(Le(P[2],P[3]),Le(Pt(Le(P[1],P[2]), Le(P[3],P[4])), Pt(Le(P[1],P[3]), Le(P[2],P[4]))))): end: # Pt1:={{1, 2}, {{{1, 3}, {2, 4}}, {{1, 4}, {2, 3}}}}, #Pt2:={{1, 3}, {{{1, 2}, {3, 4}}, {{1, 4}, {2, 3}}}}, #Pt3:={{2, 3}, {{{1, 2}, {3, 4}}, {{1, 3}, {2, 4}}}} #P12027():Amer. Math. Monthly Problem #12027, March 2018) P12027:=proc() local m,n,T,Ci,A1,B1,C1,r,R,D1,E1,F1,X1,Y1,Z1,gu,lu,lu1,i: T:=Te(m,n): Ci:=Incircle(m,n): r:=Inradius(m,n): R:=Circumradius(T): if subs({m=1/3,n=1/4},r)<0 then r:=-r: fi: if subs({m=1/3,n=1/4},R)<0 then R:=-R: fi: A1:=T[1]: B1:=T[2]: C1:=T[3]: D1:=PtLeCe(Le(B1,C1),Ci): E1:=PtLeCe(Le(C1,A1),Ci): F1:=PtLeCe(Le(A1,B1),Ci): gu:=[solve({Le(A1,D1),Ci},{x,y})]: gu:=normal({subs(gu[1],[x,y]),subs(gu[2],[x,y])}) minus {D1}: X1:=gu[1]: gu:=[solve({Le(B1,E1),Ci},{x,y})]: gu:=normal({subs(gu[1],[x,y]),subs(gu[2],[x,y])}) minus {E1}: Y1:=gu[1]: gu:=[solve({Le(C1,F1),Ci},{x,y})]: gu:=normal({subs(gu[1],[x,y]),subs(gu[2],[x,y])}) minus {F1}: Z1:=gu[1]: lu:= [simplify(sqrt(DeSq(A1,X1)/DeSq(X1,D1)),symbolic), simplify(sqrt(DeSq(B1,Y1)/DeSq(Y1,E1)),symbolic), simplify (sqrt(DeSq(C1,Z1)/DeSq(Z1,F1)) ,symbolic)]: lu1:=[]: for i from 1 to nops(lu) do if subs({m=1/3,n=1/4},lu[i])<0 then lu1:=[op(lu1),-lu[i]]: else lu1:=[op(lu1),lu[i]]: fi: od: lu:=lu1: evalb(normal(convert(lu,`+`)-(R/r-1/2))=0); end: MiquelFiveCircle:=proc() local s,P,Q,Qa,gu,i,r,C: s[5]:=-1/mul(s[i],i=1..4): gu:=1: for i from 1 to 5 do P[i]:=ParamCircle([0,0],1,gu): Q[i]:=ParamCircle([0,0],1,gu*s[i]): r[i]:=expand(DeSq(P[i],Q[i])): C[i]:=expand(DeSq([x,y],P[i])-r[i]): gu:=gu*s[i]*s[i+1]: od: for i from 1 to 4 do Qa[i]:=OtherCeCe(C[i],C[i+1],Q[i]): od: evalb(normal(DeSq(Pt(Le(Qa[1],Qa[2]),Le(Qa[3],Qa[4])),P[3])-DeSq(Q[2],P[3]))=0): end: #Added Sept. 24, 2018, suggested by Matthew Russell Symmedian:=proc(m,n) local T,f,a,b: T:=Te(m,n): f:=numer(DeSq([a,b],Ft([a,b],Le(T[2],T[3])))+DeSq([a,b],Ft([a,b],Le(T[3],T[1])))+DeSq([a,b],Ft([a,b],Le(T[1],T[2])))): factor(subs(solve({diff(f,a),diff(f,b)},{a,b}),[a,b])); end: ###start stuff May 2019 #Csqu(A,B): the cener of the square above the line AB Csq:=proc(A,B) local C: C:=B-A: A+[(C[1]-C[2])/2, (C[1]+C[2])/2]: end: vanAubel:=proc() local A,B,C,D,Cx,Cy,Dx,Dy,A1,B1,C1,D1: A:=[0,0]: B:=[1,0]: C:=[Cx,Cy] : D:=[Dx,Dy]: A1:=Csq(A,B):B1:=Csq(B,C):C1:=Csq(C,D): D1:=Csq(D,A): evalb(normal(DeSq(A1,C1)-DeSq(B1,D1))=0 and normal(Slope(A1,C1)*Slope(B1,D1)+1=0)): end: Berendonk:=proc() local A,B,C,D,A1,B1,C1,D1: A:=[0,0]: B:=[1,0]: C:=[c,e]: D:=[d,e]: B1:=Csq(C,B): D1:=Csq(A,D): A1:=[1/2,-(c-d)/2]: C1:=[(c+d)/2,e+1/2]: evalb(normal(DeSq(A1,B1)-DeSq(C1,D1))=0 and normal(DeSq(B1,C1)-DeSq(C1,D1))=0 and normal(DeSq(D1,A1)-DeSq(C1,D1))=0 and normal(Slope(B1,A1)*Slope(B1,C1)+1)=0): end: #Siebeck(): Degree 3 Siebeck (e.g.: Theorem 1, P. Gorkin, Amer. Math. Monthly v. 126 (2019) 99-11, p. 99) Siebeck:=proc() local d,z,t,Li1,i,P,m,eq,L,var,z0,F: for i from 0 to 2 do L[i]:=ParEllipse([0,0],d,t[i]): od: for i from 0 to 2 do Li1[i]:=TangentToEllipse([0,0],d,t[i]): od: for i from 0 to 2 do P[i]:=Pt(Li1[i],Li1[i+1 mod 3]): od: eq:=numer({ m[1]-DeSq(L[1],P[1])/DeSq(P[0],L[1]), m[1]/m[2]-DeSq(P[1],L[2])/DeSq(L[2],P[2]) , m[2]-DeSq(P[2],L[0])/DeSq(L[0],P[0])}); var:=factor(solve(eq,{m[1],m[2]})): m[0]:=1: m[1]:=sqrt(subs(var,m[1]),symbolic): m[2]:=-sqrt(subs(var,m[2]),symbolic): for i from 0 to 2 do z0[i]:=normal(P[i][1]+I*P[i][2]): od: F:=numer(m[0]/(z-z0[0])+m[1]/(z-z0[1])+m[2]/(z-z0[2])): F:=numer(normal(F/subs(z=0,F))): evalb(F=-z^2+d[1]^2-d[2]^2): end: #IsogonalConjugate(m,n,P): The isogonal conjugate of the point P w.r.t to Te(m,n) IsogonalConjugate:=proc(m,n,P) :factor(Pt(Le([0,0],MirRefPtLe(P,y-m*x)),Le([1,0],MirRefPtLe(P,y+n*x-n) ))):end: #IsogonalConjugateExists(): The isogonal conjugate of the point P w.r.t to Te(m,n) IsogonalConjugateExists:=proc() local m,n,P,T,A,B,C,Pa,Pb,Pc: T:=Te(m,n):A:=T[1]:B:=T[2]: C:=T[3]: Pa:=MirRefPtLe(P,y-m*x):Pb:=MirRefPtLe(P,y+n*x-n): Pc:=MirRefPtLe(P,y-C[2]-(x-C[1])*TS(m,1/n)): evalb(normal(Pt(Le(A,Pa),Le(B,Pb)))=normal(Pt(Le(A,Pa),Le(C,Pc)))): end: #Leversha(): Gerry Leversha's theorem, Mathematical Gazette Note 100.23, v.100 (2016) (issue 548) pages 336-341 Leversha:=proc() local m,n,m1,n1,T1,T2,A,B,C: T1:=Te(m,n):T2:=Te(m1,n1):A:=[0,0]:B:=T1[3]:C:=T2[3]:evalb(DeSq(IsogonalConjugate(m1,n1,B),A)=DeSq(IsogonalConjugate(m,n,C),A)):end: #LevershaRadius(m,n,m1,n1) LevershaRadius:=proc(m,n,m1,n1) local P:P:=IsogonalConjugate(m1,n1,Te(m,n)[3]): sqrt(factor(normal(P[1]^2+P[2]^2)),symbolic):end: #LevershaPoints(m,n,m1,n1): If the quadrilateral is ABDC with A=[0,0], D=[1,0], tan((angle DAB)/2)=m,tan((angle ADB)/2)=n, #tan((angle DCB)/2)=m1,tan((angle ADC)/2)=n1, LevershaPoints:=proc(m,n,m1,n1):[IsogonalConjugate(m1,n1,Te(m,n)[3]),IsogonalConjugate(m,n,Te(m1,n1)[3])]:end: