Steiner-Lehmus Theorem
Steiner-Lehmus Theorem
Hidekazu Takahashi
Header
Header
In[]:=
<<"EosHeader.m"
Construction
Construction
In[]:=
EosSession["Steiner-Lehmus Theorem"];
In[]:=
NewOrigami[10];
In[]:=
NewPoint["E"{7,10}]
Steiner-Lehmus Theorem: Step 1
Out[]=
In[]:=
HO["AE",Handle"D"]
Steiner-Lehmus Theorem: Step 2
Out[]=
In[]:=
Unfold[]
Steiner-Lehmus Theorem: Step 3
Out[]=
In[]:=
HO["BE",Handle"C"]
Steiner-Lehmus Theorem: Step 4
Out[]=
In[]:=
Unfold[]
Steiner-Lehmus Theorem: Step 5
Out[]=
In[]:=
HO["AB","AE",Mark"BE"]
Steiner-Lehmus Theorem: Step 5
Out[]=
,
In[]:=
HO["AB","AE",Mark"BE",FoldLine1]
Steiner-Lehmus Theorem: Step 6
Out[]=
In[]:=
Unfold[]
Steiner-Lehmus Theorem: Step 7
Out[]=
In[]:=
HO["AB","BE",Mark"AE"]
Steiner-Lehmus Theorem: Step 7
Out[]=
,
In[]:=
HO["AB","BE",Mark"AE",FoldLine2]
Steiner-Lehmus Theorem: Step 8
Out[]=
In[]:=
Unfold[]
Steiner-Lehmus Theorem: Step 9
Out[]=
In[]:=
seg={Thick,{Blue,Line[{"A","F"}],Line[{"B","G"}]},{Red,Line[{"A","E","B","A"}]}};
In[]:=
ShowOrigami[Moreseg]
Steiner-Lehmus Theorem: Step 9
Out[]=
Verification
Verification
We prove that if AF = BG then AE =BE.
In[]:=
Goal[SquaredDistance["A","F"]==SquaredDistance["B","G"]SquaredDistance["A","E"]==SquaredDistance["B","E"]];