GEO0010 - The fundamental principle of affine geometry The Database contents GEO0008 - Orthocenter Theorem GEO0009 -- Midpoint of a Parallelogram

GEO0009 -- Midpoint of a Parallelogram

The Theorem Statement [ZCG95]

Theorem. Let O be the intersection of the two diagonals AC and BD of a parallelogram ABCD. Then O is the midpoint of AC.

The Image - GCLC 5.0

Prover's Code

point A 20 10
point B 70 10
point C 90 40

line ab A B
parallel cd C ab

line bc B C
parallel ad A bc

intersec D ad cd

line a A C
line b D B

intersec O a b

drawsegment A B
drawsegment A D
drawsegment D C
drawsegment B C
drawsegment A C
drawsegment B D


cmark_b A
cmark_b B
cmark_t C
cmark_t D
cmark_b O

prove { equal { sratio A O O C } { 1 }  }
Proved -- Proof, made with GCLC, v1.0

proofGEO0009.pdf
Pedro Quaresma and Predrag Janicic

GEO0010 - The fundamental principle of affine geometry The Database contents GEO0008 - Orthocenter Theorem GEO0009 -- Midpoint of a Parallelogram