Menelaus’s Theorem

Hidekazu Takahashi

Header

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

Construction

In[]:=
EosSession["Menelaus's Theorem"];
In[]:=
NewOrigami[10];
In[]:=
NewPoint[{"E"{8,10},"F"{6,0}}]
Menelaus's Theorem: Step 1
Out[]=
In[]:=
HO["AE"]!
Menelaus's Theorem: Step 3
Out[]=
In[]:=
HO["EF"]!
Menelaus's Theorem: Step 5
Out[]=
In[]:=
NewPoint[{"G"{3,10},"H"{8,0}}]
Menelaus's Theorem: Step 5
Out[]=
In[]:=
HO["GH",Handle"C",Mark{"AE","EF"}]
Menelaus's Theorem: Step 6
Out[]=
In[]:=
Unfold[]
Menelaus's Theorem: Step 7
Out[]=
In[]:=
seg={{Blue,Thick,GraphicsLine["G","H"]},{Green,Thick,GraphicsLine["A","E"],GraphicsLine["E","F"],GraphicsLine["F","A"]}};
In[]:=
ShowOrigami[Moreseg]
Menelaus's Theorem: Step 7
Out[]=

Verification

Weprove
EI
IA
AH
HF
FJ
JE
=1.
In[]:=
Assume[¬("A""H")∧¬("F""H")∧¬("G""E")];
In[]:=
Goal[SquaredDistance["E","I"]SquaredDistance["A","H"]SquaredDistance["F","J"]==SquaredDistance["I","A"]SquaredDistance["H","F"]SquaredDistance["J","E"]];
In[]:=
map={"A"{0,0},"B"{1,0},"C"{1,1},"D"{0,1},"E"{u1,u2},"F"{1/2,0},"G"{u3,1},"H"{u4,0}};
In[]:=
Prove["Menelaus's Theorem",Mappingmap]
ProofbyGB
::gbstart
:Proof by Groebner basis method started at March 22, 2021 at 10:53:34 PM JST.
​
ProofbyGB
::gbsuccess
:Proof by Groebner basis method is successful.CPU time used for Groebner basis computation is 0.043102 seconds.
​
Proof is successful.
Menelaus's Theorem: Step 7
Out[]=
{Success,0.043102,
Menelaus's Theorem.nb
}
In[]:=
EndSession[];