Theorem([arbitrary(A,B,C), oncircle(A,B,C,D), perpfoot(A,C,D,F,F), perpfoot(B,C,D,G,G), perpfoot(B,A,D,E,E)],[online(E,G,F)]) Warning: the coordinates of the points from {A, B, C, D, E, F, G} are reassigned Theorem: If the points A, B, and C are arbitrary, the point D is on the circumcircle of the triangle ABC, F is the perpendicular foot of the line AC to the line DF, G is the perpendicular foot of the line BC to the line DG, and E is the perpendicular foot of the line BA to the line DE, then the point F is on the line EG. Proof: char set produced: [7 y1 2] [5 x2 1] [3 y2 1] [5 x3 1] [3 y3 1] [2 x4 1] [1 y4 1] pseudo-remainder: [6 y4 1] = y4*x2 + ... (5 terms) pseudo-remainder: [4 x4 1] = -x4*y2 + ... (3 terms) pseudo-remainder: [4 y3 1] = y3*x1 + ... (3 terms) pseudo-remainder: [6 x3 1] = -u2*x3*y2 + ... (5 terms) pseudo-remainder: [9 y2 1] = v1^2*u2^2*y2 + ... (8 terms) pseudo-remainder: [12 x2 1] = u1*u2^2*x2 + ... (11 terms) pseudo-remainder: [12 y1 2] = u1^2*v1^2*y1^2 + ... (11 terms) `The theorem is true under the following subsidiary conditions:` . the three points A, B and C are not collinear . the line AC is non-isotropic . the line BC is non-isotropic . the line AB is not perpendicular to the line BC . the line AC is not perpendicular to the line AB QED.
Theorem([arbitrary(A,C,D), perpfoot(A,C,D,F,F), perpfoot(B,C,D,G,G), perpfoot(B,A,D,E,E), online(E,G,F)],[oncircle(A,B,C,D)]) Warning: the coordinates of the points from {A, B, C, D, E, F, G} are reassigned Theorem: If the points A, C, and D are arbitrary, F is the perpendicular foot of the line AC to the line DF, G is the perpendicular foot of the line BC to the line DG, E is the perpendicular foot of the line BA to the line DE, and the point F is on the line EG, then the point D is on the circumcircle of the triangle ABC. Proof: char set produced: [1 x1 1] [1 y1 1] [25 y2 4] [7 x3 1] [4 y3 1] [7 x4 1] [4 y4 1] pseudo-remainder: [12 y2 2] = y2^2*v1*u1 + ... (11 terms) pseudo-remainder: [7 y1 0] = u1*v1*u2 + ... (6 terms) pseudo-remainder: [7 x1 0] = u1*v1*u2 + ... (6 terms) the thoerem is possibly false: further decomposition in progress Status: used = 960, alloced = 3201, time = 4.586 pseudo-remainder: [12 y2 2] = y2^2*v1*u1 + ... (11 terms) char set produced: [1 x1 1] [1 y1 1] [1 y2 1] [1 x3 1] [1 y3 1] [1 x4 1] [1 y4 1] pseudo-remainder: [12 y2 2] = y2^2*v1*u1 + ... (11 terms) further decomposition in progress 4 pseudo-remainder: [12 y2 2] = y2^2*v1*u1 + ... (11 terms) char set produced: [1 O 0] char set produced: [1 x1 1] [1 y1 1] [2 x2 1] [3 y2 1] [4 x3 1] [4 y3 1] [2 x4 1] [2 y4 1] char set produced: [1 x1 1] [1 y1 1] [2 x2 1] [3 y2 1] [2 x3 1] [2 y3 1] [4 x4 1] [4 y4 1] char set produced: [1 O 0] char set produced: [2 u2 1] [1 y2 1] [1 x3 1] [1 y3 1] [1 x4 1] [1 y4 1] pseudo-remainder: [12 y2 2] = y2^2*v1*u1 + ... (11 terms) pseudo-remainder: [6 u2 2] = -u2^2*v1*u1 + ... (5 terms) char set produced: [1 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] [1 x3 1] [1 y3 1] pseudo-remainder: [12 y2 2] = y2^2*v1*u1 + ... (11 terms) pseudo-remainder: [6 x2 2] = x2^2*v1*u1 + ... (5 terms) char set produced: [1 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] [1 x4 1] [1 y4 1] pseudo-remainder: [12 y2 2] = y2^2*v1*u1 + ... (11 terms) pseudo-remainder: [6 x2 2] = x2^2*v1*u1 + ... (5 terms) `The theorem is true under the following subsidiary conditions:` . the line AC is non-isotropic . the three points A, C and D are not collinear . v1*u1^2-u1*v1*x2+u1*u2*y2-u1*v1*u2+v1^2*y2+v1*u2*x2 <> 0 . -v1*u2^2+v1*u2*x2-u1*u2*y2+u1*v1*u2-u1*v1*x2-v1^2*y2 <> 0 . the three points A, B and C are not collinear . the three points A, C and F are not collinear . the line AC is not perpendicular to the line DF QED.
