GEO0008 - Orthocenter Theorem The Database contents GEO0006 - Menelaus' Theorem GEO0007 -- Midpoint Theorem

GEO0007 -- Midpoint Theorem

The Theorem Statement [Nar04]

Theorem. [Midpoint Theorem] Let ABC be a triangle, and let Al and Bl be the midpoints of BC and AC respectively. Then the line AlBl is parallel to the base AB.

The Image - GCLC 5.0

Prover's Code

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_lt A_l
cmark_rt B_l

prove { equal { signed_area3 A_l B_l A } { signed_area3 A_l B_l B } }
Proved -- Proof, made with GCLC, v1.0

proofGEO0007.pdf
Pedro Quaresma and Predrag Janicic

GEO0008 - Orthocenter Theorem The Database contents GEO0006 - Menelaus' Theorem GEO0007 -- Midpoint Theorem