\documentclass[11pt,a4paper]{report}
\usepackage{pstricks}
\usepackage{rotating}
\usepackage{amssymb}
\usepackage{mathabx}
\usepackage{graphicx}
\usepackage{verbatim}
\usepackage{dsfont}
%%% para as demonstra\c c\~oes feitas com o proverGCLC
\usepackage{gclc}
\usepackage[dvips]{hyperref}


%\hypersetup{colorlinks,citecolor=green,filecolor=green,linkcolor=blue,urlcolor=blue}


\newcounter{elimlemmas}
\def\eliminationlemma{\refstepcounter{elimlemmas}%
  EL\theelimlemmas%
  \label{lemma:EL\theelimlemmas}}
\def\ratio#1#2{%
  \frac{\overline{#1}}{\overline{#2}}%
}

\newcommand{\barra}{\vrule height1.2em width0em depth0.8em}
\newtheorem{defs}{Definition}%[section]
\newtheorem{lema}{Lemma}%[section]
\newtheorem{geothm}{Theorem}


\begin{document}

\thispagestyle{empty}
\vspace*{-1cm} % medido
{\ }

\vspace*{2em}
\hspace*{-2cm}\hbox{\sf TR 2006/002\hspace*{12cm} ISSN\ 0874-338X}

\vspace*{2em}
\begin{center}\Large
  GeoThms - Geometry Theorems Database\\ 
  \large (\today)
\end{center}

\vspace*{1em}
\begin{center}
  Pedro Quaresma \\ 
  Department of Mathematics\\ 
  University of Coimbra, Portugal\\ 
  \&\\ 
  Predrag Janicic\\ 
  Faculty of Mathematics\\ 
  University of Belgrade, Serbia \& Montenegro
\end{center}


\vfill
\begin{center}
  \large Centre for Informatics and Systems of the University of Coimbra
\end{center}
\pagebreak

\setcounter{page}{1}
\title{GeoThms - Geometry Theorems Database}

\author{Pedro Quaresma\thanks{This work was partially supported by
CISUC/FCT.}\\ Department of Mathematics\\ University of
Coimbra\\ 3001-454 COIMBRA, PORTUGAL\\ 
e-mail: pedro@mat.uc.pt\quad phone: +351-239 791 170
\and
Predrag Janicic\thanks{This work was partially supported by the
CISUC/FCT, Centro International de Matem\'atica (CIM),
under the programme ``Research in Pairs'', while on visit to Coimbra
University under the Coimbra Group Hospitality Scheme}\\ 
Faculty of Mathematics\\ 
University of Belgrade\\ 
Studentski trg 16\ 
11000 Belgrade, SERBIA \& MONTENEGRO\\ 
e-mail: janicic@matf.bg.ac.yu }

\maketitle



\input{abstract}

\tableofcontents

\input{intro}

\input{database}

\input{lemmas}


\appendix
\chapter{The Theorems Listing}

\section{ GEO0001 --- Ceva's Theorem }

\paragraph{The Theorem Statement~\cite{Zhang95}}

\begin{geothm}[Ceva's Theorem]  Let $\Delta ABC$ be a triangle and $P$
  be any point in the plane. Let $D=AP\cap CB$, $E=BP\cap AC$, and
  $F=CP\cap AB$. Show that:
  
  $$
  \ratio{AF}{FB}\times\ratio{BD}{DC}\times\ratio{CE}{EA}=1
  $$
  $P$ should not be in the lines parallels to AC, AB and BC and passing
  through B, C and A respectively.
\end{geothm}
\paragraph{The Image -- Eukleides 1.0.2}

\begin{center}
{\footnotesize
\input{imageGEO0001.tex}
}
\end{center}


\paragraph{Prover's Code}

\small\begin{verbatim}
point A 80 10
point B 50 100
point C 100 100
point P 75 75

line a B C
line b A C
line c A B

line pa P A
line pb P B
line pc P C

intersec D a pa
intersec E b pb
intersec F c pc

drawsegment A B
drawsegment A C
drawsegment B C

drawsegment A D
drawsegment B E
drawsegment C F

cmark_b A
cmark_t B
cmark_t C
cmark_t D
cmark_lt F
cmark_rt E
cmark_t P

prove { equal { mult { mult { sratio A F F B } 
                            { sratio B D D C } } 
                            { sratio C E E A } } 1 }
\end{verbatim}


\paragraph{Proof}

\begin{center}
No Proof in the database 
\end{center}


\vfill
\pagebreak



\bibliographystyle{alpha}
\bibliography{pedro.bib}
%\bibliography{techRepCISUC0206.bib}
\end{document}

\section{ GEO0002 --- Midpoint Theorem }

\paragraph{The Theorem Statement~\cite{Narboux04}}

\begin{geothm}[Midpoint Theorem]  
  Let $\Delta ABC$ be a triangle and $A^\prime$ and
  $B^\prime$ be the midpoints of $BC$ and $AC$ respectively. Then the line
  $A^\prime B^\prime$ is parallel to the base $AB$, that is:

  $$
  {\cal S}_{A^\prime B^\prime A}={\cal S}_{A^\prime B^\prime B}
  $$
\end{geothm}
\paragraph{The Image -- Eukleides 1.0.2}

\begin{center}
{\footnotesize
\input{imageGEO0002.tex}
}
\end{center}


\paragraph{Prover's Code}

\small\begin{verbatim}
point A 20 10
point B 70 10
point C 35 40

drawsegment A B
drawsegment A C
drawsegment B C

midpoint B_l B C
midpoint A_l A C

drawsegment A_l B_l

cmark_b A
cmark_b B
cmark_t C

cmark_l A_l
cmark_r B_l

prove { equal { signed_area3 A_l B_l A } { signed_area3 A_l B_l B } }
\end{verbatim}


\paragraph{Proof}

\begin{center}
No Proof in the database 
\end{center}


\vfill
\pagebreak

\section{ GEO0003 ---  }

\paragraph{The Theorem Statement~\cite{Zhang95}}

\begin{geothm}[]
  Let $O$ be the intersection of the two diagonals $AC$ and
  $BD$ of a parallelogram $ABCD$. The point $O$ is the midpoint of
  $AC$. 
\end{geothm}
\paragraph{The Image -- Eukleides 1.0.2}

\begin{center}
{\footnotesize
\input{imageGEO0003.tex}
}
\end{center}


\paragraph{Prover's Code \& Proof}

\begin{center}
No Proof in the database 
\end{center}




\vfill
\pagebreak

\section{ GEO0004 --- Gauss-line Theorem }

\paragraph{The Theorem Statement~\cite{Zhang95}}

\begin{geothm}[Gauss-line Theorem] Let $A_0$, $A_1$, $A_2$, and $A_3$ be
  four point on a plane, $X$ the intersection of $A_1A_2$ and $A_0A_3$
 , and $Y$ the intersection of $A_0A_1$ and $A_2A_3$. Let $M_1$,
 $M_2$, and $M_3$ be the midpoints of $A_1A_3$, $A_0A_2$, and $XY$,
 respectively, then $M_1$, $M_2$, and $M_3$ are collinear.
\end{geothm}
\paragraph{The Image -- Eukleides 1.0.2}

\begin{center}
{\footnotesize
\input{imageGEO0004.tex}
}
\end{center}


\paragraph{Prover's Code}

\small\begin{verbatim}
area 5 5 90 90

point A_0 50 10
point A_1 90 10
point A_2 75 40
point A_3 55 25

line a12 A_1 A_2
line a03 A_0 A_3

line a01 A_0 A_1
line a23 A_2 A_3

intersec X a12 a03
intersec Y a01 a23


midpoint M_1 A_1 A_3
midpoint M_2 A_0 A_2
midpoint M_3 X Y 

cmark_b A_0
cmark_b A_1
cmark_b A_2
cmark_b A_3

cmark_b X
cmark_b Y

cmark_b M_1
cmark_b M_2
cmark_b M_3

drawsegment A_0 A_1
drawsegment A_0 A_2
drawsegment A_0 A_3
drawsegment A_1 A_2
drawsegment A_1 A_3
drawsegment A_2 A_3

drawdashsegment A_1 X
drawdashsegment A_3 X

drawdashsegment A_0 Y
drawdashsegment A_2 Y

drawline M_1 M_2

prove { equal { signed_area3 M_l M_2 M_3 } { 0 }
\end{verbatim}


\paragraph{Proof}

\begin{center}
No Proof in the Database
\end{center}




\vfill
\pagebreak

\section{ GEO0005 --- Pappus' Theorem }

\paragraph{The Theorem Statement~\cite{Zhang95}}

\begin{geothm}[Pappus' Theorem]
 Let points $A$, $B$, and $C$ be on one line, and $A_1$, $B_1$, and $C_1$ be on another line. Let $P=AB_1\cap A_1B$,
$Q=AC_1\cap A_1C$, and $S=BC_1\cap B_1C$. Show that $P$, $Q$, and $S$ are collinear.
\end{geothm}
\paragraph{The Image -- Eukleides 1.0.2}

\begin{center}
{\footnotesize
\input{imageGEO0005.tex}
}
\end{center}


\paragraph{Prover's Code \& Proof}

\begin{center}
No Proof in the database 
\end{center}




\vfill
\pagebreak

\section{ GEO0006 --- The Centroid Theorem }

\paragraph{The Theorem Statement~\cite{Chou96}}

\begin{geothm}[The Centroid Theorem]
 The three medians of a triangle meet in a point, and each median is trisected by this point.
\end{geothm}

Non-degenerate condition: The triangle is non-degenerate.
\paragraph{The Image -- Eukleides 1.0.2}

\begin{center}
{\footnotesize
\input{imageGEO0006.tex}
}
\end{center}


\paragraph{Prover's Code \& Proof}

\begin{center}
No Proof in the database 
\end{center}




\vfill
\pagebreak

\section{ GEO0007 --- Menelaus' Theorem }

\paragraph{The Theorem Statement~\cite{Chou96}}

\begin{geothm}[Menelaus' Theorem]
 A transversal meets the three sides $AB$, $BC$, and $CA$ of a triangle $ABC$ in $F$, $D$, and $E$ respectively. Then $\frac{\overline{AF}}{\overline{FB}} = -\frac{\overline{DC}}{\overline{BD}}\cdot\frac{\overline{EA}}{\overline{CE}}$.
\end{geothm}

Non-degenerate condition: $A$, $B$, and $C$ are not on line $EF$. 
\paragraph{The Image -- Eukleides 1.0.2}

\begin{center}
{\footnotesize
\input{imageGEO0007.tex}
}
\end{center}


\paragraph{Prover's Code}

\small\begin{verbatim}
dim 100 100
area 5 5 90 90 

point A 30 20
point B 70 20
point C 40 70

point X 15 55
point Y 75 10

line a B C
line b A C
line c A B

line p X Y 

intersec D a p
intersec E b p
intersec F c p

drawsegment A B
drawsegment A C
drawsegment B C

drawline p 

cmark_b A
cmark_t B
cmark_t C

cmark_t D
cmark_lt E
cmark_rt F


prove { equal { signed_area3 D E F } { 0 } }
\end{verbatim}


\paragraph{Proof}

\begin{center}
No Proof in the Database
\end{center}




\vfill
\pagebreak

\section{ GEO0008 --- Pascalian Axiom }

\paragraph{The Theorem Statement~\cite{Chou96}}

\begin{geothm}[Pascalian Axiom]
 Let $A$, $B$, and $C$ be three points on one line, and $P$, $Q$, and $R$ be three  points on another line. If $AQ \| RB$ and $BP \| QC$ then $AP\| RC$.
\end{geothm}
\paragraph{The Image -- Eukleides 1.0.2}

\begin{center}
{\footnotesize
\input{imageGEO0008.tex}
}
\end{center}


\paragraph{Prover's Code \& Proof}

\begin{center}
No Proof in the database 
\end{center}




\vfill
\pagebreak

\section{ GEO0009 --- The fundamental principle of projective geometry }

\paragraph{The Theorem Statement~\cite{Zhang95}}

\begin{geothm}[The fundamental principle of projective geometry]
 Let $A$, $B$, $R$ be three points on a plane, $Q$ and $P$ be points on line $AR$ and $BR$, respectively. $S$ is the intersection of $QB$ and $AP$. $C$ is the intersection of $RS$ and $AB$. $F$ is the intersection of $QP$ and $AB$. Show that $\frac{\overline{AC}}{\overline{BC}} = - \frac{\overline{AF}}{\overline{BF}}$.
\end{geothm}
\paragraph{The Image -- GCLC 4.0}

{\footnotesize
\begin{center}
  \input{imageGEO0009.pic}
\end{center} 
}
\paragraph{Prover's Code \& Proof}

\begin{center}
No Proof in the database 
\end{center}




\vfill
\pagebreak

\section{ GEO0010 --- The fundamental principle of affine geometry }

\paragraph{The Theorem Statement~\cite{Zhang95}}

\begin{geothm}[The fundamental principle of affine geometry]
 Let $A$, $B$, and $P$ be three points on a plane, and $C$ be a point on line $PA$. The line passing through $C$ and parallel to $AB$ intersects $PB$ in $D$. $Q$ is the intersection of $AD$ and $BC$. $M$ is the intersection of $AB$ and $PQ$. Show that $M$ is the midpoint of $AB$.
\end{geothm}
\paragraph{The Image -- GCLC 4.0}

{\footnotesize
\begin{center}
  \input{imageGEO0010.pic}
\end{center} 
}
\paragraph{Prover's Code \& Proof}

\begin{center}
No Proof in the database 
\end{center}




\vfill
\pagebreak

\section{ GEO0011 --- Pascal's Theorem }

\paragraph{The Theorem Statement~\cite{Zhang95}}

\begin{geothm}[Pascal's Theorem]
 Let $A$, $B$, $C$, $D$, $E$, and $F$ be six points with $P=AB\cap DE$, $Q=BC\cap DE$, and $S=CD\cap FA$ collinear. Then $P_1=AC\cap DE$, $Q_1=BE\cap CF$, and $S_1=AB\cap FD$ are also collinear.
\end{geothm}
\paragraph{The Image -- GCLC 4.0}

{\footnotesize
\begin{center}
  \input{imageGEO0011.pic}
\end{center} 
}
\paragraph{Prover's Code \& Proof}

\begin{center}
No Proof in the database 
\end{center}




\vfill
\pagebreak

\section{ GEO0012 --- Generalization of the Butterfly Theorem }

\paragraph{The Theorem Statement~\cite{Chou96}}

\begin{geothm}[Generalization of the Butterfly Theorem]
 The cross ration of four points on a circle with respect to any points on the circle is constant.
\end{geothm}
\paragraph{The Image -- Eukleides 1.0.2}

\begin{center}
{\footnotesize
\input{imageGEO0012.tex}
}
\end{center}


\paragraph{Prover's Code \& Proof}

\begin{center}
No Proof in the database 
\end{center}




\vfill
\pagebreak

\section{ GEO0013 --- Harmonic Set }

\paragraph{The Theorem Statement~\cite{Chou96}}

\begin{geothm}[Harmonic Set]
 Let $L$ be the intersection of $AB$ and $CD$. $K$ the intersection of $AD$ and $BC$, $F$ the intersection of $BD$ and $KL$, and $G$ the intersection of $AC$ and $KL$. Them $\frac{\overline{LF}}{\overline{KF}} = \frac{\overline{LG}}{\overline{GK}}$.
\end{geothm}
\paragraph{The Image -- GCLC 4.0}

{\footnotesize
\begin{center}
  \input{imageGEO0013.pic}
\end{center} 
}
\paragraph{Prover's Code \& Proof}

\begin{center}
No Proof in the database 
\end{center}




\vfill
\pagebreak

\section{ GEO0014 --- Desargues' Theorem }

\paragraph{The Theorem Statement~\cite{Chou96}}

\begin{geothm}[Desargues's Theorem]
 Given two triangles $ABC$, $A_1B_1C_1$, if the three lines $AA_1$, $BB_1$, and $CC_1$ meet in a point $S$, the three points $P=BC\cap B_1C_1$, $Q=CA\cap C_1A_1$, and $R=AB\cap A_1B_1$ lie on a line.
\end{geothm}
\paragraph{The Image -- GCLC 4.0}

{\footnotesize
\begin{center}
  \input{imageGEO0014.pic}
\end{center} 
}
\paragraph{Prover's Code \& Proof}

\begin{center}
No Proof in the database 
\end{center}




\vfill
\pagebreak

\section{ GEO0015 --- The Orthocenter Theorem }

\paragraph{The Theorem Statement~\cite{Chou95}}

\begin{geothm}[The Orthocenter Theorem]
 Let $\Delta ABC$ be a triangle, them the three altitudes of it are concurrent.
\end{geothm}
\paragraph{The Image -- GCLC 4.0}

{\footnotesize
\begin{center}
  \input{imageGEO0015.pic}
\end{center} 
}
\paragraph{Prover's Code \& Proof}

\begin{center}
No Proof in the database 
\end{center}




\vfill
\pagebreak



\bibliographystyle{alpha}
\bibliography{pedro.bib}
%\bibliography{techRepCISUC0206.bib}
\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 