Steiner-Lehmus Theorem

Hidekazu Takahashi

Header

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

Construction

EosSession["Steiner-Lehmus Theorem"];
In[]:=
NewOrigami[10];
In[]:=
NewPoint["E"{7,10}]
In[]:=
Steiner-Lehmus Theorem: Step 1
Out[]=
HO["AE",Handle"D"]
In[]:=
Steiner-Lehmus Theorem: Step 2
Out[]=
Unfold[]
In[]:=
Steiner-Lehmus Theorem: Step 3
Out[]=
HO["BE",Handle"C"]
In[]:=
Steiner-Lehmus Theorem: Step 4
Out[]=
Unfold[]
In[]:=
Steiner-Lehmus Theorem: Step 5
Out[]=
HO["AB","AE",Mark"BE"]
In[]:=
Steiner-Lehmus Theorem: Step 5

,

Out[]=
HO["AB","AE",Mark"BE",FoldLine1]
In[]:=
Steiner-Lehmus Theorem: Step 6
Out[]=
Unfold[]
In[]:=
Steiner-Lehmus Theorem: Step 7
Out[]=
HO["AB","BE",Mark"AE"]
In[]:=
Steiner-Lehmus Theorem: Step 7

,

Out[]=
HO["AB","BE",Mark"AE",FoldLine2]
In[]:=
Steiner-Lehmus Theorem: Step 8
Out[]=
Unfold[]
In[]:=
Steiner-Lehmus Theorem: Step 9
Out[]=
seg={Thick,{Blue,Line[{"A","F"}],Line[{"B","G"}]},{Red,Line[{"A","E","B","A"}]}};
In[]:=
ShowOrigami[Moreseg]
In[]:=
Steiner-Lehmus Theorem: Step 9
Out[]=

Verification

We prove that if AF = BG then AE =BE.
Goal[SquaredDistance["A","F"]==SquaredDistance["B","G"]SquaredDistance["A","E"]==SquaredDistance["B","E"]];
In[]:=