|  |  | GEO0003 -- Harmonic Set

## GEO0003 -- Harmonic Set

##### The Theorem Statement [CGZ96]

Theorem. [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. Then (LF)/(KF) = (LG)/(GK).

##### The Image - GCLC 5.0

##### Prover's Code

    point A 30 32
    point B 40 40
    point C 48 28
    point D 40 25

    cmark_lt A
    cmark_t B
    cmark_rt C
    cmark_rb D

    % point L
    line AB A B
    line CD C D
    intersec L AB CD
    cmark_b L

    % point K
    line AD A D
    line BC B C
    intersec K AD BC
    cmark_b K

    % point F
    line BD B D
    line KL K L
    intersec F BD KL
    cmark_b F

    % point G
    line AC A C
    intersec G AC KL
    cmark_b G

    drawsegment B L
    drawsegment C L
    drawsegment A K
    drawsegment B K
    drawsegment B F
    drawsegment A G
    drawsegment L G

    prove { equal { sratio L F K F } { sratio L G G K }  }

##### Proved -- Proof, made with GCLC, v1.0

proofGEO0003.pdf

|  |  | GEO0003 -- Harmonic Set