# Menelaus’s Theorem

Menelaus’s Theorem

Hidekazu Takahashi

## Header

Header

<<"EosHeader.m"

In[]:=

## Construction

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[Moreseg]

In[]:=

Menelaus's Theorem: Step 7

Out[]=

## Verification

Verification

Weprove=1.

EI

IA

AH

HF

FJ

JE

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",Mappingmap]

In[]:=

Proof is successful.

Menelaus's Theorem: Step 7

Success,0.03962,

Out[]=

EndSession[];

In[]:=