Incenter

Load Eos

In[]:=
<<"EosHeader.m"

Incenter

For any triangle ΔABE, the angle bisectors of the three angles ∡A, ∡B and ∡E meet at the same point I.
Point I is the incenter of ΔABE.
In[]:=
EosSession["Incenter"];
In[]:=
NewOrigami[10]
Incenter: Step 1
Out[]=
In[]:=
NewPoint["E"{9,8}]
Incenter: Step 1
Out[]=
In[]:=
HO["AE"]!
Incenter: Step 3
Out[]=
In[]:=
HO["AE","AB"]
Incenter: Step 3
Out[]=

,

In[]:=
HO["AE","AB",FoldLine1]!
Incenter: Step 5
Out[]=
In[]:=
HO["BE"]!
Incenter: Step 7
Out[]=
In[]:=
HO["BA","BE"]
Incenter: Step 7
Out[]=

,

In[]:=
HO["BA","BE",FoldLine2,Mark{{$fline[4],"I"}}]!
Incenter: Step 9
Out[]=
In[]:=
HO["AB","I",Mark{{"AB","F"}}]!;
In[]:=
triangle={Thick,Red,Line[{"A","B","E","A"}]};
In[]:=
circle={Thick,Green,GraphicsCircle["I","IF"]};
In[]:=
ShowOrigami[More{triangle,circle}]
Incenter: Step 11
Out[]=
In[]:=
(*proofworksfromtheversionEos3.3.1*)
In[]:=
Goal[​​O3Q["EA","EB","EI"]SquaredDistance["I","F"]==​​SquaredDistanceLine["I","EB"]==SquaredDistanceLine["I","EA"]SquaredDistanceLine["I","AB"]];
In[]:=
Prove["Incenter",Mapping{"A"{0,0},"B"{1,0},(*"C"{1,1},"D"{0,1},*)"E"{u,v}}]
ProofbyGB
::gbstart
:Proof by Groebner basis method started at March 22, 2021 at 10:52:17 PM JST.
ProofbyGB
::gbsuccess
:Proof by Groebner basis method is successful.CPU time used for Groebner basis computation is 1.10585 seconds.
Proof is successful.
Incenter: Step 11
Out[]=
Success,1.10585,
Incenter.nb

In[]:=
EndSession[];