Theorem([arbitrary(A,F,E,C), intersection(A,F,E,C,D), midpoint(A,C,G), online(B,E,A), online(B,F,C), midpoint(E,F,I), midpoint(D,B,H)],[online(H,I,G)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H} are reassigned Theorem: If the points A, F, E, and C are arbitrary, the two lines AF and EC intersect at D, G is the midpoint of A and C, the point A is on the line BE, the point C is on the line BF, `` || (I) || ` is the midpoint of ` || E || ` and ` || F , and H is the midpoint of D and B, then `the point G is on the line H` || (I) . Proof: char set produced: [3 x1 1] [1 y1 1] [3 x2 1] [2 y2 1] [6 x3 1] [3 y3 1] [2 x4 1] [2 y4 1] [3 x5 1] [3 y5 1] pseudo-remainder: [6 y5 1] = y5*x2 + ... (5 terms) pseudo-remainder: [8 x5 1] = -2*x5*y2 + ... (7 terms) pseudo-remainder: [10 y4 1] = x1*y4 + ... (9 terms) pseudo-remainder: [10 x4 1] = -2*x4*y1 + ... (9 terms) pseudo-remainder: [10 y3 1] = -u2*y3 + ... (9 terms) pseudo-remainder: [10 x3 1] = u1*v1*x3 + ... (9 terms) pseudo-remainder: [22 y2 1] = 2*v1*u1^2*u2*y2 + ... (21 terms) pseudo-remainder: [20 x2 1] = 2*u1*v2*y1*x2 + ... (19 terms) pseudo-remainder: [17 y1 1] = u1^2*v2*y1 + ... (16 terms) pseudo-remainder: [3 x1 1] = v1*x1 + ... (2 terms) `The theorem is true under the following subsidiary conditions:` . the line AF is not parallel to the line EC . the line AF is not perpendicular to the line AE . the line AE is not parallel to the line CF QED.
Theorem([arbitrary(F,C,A,E), intersection(A,F,E,C,D), midpoint(A,C,G), online(B,E,A), midpoint(E,F,I), midpoint(D,B,H), online(H,I,G)],[online(B,F,C)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H} are reassigned Theorem: If the points F, C, A, and E are arbitrary, the two lines AF and EC intersect at D, G is the midpoint of A and C, the point A is on the line BE, `` || (I) || ` is the midpoint of ` || E || ` and ` || F , H is the midpoint of D and B, and `the point G is on the line H` || (I) , then the point C is on the line BF. Proof: char set produced: [6 x1 1] [3 y1 1] [2 x2 1] [2 y2 1] [17 x3 1] [4 y3 1] [3 x4 1] [2 y4 1] [3 x5 1] [3 y5 1] pseudo-remainder: [2 y3 1] = -u1*y3 + ... (1 terms) pseudo-remainder: [6 x3 1] = -u1*v1*x3 + ... (5 terms) pseudo-remainder: [32 y2 1] = -2*v1*u1^2*u3*y2 + ... (31 terms) pseudo-remainder: [26 x2 1] = 2*v2*x2*v1*u1 + ... (25 terms) pseudo-remainder: [22 y1 1] = u1^2*y1*v1 + ... (21 terms) pseudo-remainder: [20 x1 1] = -u1^2*v2*v1*x1 + ... (19 terms) `The theorem is true under the following subsidiary conditions:` . the line AF is not parallel to the line EC . the line AF is not perpendicular to the line CF . the line AE is not perpendicular to the line CF . -2*u3*y2+2*v2*x2-u1*v2-2*v1*x2+v1*u1+u3*v1 <> 0 QED.
Theorem([arbitrary(A,E,F,C), intersection(A,F,E,C,D), midpoint(A,C,G), online(B,F,C), midpoint(E,F,I), midpoint(D,B,H), online(H,I,G)],[online(B,E,A)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H} are reassigned Theorem: If the points A, E, F, and C are arbitrary, the two lines AF and EC intersect at D, G is the midpoint of A and C, the point C is on the line BF, `` || (I) || ` is the midpoint of ` || E || ` and ` || F , H is the midpoint of D and B, and `the point G is on the line H` || (I) , then the point A is on the line BE. Proof: char set produced: [6 x1 1] [3 y1 1] [3 x2 1] [2 y2 1] [12 x3 1] [4 y3 1] [2 x4 1] [2 y4 1] [3 x5 1] [3 y5 1] pseudo-remainder: [2 y3 1] = u1*y3 + ... (1 terms) pseudo-remainder: [6 x3 1] = -u1*v1*x3 + ... (5 terms) pseudo-remainder: [28 y2 1] = -2*u3*v1*u2*u1*y2 + ... (27 terms) pseudo-remainder: [26 x2 1] = 2*v1^2*u1*x2 + ... (25 terms) pseudo-remainder: [22 y1 1] = -u1^2*y1*v1 + ... (21 terms) pseudo-remainder: [20 x1 1] = -u1^2*v2*v1*x1 + ... (19 terms) `The theorem is true under the following subsidiary conditions:` . the line AF is not parallel to the line EC . the line AF is not perpendicular to the line AE . the line AE is not perpendicular to the line CF . -2*u3*y2+u3*v1-2*v1*x2+v1*u2+2*v2*x2-u2*v2 <> 0 QED.
