Theorem([arbitrary(B,C,A), perpfoot(B,C,A,G,G), perpfoot(B,A,C,H,H), equidistance(D,A,B,D), midpoint(B,A,E), midpoint(C,A,F), equidistance(D,A,D,C), intersection(H,C,G,A,J), intersection(B,F,E,C,I)],[online(D,J,I)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J} are reassigned Theorem: If the points B, C, and A are arbitrary, G is the perpendicular foot of the line BC to the line AG, H is the perpendicular foot of the line BA to the line CH, the distance between D and A is equal to the distance between B and D, E is the midpoint of B and A, F is the midpoint of C and A, the distance between D and A is equal to the distance between D and C, the two lines HC and GA intersect at J, and `the two lines BF and EC intersect at ` || (I) , then `the point ` || (I) || ` is on the line ` || D || J . Proof: char set produced: [1 x1 1] [1 y1 1] [4 x2 1] [3 y2 1] [3 x3 1] [4 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [8 x6 1] [4 y6 1] [8 x7 1] [4 y7 1] char set recomputed: [1 x1 1] [1 y1 1] [4 x2 1] [3 y2 1] [3 x3 1] [4 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [1 x6 1] [3 y6 1] [3 x7 1] [4 y7 1] pseudo-remainder: [6 y7 1] = -x3*y7 + ... (5 terms) pseudo-remainder: [12 x7 1] = u1*y3*x7 + ... (11 terms) pseudo-remainder: [14 y6 1] = u1^2*y6 + ... (13 terms) pseudo-remainder: [11 x6 1] = u1^2*x6 + ... (10 terms) pseudo-remainder: [6 y3 1] = -v1*u1*y3 + ... (5 terms) pseudo-remainder: [8 x3 1] = 2*u1^2*x3 + ... (7 terms) `The theorem is true under the following subsidiary conditions:` . the line BA is non-isotropic . the line BC is non-isotropic . -2*u2+u1 <> 0 . the three points A, B and C are not collinear . the line AB is not perpendicular to the line BC QED.
Theorem([arbitrary(B,C,A), perpfoot(B,C,A,G,G), perpfoot(B,A,C,H,H), equidistance(D,A,B,D), midpoint(B,A,E), midpoint(C,A,F), intersection(H,C,G,A,J), intersection(B,F,E,C,I), online(D,J,I)],[equidistance(D,A,D,C)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J} are reassigned Theorem: If the points B, C, and A are arbitrary, G is the perpendicular foot of the line BC to the line AG, H is the perpendicular foot of the line BA to the line CH, the distance between D and A is equal to the distance between B and D, E is the midpoint of B and A, F is the midpoint of C and A, the two lines HC and GA intersect at J, `the two lines BF and EC intersect at ` || (I) , and `the point ` || (I) || ` is on the line ` || D || J , then the distance between D and A is equal to the distance between D and C. Proof: Status: used = 805, alloced = 3072, time = 4.555 char set produced: [1 x1 1] [1 y1 1] [4 x2 1] [3 y2 1] [47 x3 1] [4 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [8 x6 1] [4 y6 1] [8 x7 1] [4 y7 1] char set recomputed: [1 x1 1] [1 y1 1] [4 x2 1] [3 y2 1] [3 x3 2] [4 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [1 x6 1] [3 y6 1] [11 x7 1] [6 y7 1] pseudo-remainder: [4 y3 1] = -2*y3*v1 + ... (3 terms) pseudo-remainder: [4 x3 1] = 2*u1*x3 + ... (3 terms) pseudo-remainder: [3 y2 0] = -u1 + ... (2 terms) pseudo-remainder: [3 x2 0] = -u1 + ... (2 terms) pseudo-remainder: [3 y1 0] = -u1 + ... (2 terms) pseudo-remainder: [3 x1 0] = -u1 + ... (2 terms) the thoerem is possibly false: further decomposition in progress pseudo-remainder: [4 y3 1] = -2*y3*v1 + ... (3 terms) pseudo-remainder: [3 x3 1] = -2*x3*u2 + ... (2 terms) char set produced: [1 u1 1] [1 x1 1] [1 y1 1] [1 x2 1] [1 y2 1] [2 x3 1] [2 y3 1] [1 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [1 x6 1] [2 x7 1] [2 y7 1] pseudo-remainder: [4 y3 1] = -2*y3*v1 + ... (3 terms) pseudo-remainder: [2 x3 1] = -2*x3*u2 + ... (1 terms) pseudo-remainder: [1 y2 0] = -u2^2 pseudo-remainder: [1 x2 0] = -u2^2 pseudo-remainder: [1 y1 0] = -u2^2 pseudo-remainder: [1 x1 0] = -u2^2 pseudo-remainder: [1 u1 0] = -u2^2 further decomposition in progress 4 pseudo-remainder: [4 y3 1] = -2*y3*v1 + ... (3 terms) pseudo-remainder: [3 x3 1] = 2*x3*u2^2 + ... (2 terms) pseudo-remainder: [2 v1 2] = -3*v1^2*u2 + ... (1 terms) pseudo-remainder: [1 u1 0] = u2^3 char set produced: [1 v1 1] [1 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] [2 x3 1] [2 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [1 y7 1] pseudo-remainder: [4 x3 1] = 2*x3*u2 + ... (3 terms) pseudo-remainder: [4 y2 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 x2 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 y1 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 x1 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 v1 2] = -v1^2 + ... (3 terms) further decomposition in progress 7 pseudo-remainder: [4 x5 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 y4 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x4 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x3 1] = 2*x3*u2 + ... (3 terms) pseudo-remainder: [4 y2 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 x2 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 y1 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 x1 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 v1 2] = -v1^2 + ... (3 terms) char set produced: [1 O 0] char set produced: [2 u2 1] [1 x1 1] [1 y1 1] [4 x2 1] [3 y2 1] [4 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [1 x6 1] [2 x7 1] [2 y7 1] pseudo-remainder: [4 y3 1] = -2*y3*v1 + ... (3 terms) pseudo-remainder: [4 y2 0] = -u1^2 + ... (3 terms) pseudo-remainder: [4 x2 0] = -u1^2 + ... (3 terms) pseudo-remainder: [4 y1 0] = -u1^2 + ... (3 terms) pseudo-remainder: [4 x1 0] = -u1^2 + ... (3 terms) pseudo-remainder: [4 u2 2] = u2^2 + ... (3 terms) further decomposition in progress 9 Status: used = 4040, alloced = 5506, time = 4.773000000000001 pseudo-remainder: [4 y3 1] = -2*y3*v1 + ... (3 terms) pseudo-remainder: [3 x3 1] = -4*v1^3*x3*u2 + ... (2 terms) pseudo-remainder: [3 y1 0] = -v1^3*u1^3 + ... (2 terms) pseudo-remainder: [3 u2 2] = -2*u1*u2^2 + ... (2 terms) char set produced: [3 v1 2] [1 x1 1] [1 y1 1] [2 x2 1] [2 y2 1] [3 x3 1] [3 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [1 x6 1] [3 y6 1] [3 x7 1] [3 y7 1] char set produced: [1 u1 1] [1 u2 1] [1 x2 1] [1 y2 1] [2 y3 1] [1 x4 1] [2 y4 1] [1 x5 1] [2 y5 1] [4 y6 1] [1 x7 1] [6 y7 1] pseudo-remainder: [4 y6 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 y5 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x5 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 y4 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x4 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 y3 1] = -2*y3*v1 + ... (3 terms) pseudo-remainder: [2 y2 0] = u2^2 + ... (1 terms) pseudo-remainder: [2 x2 0] = u2^2 + ... (1 terms) pseudo-remainder: [2 u2 2] = u2^2 + ... (1 terms) pseudo-remainder: [3 y3 1] = -2*y3*v1 + ... (2 terms) pseudo-remainder: [1 u2 2] = u2^2 char set produced: [1 u1 1] [1 v1 1] [1 x1 1] [1 y1 1] [1 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [4 y6 1] [8 x7 1] [1 y7 1] pseudo-remainder: [4 y5 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x5 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 y4 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x4 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 y1 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x1 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 v1 2] = v1^2 + ... (3 terms) pseudo-remainder: [2 u1 0] = -u2^2 + ... (1 terms) further decomposition in progress 10 pseudo-remainder: [4 y5 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x5 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 y4 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x4 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 y1 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x1 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 v1 2] = v1^2 + ... (3 terms) pseudo-remainder: [2 u1 0] = -u2^2 + ... (1 terms) char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [2 u2 1] [2 x2 1] [1 y2 1] [4 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [1 x6 1] [2 y6 1] [1 x7 1] [2 y7 1] pseudo-remainder: [4 y3 1] = -2*y3*v1 + ... (3 terms) pseudo-remainder: [4 y2 0] = -u1^2 + ... (3 terms) pseudo-remainder: [4 x2 0] = -u1^2 + ... (3 terms) pseudo-remainder: [4 u2 2] = u2^2 + ... (3 terms) char set produced: [2 u2 1] [1 v1 1] [1 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] [2 x3 1] [2 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [1 y7 1] pseudo-remainder: [4 x3 1] = 2*x3*u2 + ... (3 terms) pseudo-remainder: [4 v1 2] = -v1^2 + ... (3 terms) pseudo-remainder: [2 u2 2] = u2^2 + ... (1 terms) further decomposition in progress 7 pseudo-remainder: [4 x5 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 y4 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x4 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x3 1] = 2*x3*u2 + ... (3 terms) pseudo-remainder: [4 y2 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 x2 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 y1 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 x1 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 v1 2] = -v1^2 + ... (3 terms) pseudo-remainder: [2 u2 2] = u2^2 + ... (1 terms) char set produced: [2 u2 1] [1 v1 1] [1 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] [2 x3 1] [2 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [2 x7 1] [1 y7 1] pseudo-remainder: [4 x3 1] = 2*x3*u2 + ... (3 terms) pseudo-remainder: [4 v1 2] = -v1^2 + ... (3 terms) pseudo-remainder: [2 u2 2] = u2^2 + ... (1 terms) further decomposition in progress 7 pseudo-remainder: [4 x5 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 y4 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x4 0] = -u2^2 + ... (3 terms) pseudo-remainder: [4 x3 1] = 2*x3*u2 + ... (3 terms) pseudo-remainder: [4 y2 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 x2 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 y1 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 x1 0] = -u1*u2 + ... (3 terms) pseudo-remainder: [4 v1 2] = -v1^2 + ... (3 terms) pseudo-remainder: [2 u2 2] = u2^2 + ... (1 terms) char set produced: [2 u2 1] [2 x2 1] [1 y2 1] [4 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [1 x6 1] [2 y6 1] [1 x7 1] [2 y7 1] char set produced: [1 O 0] char set produced: [2 u2 1] [1 v1 1] [1 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] [2 x3 1] [2 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [2 x6 1] [2 x7 1] [1 y7 1] char set produced: [1 O 0] char set produced: [2 u2 1] [1 x1 1] [1 y1 1] [4 x2 1] [3 y2 1] [2 x3 1] [2 y3 1] [2 x4 1] [2 y4 1] [2 x5 1] [2 y5 1] [1 x6 1] [2 x7 1] [2 y7 1] pseudo-remainder: [4 y3 1] = -2*y3*v1 + ... (3 terms) pseudo-remainder: [2 x3 1] = -2*x3*u2 + ... (1 terms) pseudo-remainder: [2 u2 2] = -u2^2 + ... (1 terms) further decomposition in progress 4 pseudo-remainder: [4 y3 1] = -2*y3*v1 + ... (3 terms) pseudo-remainder: [3 x3 1] = 2*u1*u2*x3 + ... (2 terms) pseudo-remainder: [3 v1 2] = -v1^2*u1 + ... (2 terms) pseudo-remainder: [2 u2 2] = u1*u2^2 + ... (1 terms) char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [1 O 0] char set produced: [2 u2 1] [1 v1 1] [1 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] [2 x3 1] [2 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [2 x6 1] [2 x7 1] [1 y7 1] pseudo-remainder: [4 x3 1] = 2*x3*u2 + ... (3 terms) pseudo-remainder: [4 v1 2] = -v1^2 + ... (3 terms) pseudo-remainder: [2 u2 2] = u2^2 + ... (1 terms) further decomposition in progress 3 pseudo-remainder: [4 x3 1] = 2*x3*u2 + ... (3 terms) pseudo-remainder: [4 v1 2] = -v1^2 + ... (3 terms) pseudo-remainder: [2 u2 2] = u2^2 + ... (1 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: [2 u2 1] [1 v1 1] [1 x1 1] [1 y1 1] [2 x2 1] [1 y2 1] [2 x3 1] [1 y3 1] [2 x4 1] [1 y4 1] [2 x5 1] [1 y5 1] [2 x7 1] [1 y7 1] pseudo-remainder: [4 y3 1] = -2*y3*v1 + ... (3 terms) pseudo-remainder: [3 x3 1] = 2*x3*u2 + ... (2 terms) pseudo-remainder: [3 v1 2] = -v1^2 + ... (2 terms) pseudo-remainder: [2 u2 2] = u2^2 + ... (1 terms) further decomposition in progress 1 pseudo-remainder: [4 y3 1] = -2*y3*v1 + ... (3 terms) pseudo-remainder: [3 x3 1] = 2*x3*u2 + ... (2 terms) pseudo-remainder: [3 v1 2] = -v1^2 + ... (2 terms) pseudo-remainder: [2 u2 2] = u2^2 + ... (1 terms) 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 line BA is non-isotropic . the line BC is non-isotropic . y7 <> 0 . 2*u1-u2 <> 0 . -3*x7+u2 <> 0 . the three points A, B and C are not collinear . the line AB is not perpendicular to the line BC . the line AC is not perpendicular to the line BC . u1-2*x3 <> 0 . -3*x3+u2 <> 0 . the three points B, C and D are not collinear . the three points B, C and E are not collinear . the three points B, C and F are not collinear . the line BF is not perpendicular to the line BC . u1-2*x2 <> 0 . -x2+2*u1 <> 0 . the three points B, C and H are not collinear . the line BC is not perpendicular to the line CH . -2*x6+u1 <> 0 . the three points B, C and J are not collinear . -2*y6*x7+2*y3*x7-2*x6*y3+u1*y6 <> 0 . the line BC is not parallel to the line DJ . the line BC is not perpendicular to the line DJ . x2*y3+y2*u2-u2*y3-y2*x6 <> 0 . -x2*y3*x7+x2*x6*y3-y2*x6*x3-y2*u2*x7+u2*y3*x7-u2*x6*y3+y2*x6*x7+y2*u2*x3 <> 0 QED.
Theorem([arbitrary(B,A,C), perpfoot(B,C,A,G,G), perpfoot(B,A,C,H,H), midpoint(B,A,E), midpoint(C,A,F), equidistance(D,A,D,C), intersection(H,C,G,A,J), intersection(B,F,E,C,I), online(D,J,I)],[equidistance(D,A,B,D)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J} are reassigned Theorem: If the points B, A, and C are arbitrary, G is the perpendicular foot of the line BC to the line AG, H is the perpendicular foot of the line BA to the line CH, E is the midpoint of B and A, F is the midpoint of C and A, the distance between D and A is equal to the distance between D and C, the two lines HC and GA intersect at J, `the two lines BF and EC intersect at ` || (I) , and `the point ` || (I) || ` is on the line ` || D || J , then the distance between D and A is equal to the distance between B and D. Proof: char set produced: [4 x1 1] [3 y1 1] [1 x2 1] [1 y2 1] [3 x3 1] [1 y3 1] [2 x4 1] [2 y4 1] [130 x5 1] [4 y5 1] [8 x6 1] [4 y6 1] [8 x7 1] [4 y7 1] pseudo-remainder: [4 x5 1] = 2*u1*x5 + ... (3 terms) pseudo-remainder: [108 y4 1] = v1*u2^2*u1^2*x3*y4 + ... (107 terms) pseudo-remainder: [90 x4 1] = -2*v1^2*x2*u2^2*x4*u1 + ... (89 terms) pseudo-remainder: [68 y3 1] = -2*v1*x2*u2^2*u1^2*y3 + ... (67 terms) pseudo-remainder: [45 x3 1] = -v1^2*u2^2*u1^2*x3 + ... (44 terms) pseudo-remainder: [25 y2 1] = y2*u2^2*u1^3 + ... (24 terms) pseudo-remainder: [13 x2 1] = y1*x2*u2*u1^2 + ... (12 terms) pseudo-remainder: [6 y1 1] = -u1*u2*v1^2*y1 + ... (5 terms) pseudo-remainder: [8 x1 1] = -x1*u2*u1^3 + ... (7 terms) `The theorem is true under the following subsidiary conditions:` . the line BA is non-isotropic . the line BC is non-isotropic . the line BF is not parallel to the line EC . the line HC is not parallel to the line GA . the three points A, B and C are not collinear . the line AB is not perpendicular to the line BC . the line AB is not perpendicular to the line CE . the line AG is not perpendicular to the line AB . -v1*x2*u2^2*u1*y3+x2*u2^2*y1*v1*x4-x2*u2^2*y1*u1*v1-x2*u2^2*y1*y3*x4+x2*u2^2*y1*u1*y3-v1*x1*u2*u1*x3*y4+x1*y2*u2*u1*x3*y4+x1*y2*u2*v1*x3*x4-x1*y2*u2*u1*v1*x3-y1*x2*u2*u1*x3*y4-y1*x2*u2*v1*x3*x4+y1*x2*u2*u1*v1*x3+v1*x1*x2*u2*x3*y4+v1^2*x1*x2*u2*x4-v1^2*x1*x2*u2*u1+v1*x2*u2^2*y3*x4+v1^2*u2^2*x3*x4-v1^2*u2^2*u1*x3-u2*v1^3*x3*y4+u2*v1^3*x4*y1+v1^3*x1*x3*y4-v1^3*x2*y1*x4-u1*v1^2*x2*y1*y4+u1*u2*v1^2*y1*y2+u1*u2*v1^2*y1*y3-u1*u2*v1^2*y2*y4-u1*u2*v1^2*y3*y4+u1*v1^2*x1*y2*y4+u1*v1^2*x1*y3*y4-u1*v1^2*x2*y1*y3-u2*v1*x3*y1*y2*y4+u2*v1*x4*y1*y2*y3-u1*u2*v1*y1*y2*y3+u1*u2*v1*y2*y3*y4-u1*v1*x1*y2*y3*y4+u1*v1*x2*y1*y3*y4-v1*x1*x2*u2*y3*x4+v1*x1*x2*u2*u1*y3-u1*u2*v1^3*y1+u1*u2*v1^3*y4-u1*v1^3*x1*y4+u1*v1^3*x2*y1+u2*v1^2*x3*y1*y4+u2*v1^2*x3*y2*y4-u2*v1^2*x4*y1*y2-u2*v1^2*x4*y1*y3-v1^2*x1*x3*y2*y4+v1^2*x2*y1*y3*x4-v1*x2*u2^2*x3*y4-v1^2*x2*u2^2*x4+v1^2*x2*u2^2*u1+x2*u2^2*y1*x3*y4-v1^2*x1*u2*x3*x4+v1^2*x1*u2*u1*x3+v1*u2^2*u1*x3*y4-y2*u2^2*u1*x3*y4-y2*u2^2*v1*x3*x4+y2*u2^2*u1*v1*x3 <> 0 QED.
