Steiner-Lehmus Theorem

Hidekazu Takahashi

Header

In[]:=

<<EosLoader`

Eos3.7.2 (June 24,2023) running under Mathematica 13.2.1 for Mac OS X ARM (64-bit) (January 27, 2023) on Fri 23 Jun 2023 16:16:42.

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/Origami: Step 9

Out[]=

{Success,0.023249,

}

In[]:=

EndSession[];