Incenter

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)

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.
EosSession["Incenter"];
In[]:=
NewOrigami[10]
In[]:=
Incenter: Step 1
Out[]=
NewPoint["E"{9,8}]
In[]:=
Incenter: Step 1
Out[]=
HO["AE"]!
In[]:=
Incenter: Step 3
Out[]=
HO["AE","AB"]
In[]:=
Incenter: Step 3

,

Out[]=
HO["AE","AB",FoldLine1]!
In[]:=
Incenter: Step 5
Out[]=
HO["BE"]!
In[]:=
Incenter: Step 7
Out[]=
HO["BA","BE"]
In[]:=
Incenter: Step 7

,

Out[]=
HO["BA","BE",FoldLine2,Mark{{$fline[4],"I"}}]!
In[]:=
Incenter: Step 9
Out[]=
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}]
In[]:=
Incenter: Step 11
Out[]=
(*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}}]
In[]:=
ProofbyGB
::gbstart
:Proof by Groebner basis method started at November 30, 2020 at 9:07:56 AM JST.
ProofbyGB
::gbsuccess
:Proof by Groebner basis method is successful.CPU time used for Groebner basis computation is 1.07293 seconds.
Proof is successful.
Incenter: Step 11
Success,1.07293,
Incenter.nb

Out[]=
EndSession[];
In[]:=