|  |  | GEO0005 -- Pappus' Hexagon Theorem

## GEO0005 -- Pappus' Hexagon Theorem

##### The Theorem Statement [ZCG95]

Theorem. [Pappus's Hexagon Theorem] If A, B, and C are three points on one line, A1, B1, and C1 are three points on another line, and AB1 meets BA1 at P, AC1 meets CA1 at Q, and BC1 meets CD1 at S, then the three points P, Q, and S are collinear.

##### The Image - GCLC 5.0

##### Prover's Code

    point A 40 10
    point B 90 10
    %point C 120 10
    online C A B

    drawline A C

    cmark_b A
    cmark_b B
    cmark_b C

    point A_1 25 40
    point B_1 45 45
    %point C_1 65 50
    online C_1 A_1 B_1

    line A_1B_1 A_1 B_1

    drawline A_1 C_1
    cmark_t A_1
    cmark_t B_1
    cmark_t C_1

    line AB_1 A B_1
    line AC_1 A C_1
    line BA_1 B A_1
    line BC_1 B C_1
    line CA_1 C A_1
    line CB_1 C B_1

    drawsegment A B_1
    drawsegment A C_1
    drawsegment B A_1
    drawsegment B C_1
    drawsegment C A_1
    drawsegment C B_1

    intersec P AB_1 BA_1
    intersec Q AC_1 CA_1
    intersec S BC_1 CB_1
    cmark_l P
    cmark_t Q
    cmark_t S

    color 255 0 0
    drawline P S

    prove { equal { signed_area3 P Q S } 0 }

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

proofGEO0005.pdf

|  |  | GEO0005 -- Pappus' Hexagon Theorem