####Version of 10/9/98 (includes Poncelet) (DELETE THIS LINE!) #PLANE GEOMETRY: AN ELEMENTARY SCHOOL TEXTBOOK (ca. 2050 AD) #By Shalosh B. Ekhad, XIV ##Downloaded from the Future by Doron Zeilberger (zeilberg@math.temple.edu) #INTRODUCTION: #Dear Children, #Do you know that until fifty years ago most of mathematics was #done by humans? Even more strangely, they used human language #to state and prove mathematical theorems. Even when they started #to use computers to prove theorems, they always translated the #proof into the imprecise human language, because, ironically, computer #proofs were considered of questionable rigor! ## ##Only thirty years ago, when more and more mathematics was getting #done by computer, people realized how silly it is to go back-and-forth #from the precise programming-language to the imprecise humanese. #At the historical ICM 2022, the IMS (International Math Standards) #were introduced, and Maple was chosen the official language for mathematical #communication. They also realized that once a theorem is stated precisely, #in Maple, the proof process can be started right away, by running the #program-statement of the theorem. ## #All the theorems that were known to our grandparents, and most of what they #called conjectures, can now be proved in a few nano-seconds on any PC. #As you probably know, computers have since discovered much deeper theorems #for which we only have semi-rigorous proofs, because a complete proof would #take too long. ## #All the theorems in this textbook were automatically discovered (and #of course proved) by computer. The discovery program started with 3 #generic points in the plane, and iteratively constructed new points, lines, #and circles using a few primitives. Whenever a new point (or line, or circle, #or whatever) coincided with an old one, a "theorem" was born. Then a search #in Eric's Math Treasure Trove, version 1998, was performed, to see which of #the theorems that were discovered by the Discovery Program were anticipated #by humans; the program then automatically attached the human names #to the theorems. Not surprisingly, all the theorems that turned out to #be anticipated by humans, and that are presented in this very elementary #textbook, were of very low complexity and depth. # ##HOW TO USE THIS TEXTBOOK: # #You don't have to read it cover-to-cover. Pick any theorem #in Part I, and then look up, in Part II, the definitions used in the #statement-program of that theorem. #These definitions, in turn, may involve other definitions, etc. #Don't worry, none of the definitions are circular. ## ##Example: Look up Napoleon's Theorem. It involves two definitions: #ItIsEqui and CET. Look up ItIsEqui. It involves DeSq. DeSq is #primitive. Now look up CET. It uses Circumcenter. Circumcenter involves #the primitive definitions Ce and Center. Hence to understand the statement #of Napoleon's theorem you only need to look up the definitions: Ce, Center, #CET, Circumcenter, DeSq and ItIsEqui, and get a completely self-contained #statement of the so-called Napoleon Theorem. Then to prove it, get into #Maple by typing: "maple" (without the quotes); once inside Maple, #type: "read text;" (without the quotes), and then "Napoleon();" #(without the quotes). You should immediately get the response of the #computer: true. ## ## ##Note: A point is represented as a list of length 2. Lines are ##represented as a*x+b*y+c. ##WARNING: x and y are global variables! ### ###Note From the Downloader (DZ): ##IMPORTANT: THIS TEXTBOOK IS ALSO AVAILABLE ON-LINE AS A MAPLE PACKAGE ##CALLED "RENE", FROM http://www.math.temple.edu/~zeilberg/ ##(click on "Maple packages and programs", then click on "RENE"). ##This textbook was tested for Maple V, ver. 5 and previous versions. ##Unfortunately, every year or so, Maple comes out with a new version ##(bigger but not always better, and sometimes buggier) ##that is not fully compatible with code written for previous versions. ##The package RENE will be constantly updated to conform to future ##versions, but let's hope that Maple will start to become upward-compatible. ##RENE will also be continuously enlarged to include new proofs, in particular ##of Monthly problems and IMO problems (it already has a few now). ##########################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: 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: 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: 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: EulerLineExists:=proc() local A,B,C: Colinear(Orthocenter(A,B,C),Circumcenter(A,B,C),Centroid(A,B,C)):end: EulerTetrahedronVolumeFormula:=proc() local P1,P2,P3,P4,P,Q,R,A,B,C,Vol, p31,p32,p41,p42,p43: with(linalg):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: 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: 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: 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)):factor(DeSq([1,0],N)-DeSq([0,0],M)):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: 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: 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,I,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):I:=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,I,K,L,M):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: Poncelet:=proc() local t0,t1,t2,t3,A,B,C,t,R,Q,Q1,Q2,P,c,L1,L2,L3,eq: print(`Works, on Maple V, 0-5, except ver.3`): 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: 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: Soddy:=proc() local q,e1,e2,e3,e4,c,d,e,TC,R,r,s,t,p:with(grobner): 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: ########################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: #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 Circumcircle of the input 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):[-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: #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):Radius(Ce(A,B,C)):end: #Def (Are the input 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: #Def (The common point of the input lines) Concurrency:=proc() local q: q:=solve({args},{x,y}):[subs(q,x),subs(q,y)]: end: #Def (Are the input lines concurrent?) Concurrent:=proc(): not evalb(solve({args},{x,y})=NULL): end: #Def (Are the input 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 C1<>Ce(args[1],args[2],args[i]) then RETURN(false): fi: od: true: end: #Def (Square of distance of point P to line L) DePtLeSq:=proc(P,L):DeSq(Pt(Altitude(P,L),L),P):end: #Def (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 (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 (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 (The incenter of the triangle with vertices A(0,0), B(1,0), and with #slopes of AC and BC equal TS(m,m) and 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 of 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):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: #Def (The eq. of the line joining A and B) Le:=proc(A,B) AREA(A,B,[x,y]):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 the origin w.r.t. 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 origin w.r.t. the line Le) 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 (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 (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: #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 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: #Def (Generic point on a parametric line) ParamLine:=proc(m,b,t):[t,m*t+b]: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 (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 (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 radius of a circle Circ) Radius:=proc(Circ) local q: q:=Center(Circ):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: #Def (Given a circle Ce1 and a point Pt1 on it, find the eq. 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: #Def (Do the 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) and B(1,0) and with angles #CAB and CAB given) 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 and C2, do 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 guarantees 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, do 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 guarantees 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 (Tangent of a sum of given angles) 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: