# Ceva’s Theorem

Ceva’s Theorem

Hidekazu Takahashi

## Load Eos

Load Eos

In[]:=

<<EosLoader`

Eos3.7.1.1 (March 21,2023) running under Mathematica 13.2.0 for Mac OS X ARM (64-bit) (November 18, 2022) on Thu 30 Mar 2023 14:46:19.

## Construction

Construction

## 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: Step 11

Out[]=

In[]:=

EndSession[];