Ceva’s Theorem
Ceva’s Theorem
Hidekazu Takahashi
Load Eos
Load Eos
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:13:21.
Construction
Construction
In[]:=
EosSession["Ceva's Theorem"];
In[]:=
NewOrigami[10];
In[]:=
NewPoint["E"{7,10}]
Ceva's Theorem/Origami: Step 1
Out[]=
In[]:=
HO["AE",Handle"D"]!
Ceva's Theorem/Origami: Step 3
Out[]=
In[]:=
HO["BE",Handle"C"]!
Ceva's Theorem/Origami: Step 5
Out[]=
In[]:=
NewPoint["F"{6,3}]
Ceva's Theorem/Origami: Step 5
Out[]=
In[]:=
HO["AF",Handle"B",Mark"BE"]!
Ceva's Theorem/Origami: Step 7
Out[]=
In[]:=
HO["BF",Handle"A",Mark{"AE"}]!
Ceva's Theorem/Origami: Step 9
Out[]=
In[]:=
HO["EF",Handle"B",Mark{"AB"}]!
Ceva's Theorem/Origami: Step 11
Out[]=
In[]:=
seg={Thick,Green,Line[{"A","G"}],Line[{"B","H"}],Line[{"E","I"}],Red,Line[{"A","E","B","A"}]};
In[]:=
GraphicsOrigami[Moreseg]
Ceva's Theorem/Origami: Step 11
Out[]=
Verification
Verification
Weprove=1.
EH
HA
AI
IB
BG
GE
In[]:=
Goal[SquaredDistance["E","H"]SquaredDistance["A","I"]SquaredDistance["B","G"]==SquaredDistance["H","A"]SquaredDistance["I","B"]SquaredDistance["G","E"]];
In[]:=
map={"A"{0,0},"B"{1,0},"C"{1,1},"D"{0,1},"E"{u1,u2},"F"{u3,u4}};
In[]:=
Prove["Ceva's Theorem",Mappingmap]
Proof is successful.
Ceva's Theorem/Origami: Step 11
Out[]=
In[]:=
EndSession[];