Theorem([arbitrary(C,D,B,E), perpfoot(B,C,D,E,F), oncircle(B,E,D,C), midpoint(B,E,G), equidistance(F,G,B,G), equidistance(F,G,G,E), perpfoot(D,C,G,H,H)],[online(G,H,F)]) Warning: the coordinates of the points from {B, C, D, E, F, G, H} are reassigned Theorem: If the points C, D, B, and E are arbitrary, F is the perpendicular foot of the line BC to the line DE, the point C is on the circumcircle of the triangle BED, G is the midpoint of B and E, the distance between F and G is equal to the distance between B and G, the distance between F and G is equal to the distance between G and E, and H is the perpendicular foot of the line DC to the line GH, then the point F is on the line GH. Proof: char set produced: [4 v1 2] [3 v2 1] [6 x1 1] [3 y1 1] [2 x2 1] [3 y2 1] [2 x3 1] [1 y3 1] pseudo-remainder: [6 y3 1] = -y3*x1 + ... (5 terms) pseudo-remainder: [4 x3 1] = x3*y1 + ... (3 terms) pseudo-remainder: [2 y2 1] = y2*x1 + ... (1 terms) pseudo-remainder: [4 x2 1] = -v1*x2 + ... (3 terms) pseudo-remainder: [4 x1 1] = 2*v1*x1 + ... (3 terms) pseudo-remainder: [9 v2 2] = 2*u1*v2^2*u2 + ... (8 terms) pseudo-remainder: [13 v1 4] = -2*u1*v1^4*u2 + ... (12 terms) `The theorem is true under the following subsidiary conditions:` . the line DC is non-isotropic . the three points B, C and D are not collinear . the line BC is not perpendicular to the line CD . 2*u1-u3 <> 0 . the line BC is not parallel to the line DE . the line CD is not perpendicular to the line DE QED.
Theorem([arbitrary(C,D,E,B), perpfoot(B,C,D,E,F), oncircle(B,E,D,C), midpoint(B,E,G), equidistance(F,G,B,G), perpfoot(D,C,G,H,H), online(G,H,F)],[equidistance(F,G,G,E)]) Warning: the coordinates of the points from {B, C, D, E, F, G, H} are reassigned Theorem: If the points C, D, E, and B are arbitrary, F is the perpendicular foot of the line BC to the line DE, the point C is on the circumcircle of the triangle BED, G is the midpoint of B and E, the distance between F and G is equal to the distance between B and G, H is the perpendicular foot of the line DC to the line GH, and the point F is on the line GH, then the distance between F and G is equal to the distance between G and E. Proof: char set produced: [4 v1 2] [3 v2 1] [6 x1 1] [3 y1 1] [2 x2 1] [3 y2 1] [2 x3 1] [1 y3 1] pseudo-remainder: [6 y2 1] = 2*v1*y2 + ... (5 terms) pseudo-remainder: [6 x2 1] = -2*x1*x2 + ... (5 terms) pseudo-remainder: [6 y1 2] = y1^2 + ... (5 terms) pseudo-remainder: [5 x1 2] = u2^2*x1^2 + ... (4 terms) pseudo-remainder: [21 v2 3] = u1*v2^3*u2^3*v1 + ... (20 terms) Status: used = 1029, alloced = 3201, time = 4.586 `The theorem is true under the following subsidiary conditions:` . the line DC is non-isotropic . the three points C, D and E are not collinear . the line CD is not perpendicular to the line DE . 2*u2-u3 <> 0 . the line BC is not parallel to the line DE . the line BC is not perpendicular to the line CD QED.
Theorem([arbitrary(B,C,D,E), perpfoot(B,C,D,E,F), oncircle(B,E,D,C), midpoint(B,E,G), equidistance(F,G,G,E), perpfoot(D,C,G,H,H), online(G,H,F)],[equidistance(F,G,B,G)]) Warning: the coordinates of the points from {B, C, D, E, F, G, H} are reassigned Theorem: If the points B, C, D, and E are arbitrary, F is the perpendicular foot of the line BC to the line DE, the point C is on the circumcircle of the triangle BED, G is the midpoint of B and E, the distance between F and G is equal to the distance between G and E, H is the perpendicular foot of the line DC to the line GH, and the point F is on the line GH, then the distance between F and G is equal to the distance between B and G. Proof: char set produced: [1 u3 1] [1 v1 2] [6 v2 1] [3 x1 1] [1 y1 1] [3 x2 1] [2 y2 1] [5 x3 1] [3 y3 1] char set recomputed: [1 u3 1] [7 v2 2] [1 x1 1] [1 y1 1] [3 x2 1] [2 y2 1] [5 x3 1] [3 y3 1] pseudo-remainder: [6 y2 1] = -2*y1*y2 + ... (5 terms) pseudo-remainder: [6 x2 1] = 2*u1*x2 + ... (5 terms) pseudo-remainder: [6 y1 2] = y1^2 + ... (5 terms) pseudo-remainder: [4 x1 2] = x1^2 + ... (3 terms) pseudo-remainder: [1 u3 1] = u1*u3 `The theorem is true under the following subsidiary conditions:` . the line BC is non-isotropic . the line DC is non-isotropic . the three points B, C and D are not collinear . the line BC is not perpendicular to the line CD . the line BC is not parallel to the line DE QED.
Theorem([arbitrary(C,D,B,E), perpfoot(B,C,D,E,F), midpoint(B,E,G), equidistance(F,G,B,G), equidistance(F,G,G,E), perpfoot(D,C,G,H,H), online(G,H,F)],[oncircle(B,E,D,C)]) Warning: the coordinates of the points from {B, C, D, E, F, G, H} are reassigned Theorem: If the points C, D, B, and E are arbitrary, F is the perpendicular foot of the line BC to the line DE, G is the midpoint of B and E, the distance between F and G is equal to the distance between B and G, the distance between F and G is equal to the distance between G and E, H is the perpendicular foot of the line DC to the line GH, and the point F is on the line GH, then the point C is on the circumcircle of the triangle BED. Proof: char set produced: [8 v1 4] [3 v2 1] [6 x1 1] [3 y1 1] [2 x2 1] [3 y2 1] [2 x3 1] [1 y3 1] pseudo-remainder: [12 v2 2] = -v2^2*u1*v1 + ... (11 terms) pseudo-remainder: [7 v1 2] = -2*u1*v1^2*u2 + ... (6 terms) the thoerem is possibly false: further decomposition in progress char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [2 u2 1] [3 v2 1] [2 x1 1] [1 y1 1] [2 x2 1] [4 y2 1] [8 y3 1] pseudo-remainder: [12 v2 2] = -v2^2*u1*v1 + ... (11 terms) pseudo-remainder: [14 u2 2] = u1^3*u2^2 + ... (13 terms) char set produced: [1 O 0] char set produced: [3 v1 2] [3 v2 1] [5 x1 1] [5 y1 1] [2 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] pseudo-remainder: [12 v2 2] = -v2^2*u1*v1 + ... (11 terms) pseudo-remainder: [13 v1 2] = -2*u1^2*u2*v1^2 + ... (12 terms) further decomposition in progress 1 pseudo-remainder: [12 v2 2] = -v2^2*u1*v1 + ... (11 terms) pseudo-remainder: [13 v1 2] = -2*u1^2*u2*v1^2 + ... (12 terms) char set produced: [4 v1 2] [3 v2 1] [2 x1 1] [3 y1 1] [2 x2 1] [6 y2 1] [2 x3 1] [1 y3 1] pseudo-remainder: [12 v2 2] = -v2^2*u1*v1 + ... (11 terms) pseudo-remainder: [13 v1 2] = -2*u1^2*u2*v1^2 + ... (12 terms) char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] `The theorem is true under the following subsidiary conditions:` . the three points B, C and D are not collinear . the line BC is not perpendicular to the line CD . 2*u1-u3 <> 0 . u2+u1-u3 <> 0 . -v1^2-u1*u3+u1*u2 <> 0 . the line CD is not perpendicular to the line DE . the line BF is not perpendicular to the line DC . the three points C, D and G are not collinear . -u2*x1+2*u1*u2-u1*x1-u1*u3+u3*x1 <> 0 . -u2*y1-v1*u2-u1*y1+u1*v1+u3*y1 <> 0 QED.
