Circumcenter

Load Eos

<<"EosHeader.m"
In[]:=
g3 Version 1.2.9
Eos3.31 (November 5,2020) running under Mathematica 12.1.1 for Mac OS X x86 (64-bit) (June 22, 2020)

Circumcenter

For any triangle ΔABE, the perpendicular bisectors of the three edges AB, BE and EA meet at the same point H.
Point H is called the circumcenter of ΔABE.
EosSession["Circumcenter"];
In[]:=
MarkOn[];
In[]:=
NewOrigami[10]
In[]:=
Circumcenter: Step 1
Out[]=
NewPoint["E"{7,8}]
In[]:=
Circumcenter: Step 1
Out[]=
HO["A","E"]!
In[]:=
Circumcenter: Step 3
Out[]=
HO["B","E",Mark{{"FG","H"},{"BC","I"}}]!
In[]:=
Circumcenter: Step 5
Out[]=
HO["A","B"]!
In[]:=
Circumcenter: Step 7
Out[]=
circle={Thick,Green,GraphicsCircle["H","AH"]};​​triangle={Thick,Red,Line[{"A","B","E","A"}]};
In[]:=
ShowOrigami[More{circle,triangle}]
In[]:=
Circumcenter: Step 7
Out[]=
Prove["circumcenter",Goal(IncidentQ["H","JK"]∧​​SquaredDistance["H","A"]==SquaredDistance["H","B"]SquaredDistance["H","E"]),Mapping{"A"{0,0},"B"{1,0},"C"{1,1},"D"{0,1},"E"{u,v}}]
In[]:=
ProofbyGB
::gbstart
:Proof by Groebner basis method started at November 30, 2020 at 10:53:58 AM JST.
ProofbyGB
::gbsuccess
:Proof by Groebner basis method is successful.CPU time used for Groebner basis computation is 0.070567 seconds.
Proof is successful.
Circumcenter: Step 7
Success,0.070567,
circumcenter.nb

Out[]=
EndSession[];
In[]:=