Menelaus’s Theorem

Hidekazu Takahashi

Header

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

Construction

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

Verification

Weprove
EI
IA
AH
HF
FJ
JE
=1.
Assume[¬("A""H")∧¬("F""H")∧¬("G","E")];
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]
In[]:=
ProofbyGB
::gbstart
:Proof by Groebner basis method started at November 30, 2020 at 2:29:00 PM JST.
ProofbyGB
::gbsuccess
:Proof by Groebner basis method is successful.CPU time used for Groebner basis computation is 0.03962 seconds.
Proof is successful.
Menelaus's Theorem: Step 7
Success,0.03962,
Menelaus's Theorem.nb

Out[]=
EndSession[];
In[]:=