Steiner-Lehmus Theorem

Hidekazu Takahashi

Header

In[]:=
<<EosLoader`
Eos3.7.1.1 (March 21,2023) running under Mathematica 13.2.0 for Mac OS X ARM (64-bit) (November 18, 2022) on Thu 30 Mar 2023 14:42:34.

Construction


Verification

We prove that if AF = BG then AE =BE.
In[]:=
Goal[SquaredDistance["A","F"]==SquaredDistance["B","G"]SquaredDistance["A","E"]==SquaredDistance["B","E"]];
In[]:=
map={"A"{0,0},"B"{1,0},"C"{1,1},"D"{0,1},"E"{u1,u2}};
In[]:=
Prove["Steiner-Lehmus Theorem",Mappingmap]
Proof is successful.
Steiner-Lehmus Theorem: Step 9
Out[]=
{Success,0.024429,
Steiner-Lehmus Theorem.pdoc.nb
}
In[]:=
EndSession[];