Theorem([arbitrary(D,C,E), oncircle(D,C,E,G), oncircle(D,C,E,B), oncircle(D,C,E,F), online(D,I,E), online(H,B,D), online(I,C,G), online(B,J,C), intersection(E,J,H,G,F)],[online(H,J,I)]) Warning: the coordinates of the points from {I, B, C, D, E, F, G, H, J} are reassigned Theorem: If the points D, C, and E are arbitrary, the point G is on the circumcircle of the triangle DCE, the point B is on the circumcircle of the triangle DCE, the point F is on the circumcircle of the triangle DCE, `the point E is on the line D` || (I) , the point D is on the line HB, `the point G is on the line ` || (I) || C , the point C is on the line BJ, and the two lines EJ and HG intersect at F, then `the point ` || (I) || ` is on the line ` || H || J . Proof: char set produced: [7 y1 2] [7 y2 2] [7 y3 2] [6 x4 1] [3 y4 1] [12 x5 1] [4 y5 1] [8 x6 1] [4 y6 1] pseudo-remainder: [6 y6 1] = -y6*x4 + ... (5 terms) pseudo-remainder: [12 x6 1] = -u2*x6*y4 + ... (11 terms) pseudo-remainder: [38 y5 1] = -u2^2*v1*x3*y5 + ... (37 terms) pseudo-remainder: [38 x5 1] = u1*u2*v1*y2*x5 + ... (37 terms) pseudo-remainder: [161 y4 1] = y2*u1^2*x1*u2*v1*y4 + ... (160 terms) pseudo-remainder: [100 x4 1] = u1^2*y1*y2*v1*x2*x4 + ... (99 terms) pseudo-remainder: [84 y3 2] = u1^3*y1*v1*u2*x1*y3^2 + ... (83 terms) pseudo-remainder: [86 y2 2] = -u1*u2*v1^2*x1*y1*y2^2 + ... (85 terms) pseudo-remainder: [68 y1 2] = u1*u2*v1^2*x2*y1^2*y2 + ... (67 terms) Status: used = 626, alloced = 3072, time = 4.508 `The theorem is true under the following subsidiary conditions:` . the three points D, C and E are not collinear . the line CD is not perpendicular to the line DE . the line BC is not perpendicular to the line CD . the line BD is not perpendicular to the line CD . the line CG is not parallel to the line ED . the line BC is not parallel to the line EF . the line BD is not parallel to the line FG QED.
Theorem([arbitrary(C,D,E), oncircle(D,C,E,G), oncircle(D,C,E,B), oncircle(D,C,E,F), online(D,I,E), online(H,B,D), online(I,C,G), intersection(E,J,H,G,F), online(H,J,I)],[online(B,J,C)]) Warning: the coordinates of the points from {I, B, C, D, E, F, G, H, J} are reassigned Theorem: If the points C, D, and E are arbitrary, the point G is on the circumcircle of the triangle DCE, the point B is on the circumcircle of the triangle DCE, the point F is on the circumcircle of the triangle DCE, `the point E is on the line D` || (I) , the point D is on the line HB, `the point G is on the line ` || (I) || C , the two lines EJ and HG intersect at F, and `the point ` || (I) || ` is on the line ` || H || J , then the point C is on the line BJ. Proof: char set produced: [7 y1 2] [7 y2 2] [7 y3 2] [6 x4 1] [3 y4 1] [12 x5 1] [4 y5 1] [10 x6 1] [4 y6 1] pseudo-remainder: [4 y6 1] = -y6*u1 + ... (3 terms) pseudo-remainder: [8 x6 1] = -x6*v1*u1 + ... (7 terms) pseudo-remainder: [22 y5 1] = y5*x3^2*u1*v1 + ... (21 terms) pseudo-remainder: [38 x5 1] = -u1*u2*v1*y2*x5 + ... (37 terms) pseudo-remainder: [161 y4 1] = -y2*u2^2*x1*u1*v1*y4 + ... (160 terms) pseudo-remainder: [100 x4 1] = x4*v1^2*u1*u2*x1*y2 + ... (99 terms) pseudo-remainder: [84 y3 2] = u1^2*u2^2*y1*v1*x1*y3^2 + ... (83 terms) pseudo-remainder: [86 y2 2] = u1*u2*v1^2*x1*y1*y2^2 + ... (85 terms) pseudo-remainder: [68 y1 2] = u1*u2*v1^2*x2*y1^2*y2 + ... (67 terms) `The theorem is true under the following subsidiary conditions:` . the three points D, C and E are not collinear . the line CD is not perpendicular to the line DE . the line BD is not perpendicular to the line CD . the line CD is not perpendicular to the line EF . the line CG is not parallel to the line ED . x3*y4-y5*x3-y3*x4+x5*y3+x4*v1-v1*x5 <> 0 . the line BD is not parallel to the line FG QED.
Theorem([arbitrary(C,D,E), oncircle(D,C,E,G), oncircle(D,C,E,B), oncircle(D,C,E,F), online(D,I,E), online(H,B,D), online(B,J,C), intersection(E,J,H,G,F), online(H,J,I)],[online(I,C,G)]) Warning: the coordinates of the points from {I, B, C, D, E, F, G, H, J} are reassigned Theorem: If the points C, D, and E are arbitrary, the point G is on the circumcircle of the triangle DCE, the point B is on the circumcircle of the triangle DCE, the point F is on the circumcircle of the triangle DCE, `the point E is on the line D` || (I) , the point D is on the line HB, the point C is on the line BJ, the two lines EJ and HG intersect at F, and `the point ` || (I) || ` is on the line ` || H || J , then `the point G is on the line ` || (I) || C . Proof: char set produced: [7 y1 2] [7 y2 2] [7 y3 2] [100 x4 1] [3 y4 1] [12 x5 1] [4 y5 1] [8 x6 1] [4 y6 1] pseudo-remainder: [4 y4 1] = -y4*u1 + ... (3 terms) pseudo-remainder: [6 x4 1] = x4*v1*u1 + ... (5 terms) pseudo-remainder: [84 y3 2] = -u1^2*u2^2*y1*v1*x1*y3^2 + ... (83 terms) pseudo-remainder: [86 y2 2] = -u1*u2*v1^2*x1*y1*y2^2 + ... (85 terms) pseudo-remainder: [68 y1 2] = -u1*u2*v1^2*x2*y1^2*y2 + ... (67 terms) `The theorem is true under the following subsidiary conditions:` . the three points D, C and E are not collinear . the line CD is not perpendicular to the line DE . the line BC is not perpendicular to the line CD . the line BD is not perpendicular to the line CD . the line BC is not parallel to the line EF . v1^2*y2*x1*x2*x3-v1*x2^2*y1*x3*y3-u1*v1*x1*y3^2*x2+u1*v1^2*x1*y3*x2-u1*v1^2*y3*x3*x2-u1*v1^2*y2*x1*x3-v1^2*u2*y2*x1*x2+u1*v1^2*y2*x1*u2-u2^2*y1*y2^2*x3-u2^2*y3^2*x2*y2+u2^2*y3*y2^2*x3-y1*x3^2*y2*u2*v1+x1*y3^2*x2*y2*u2-x1*y3*y2^2*x3*u2-u1*u2*v1*x1*y2^2+u1*u2*v1*x3*y2^2+u1*u2*x1*y2^2*y3-u1*u2*x1*y2*y3^2+u1*v1*x1*x3*y2^2+v1*y1*x3*u2*y3*x2-v1*u1*u2*x3*y1*y3+u1*u2*x3*y1*y2*y3-u1*v1*x2*x3*y1*y2+u1*v1*x2*x3*y2*y3-y2^2*u1*x3*u2*y3+u1*y3^2*x2*y2*u2+u2^2*y1*v1*x3*y2+u2^2*y1*x2*y3*y2-u2^2*y3*v1*x3*y2-y1*x3*x2*y3*y2*u2+x1*y3*y2*u2*v1*x3+v1^2*x3*y2*u2*x2-v1^2*y2*u1*u2*x3-v1*x1*y3^2*u2*x2+v1*u1*u2*x1*y3^2+v1^2*x1*y3*u2*x2-v1^2*y3*u2*x3*x2-v1^2*u1*u2*x1*y3+v1^2*u1*u2*x3*y3+u1*v1*y1*x3*y3*x2+y1*x3^2*y2^2*u2-u1*v1*x3^2*y2^2+v1*x2^2*x1*y3^2+v1^2*x2^2*y3*x3-v1^2*y2*x3^2*x2-v1^2*x2^2*x1*y3+u1*v1^2*y2*x3^2-x2*x1*y3*y2*v1*x3-x2*y3*y2*u1*u2*v1-u1*y1*x2*y3*y2*u2+u1*y1*x2*v1*y2*u2-u2^2*y1*y2*x2*v1+u2^2*y3*y2*x2*v1+x2*y1*x3^2*y2*v1 <> 0 . the line BD is not parallel to the line FG QED.
Theorem([arbitrary(D,C,E), oncircle(D,C,E,G), oncircle(D,C,E,B), oncircle(D,C,E,F), online(D,I,E), online(I,C,G), online(B,J,C), intersection(E,J,H,G,F), online(H,J,I)],[online(H,B,D)]) Warning: the coordinates of the points from {I, B, C, D, E, F, G, H, J} are reassigned Theorem: If the points D, C, and E are arbitrary, the point G is on the circumcircle of the triangle DCE, the point B is on the circumcircle of the triangle DCE, the point F is on the circumcircle of the triangle DCE, `the point E is on the line D` || (I) , `the point G is on the line ` || (I) || C , the point C is on the line BJ, the two lines EJ and HG intersect at F, and `the point ` || (I) || ` is on the line ` || H || J , then the point D is on the line HB. Proof: char set produced: [7 y1 2] [7 y2 2] [7 y3 2] [6 x4 1] [3 y4 1] [8 x5 1] [4 y5 1] [16 x6 1] [6 y6 1] pseudo-remainder: [4 y6 1] = y6*u1 + ... (3 terms) pseudo-remainder: [12 x6 1] = -x6*y1*u1 + ... (11 terms) pseudo-remainder: [60 y5 1] = x1^2*y5*y2*u1 + ... (59 terms) pseudo-remainder: [56 x5 1] = u2*y1*x5*y2*u1 + ... (55 terms) pseudo-remainder: [159 y4 1] = -y2*u2^2*x1*u1*v1*y4 + ... (158 terms) pseudo-remainder: [100 x4 1] = -u1^2*y1*y2*v1*x2*x4 + ... (99 terms) pseudo-remainder: [84 y3 2] = -u1^3*y1*v1*u2*x1*y3^2 + ... (83 terms) pseudo-remainder: [86 y2 2] = u1*u2*v1^2*x1*y1*y2^2 + ... (85 terms) pseudo-remainder: [68 y1 2] = -u1*u2*v1^2*x2*y1^2*y2 + ... (67 terms) `The theorem is true under the following subsidiary conditions:` . the three points D, C and E are not collinear . the line CD is not perpendicular to the line DE . the line BC is not perpendicular to the line CD . the line CG is not parallel to the line ED . the line BC is not parallel to the line EF . the line CD is not perpendicular to the line FG . y5*x3-x3*y4-x1*y5+y4*x1-x4*y1+y1*x5+y3*x4-x5*y3 <> 0 QED.
Theorem([arbitrary(D,E,C), oncircle(D,C,E,G), oncircle(D,C,E,B), oncircle(D,C,E,F), online(H,B,D), online(I,C,G), online(B,J,C), intersection(E,J,H,G,F), online(H,J,I)],[online(D,I,E)]) Warning: the coordinates of the points from {I, B, C, D, E, F, G, H, J} are reassigned Theorem: If the points D, E, and C are arbitrary, the point G is on the circumcircle of the triangle DCE, the point B is on the circumcircle of the triangle DCE, the point F is on the circumcircle of the triangle DCE, the point D is on the line HB, `the point G is on the line ` || (I) || C , the point C is on the line BJ, the two lines EJ and HG intersect at F, and `the point ` || (I) || ` is on the line ` || H || J , then `the point E is on the line D` || (I) . Proof: char set produced: [7 y1 2] [7 y2 2] [7 y3 2] [12 x4 1] [4 y4 1] [36 x5 1] [4 y5 1] [8 x6 1] [4 y6 1] pseudo-remainder: [2 y5 1] = y5*u1 + ... (1 terms) pseudo-remainder: [3 x5 1] = -v1*x5 + ... (2 terms) pseudo-remainder: [20 y4 1] = x1^2*v1^2*u2*y4 + ... (19 terms) pseudo-remainder: [36 x4 1] = x4*v1^2*u1*u2*y3 + ... (35 terms) pseudo-remainder: [100 y3 2] = -u2*u1^2*y1*v1*x1*y3^2 + ... (99 terms) pseudo-remainder: [86 y2 2] = -u1*u2*v1^2*x1*y1*y2^2 + ... (85 terms) pseudo-remainder: [68 y1 2] = -u1*u2*v1^2*x2*y1^2*y2 + ... (67 terms) `The theorem is true under the following subsidiary conditions:` . the three points D, C and E are not collinear . the line BC is not perpendicular to the line DE . the line BD is not perpendicular to the line DE . the line CG is not perpendicular to the line ED Status: used = 2855, alloced = 5249, time = 4.710999999999999 . the line BC is not parallel to the line EF . the line BD is not parallel to the line FG . u2*v1*y2*x4+y1*x2*v1*x3-y1*x2*y3*x4+u2*y1*x2*y3-u2*y1*x2*v1-v1^2*u2*x4+x2*y3*x4*v1+v1^2*x3*x4-x1*x2*y3*v1+u2*x2*v1^2+y1*v1*u2*x4+x4*y1*y2*x3-y1*x3*x4*v1-v1*x3*y2*x4-x1*v1*u2*y4+x1*x3*y4*v1+x1*u2*y3*v1-u2*y3*x2*v1+u2*x1*y4*y2-u2*y2*x4*y1+x1*y4*x2*y3-y3*y2*u2*x1-x3*y4*y2*x1-v1^2*x3*x2 <> 0 QED.
Theorem([arbitrary(D,C,E), oncircle(D,C,E,G), oncircle(D,C,E,B), online(D,I,E), online(H,B,D), online(I,C,G), online(B,J,C), intersection(E,J,H,G,F), online(H,J,I)],[oncircle(D,C,E,F)]) Warning: the coordinates of the points from {I, B, C, D, E, F, G, H, J} are reassigned Theorem: If the points D, C, and E are arbitrary, the point G is on the circumcircle of the triangle DCE, the point B is on the circumcircle of the triangle DCE, `the point E is on the line D` || (I) , the point D is on the line HB, `the point G is on the line ` || (I) || C , the point C is on the line BJ, the two lines EJ and HG intersect at F, and `the point ` || (I) || ` is on the line ` || H || J , then the point F is on the circumcircle of the triangle DCE. Proof: char set produced: [7 y1 2] [7 y2 2] [6 x3 1] [3 y3 1] [4 y4 1] [12 x5 1] [4 y5 1] [10 x6 1] [6 y6 1] pseudo-remainder: [12 y6 2] = y6^2*v1*u1 + ... (11 terms) pseudo-remainder: [38 x6 2] = x1^2*x6^2*v1 + ... (37 terms) pseudo-remainder: [272 y5 2] = x1^4*y5^2*u1*v1*u2 + ... (271 terms) pseudo-remainder: [414 x5 2] = -u2^2*u1*v1^2*x1*x5^2*y1 + ... (413 terms) pseudo-remainder: [3882 y4 4] = u1*u2^5*v1*x1*x3*y4^4 + ... (3881 terms) pseudo-remainder: [567 y3 2] = u1^5*u2^3*v1^3*x1^2*y3^2 + ... (566 terms) pseudo-remainder: [602 x3 2] = y2^2*u1^6*u2*v1^3*x1^2*x3^2 + ... (601 terms) pseudo-remainder: [914 y2 6] = u1^7*u2^2*v1^3*x1^2*y2^6 + ... (913 terms) pseudo-remainder: [39 y1 3] = u1^2*u2*v1^6*x1*y1^3 + ... (38 terms) pseudo-remainder: [39 y1 3] = u1^6*u2^5*v1^2*x1*y1^3 + ... (38 terms) pseudo-remainder: [39 y1 3] = -u1^6*v1^3*u2^5*x1*y1^3 + ... (38 terms) pseudo-remainder: [45 y1 3] = -v1^5*u1^2*u2^2*x1*y1^3 + ... (44 terms) pseudo-remainder: [56 y1 3] = -u1^5*u2^5*v1^2*x1*y1^3 + ... (55 terms) pseudo-remainder: [58 y1 3] = -5*u1^4*u2^3*v1^4*x1*y1^3 + ... (57 terms) pseudo-remainder: [73 y1 3] = 2*u1^3*u2^3*v1^4*x1*y1^3 + ... (72 terms) pseudo-remainder: [75 y1 3] = u1^6*v1^3*u2^4*x1*y1^3 + ... (74 terms) pseudo-remainder: [77 y1 3] = 4*u1^3*v1^5*u2^2*x1*y1^3 + ... (76 terms) pseudo-remainder: [88 y1 3] = v1^3*u1^4*u2^4*x1*y1^3 + ... (87 terms) pseudo-remainder: [91 y1 3] = -2*u1^5*v1^3*u2^4*x1*y1^3 + ... (90 terms) pseudo-remainder: [875 y3 2] = -u1^5*u2*v1^2*y2*y3^2 + ... (874 terms) pseudo-remainder: [941 x3 2] = -v1^4*x3^2*u1^5*u2*y2 + ... (940 terms) pseudo-remainder: [1091 y2 6] = u1^4*u2^2*v1^3*x1^2*y2^6 + ... (1090 terms) pseudo-remainder: [47 y1 4] = -u1*v1^6*y1^4 + ... (46 terms) pseudo-remainder: [48 y1 4] = -u1*u2*v1^5*y1^4 + ... (47 terms) pseudo-remainder: [65 y1 4] = u1^5*u2^3*v1^3*y1^4 + ... (64 terms) pseudo-remainder: [65 y1 4] = -u1^5*u2^3*v1^4*y1^4 + ... (64 terms) pseudo-remainder: [76 y1 4] = -2*u1^4*u2^3*v1^3*y1^4 + ... (75 terms) pseudo-remainder: [90 y1 4] = 4*u1^2*u2*v1^5*y1^4 + ... (89 terms) pseudo-remainder: [96 y1 4] = -u1^2*u2^2*v1^4*y1^4 + ... (95 terms) pseudo-remainder: [109 y1 4] = u1^5*u2^2*v1^4*y1^4 + ... (108 terms) pseudo-remainder: [137 y1 4] = 3*u1^3*u2^2*v1^4*y1^4 + ... (136 terms) pseudo-remainder: [138 y1 4] = u1^3*u2^3*v1^3*y1^4 + ... (137 terms) pseudo-remainder: [146 y1 4] = -3*u1^4*u2^2*v1^4*y1^4 + ... (145 terms) pseudo-remainder: [1493 y3 2] = -2*u1^5*u2^3*v1^3*x1*y3^2 + ... (1492 terms) pseudo-remainder: [1388 x3 2] = -2*y2^2*u1^7*u2*v1^3*x1*x3^2 + ... (1387 terms) pseudo-remainder: [1575 y2 6] = -4*u1^7*u2^2*v1^3*x1^2*y2^6 + ... (1574 terms) pseudo-remainder: [39 y1 3] = u1^7*u2^5*v1^3*x1*y1^3 + ... (38 terms) pseudo-remainder: [39 y1 3] = -u1^7*u2^5*v1^2*x1*y1^3 + ... (38 terms) pseudo-remainder: [68 y1 4] = u1^2*u2*v1^6*y1^4 + ... (67 terms) pseudo-remainder: [71 y1 4] = u1^2*u2^2*v1^5*y1^4 + ... (70 terms) pseudo-remainder: [75 y1 4] = -u1^6*u2^4*v1^3*y1^4 + ... (74 terms) pseudo-remainder: [82 y1 4] = u1^6*u2^4*v1^4*y1^4 + ... (81 terms) pseudo-remainder: [98 y1 4] = 2*u1^5*u2^4*v1^3*y1^4 + ... (97 terms) pseudo-remainder: [113 y1 4] = u1^3*u2^3*v1^4*y1^4 + ... (112 terms) pseudo-remainder: [118 y1 4] = -4*u1^3*u2^2*v1^5*y1^4 + ... (117 terms) pseudo-remainder: [128 y1 4] = -u1^6*u2^3*v1^4*y1^4 + ... (127 terms) pseudo-remainder: [141 y1 4] = -3*u1^4*u2^3*v1^4*y1^4 + ... (140 terms) pseudo-remainder: [147 y1 4] = -u1^4*u2^4*v1^3*y1^4 + ... (146 terms) pseudo-remainder: [157 y1 4] = 3*u1^5*u2^3*v1^4*y1^4 + ... (156 terms) pseudo-remainder: [1825 y3 2] = -u1^5*u2^2*v1^3*y3^2 + ... (1824 terms) pseudo-remainder: [1710 x3 2] = v1^4*x3^2*u1^6*u2*y2 + ... (1709 terms) pseudo-remainder: [1710 y2 6] = -4*u1^5*u2^2*v1^3*x1^2*y2^6 + ... (1709 terms) pseudo-remainder: [47 y1 4] = u1*v1^6*y1^4 + ... (46 terms) pseudo-remainder: [48 y1 4] = u1*u2*v1^5*y1^4 + ... (47 terms) pseudo-remainder: [85 y1 4] = -u1^6*u2^3*v1^3*y1^4 + ... (84 terms) pseudo-remainder: [85 y1 4] = u1^6*u2^3*v1^4*y1^4 + ... (84 terms) pseudo-remainder: [89 y1 4] = u1^2*u2^2*v1^4*y1^4 + ... (88 terms) pseudo-remainder: [93 y1 4] = -3*u1^2*u2*v1^5*y1^4 + ... (92 terms) pseudo-remainder: [107 y1 4] = u1^5*u2^3*v1^3*y1^4 + ... (106 terms) pseudo-remainder: [127 y1 4] = -2*u1^3*u2^2*v1^4*y1^4 + ... (126 terms) pseudo-remainder: [131 y1 4] = -u1^6*u2^2*v1^4*y1^4 + ... (130 terms) pseudo-remainder: [140 y1 4] = -u1^3*u2^3*v1^3*y1^4 + ... (139 terms) pseudo-remainder: [154 y1 4] = 2*u1^4*v1^6*y1^4 + ... (153 terms) pseudo-remainder: [164 y1 4] = 2*u1^5*u2^2*v1^4*y1^4 + ... (163 terms) pseudo-remainder: [165 y1 4] = u1^4*u2^3*v1^3*y1^4 + ... (164 terms) pseudo-remainder: [2150 y3 2] = u1^5*u2^3*v1^3*y3^2 + ... (2149 terms) Status: used = 12551, alloced = 13334, time = 5.678 pseudo-remainder: [1937 x3 2] = v1^3*x3^2*y2^2*u1^7*u2 + ... (1936 terms) pseudo-remainder: [1908 y2 6] = 6*u1^6*u2^2*v1^3*x1^2*y2^6 + ... (1907 terms) pseudo-remainder: [68 y1 4] = -u1^2*u2*v1^5*y1^4 + ... (67 terms) pseudo-remainder: [74 y1 4] = u1^6*u2^4*v1^3*y1^4 + ... (73 terms) pseudo-remainder: [74 y1 4] = -u1^6*u2^4*v1^4*y1^4 + ... (73 terms) pseudo-remainder: [75 y1 4] = -u1^2*v1^6*y1^4 + ... (74 terms) pseudo-remainder: [105 y1 4] = u1^6*u2^3*v1^3*y1^4 + ... (104 terms) pseudo-remainder: [112 y1 4] = 2*u1^5*u2^4*v1^4*y1^4 + ... (111 terms) pseudo-remainder: [120 y1 4] = -u1^3*u2^2*v1^4*y1^4 + ... (119 terms) pseudo-remainder: [124 y1 4] = 4*u1^3*u2*v1^5*y1^4 + ... (123 terms) pseudo-remainder: [147 y1 4] = u1^4*u2^3*v1^3*y1^4 + ... (146 terms) pseudo-remainder: [147 y1 4] = u1^6*u2^2*v1^4*y1^4 + ... (146 terms) pseudo-remainder: [149 y1 4] = 3*u1^4*u2^2*v1^4*y1^4 + ... (148 terms) pseudo-remainder: [165 y1 4] = -2*u1^5*u2^3*v1^3*y1^4 + ... (164 terms) pseudo-remainder: [174 y1 4] = -3*u1^5*u2^2*v1^4*y1^4 + ... (173 terms) `The theorem is true under the following subsidiary conditions:` . the three points D, C and E are not collinear . the line EJ is not parallel to the line HG . the line CD is not perpendicular to the line DE . the line BC is not perpendicular to the line CD . the line BD is not perpendicular to the line CD . the line CG is not parallel to the line ED . -y2*x4+y2*x3-u2*y4+u2*y3+x2*y4-x2*y3 <> 0 . the line CD is not perpendicular to the line GH QED.
Theorem([arbitrary(D,C,E), oncircle(D,C,E,G), oncircle(D,C,E,F), online(D,I,E), online(H,B,D), online(I,C,G), online(B,J,C), intersection(E,J,H,G,F), online(H,J,I)],[oncircle(D,C,E,B)]) Warning: the coordinates of the points from {I, B, C, D, E, F, G, H, J} are reassigned Theorem: If the points D, C, and E are arbitrary, the point G is on the circumcircle of the triangle DCE, the point F is on the circumcircle of the triangle DCE, `the point E is on the line D` || (I) , the point D is on the line HB, `the point G is on the line ` || (I) || C , the point C is on the line BJ, the two lines EJ and HG intersect at F, and `the point ` || (I) || ` is on the line ` || H || J , then the point B is on the circumcircle of the triangle DCE. Proof: char set produced: [7 y1 2] [7 y2 2] [6 x3 1] [3 y3 1] [6 y4 1] [38 x5 1] [4 y5 1] [10 x6 1] [4 y6 1] pseudo-remainder: [12 y5 2] = y5^2*v1*u1 + ... (11 terms) pseudo-remainder: [23 x5 2] = x5^2*v1*u1^2 + ... (22 terms) pseudo-remainder: [1271 y4 4] = u1^4*u2^2*v1*x2^2*y4^4 + ... (1270 terms) pseudo-remainder: [645 y3 2] = -u1*u2^2*v1^2*x1^4*x2^2*y2*y3^2 + ... (644 terms) pseudo-remainder: [709 x3 2] = u1^3*u2*v1^3*x1^4*x3^2*y2^2 + ... (708 terms) pseudo-remainder: [1167 y2 6] = u1^4*u2^2*v1^3*x1^4*y2^6 + ... (1166 terms) pseudo-remainder: [39 y1 3] = -u1^5*u2^6*v1*x1^3*y1^3 + ... (38 terms) pseudo-remainder: [39 y1 3] = u1^5*u2^6*v1^2*x1^3*y1^3 + ... (38 terms) pseudo-remainder: [73 y1 4] = 3*u1^4*u2^5*v1^2*x1^2*y1^4 + ... (72 terms) pseudo-remainder: [87 y1 6] = 2*u1*u2*v1^6*y1^6 + ... (86 terms) pseudo-remainder: [90 y1 6] = -u1*u2^2*v1^5*y1^6 + ... (89 terms) pseudo-remainder: [96 y1 4] = -3*u1^4*u2^5*v1^3*x1^2*y1^4 + ... (95 terms) pseudo-remainder: [102 y1 5] = -3*u1^3*u2^4*v1^3*x1*y1^5 + ... (101 terms) pseudo-remainder: [133 y1 6] = u1^2*u2^3*v1^4*y1^6 + ... (132 terms) pseudo-remainder: [144 y1 5] = 3*u1^3*u2^4*v1^4*x1*y1^5 + ... (143 terms) pseudo-remainder: [160 y1 6] = u1^2*u2^2*v1^5*y1^6 + ... (159 terms) pseudo-remainder: [174 y1 6] = -u1^2*u2^3*v1^5*y1^6 + ... (173 terms) pseudo-remainder: [851 y3 2] = u1*u2*v1^2*x1^3*y1*y3^2 + ... (850 terms) pseudo-remainder: [752 x3 2] = u1^3*u2*v1^2*x1*x3^2*y1^3 + ... (751 terms) pseudo-remainder: [1129 y2 6] = u1^5*u2^2*v1^3*y2^6 + ... (1128 terms) pseudo-remainder: [40 y1 3] = -u1^2*u2*v1^6*y1^3 + ... (39 terms) pseudo-remainder: [41 y1 3] = -u1^2*u2^2*v1^5*y1^3 + ... (40 terms) pseudo-remainder: [93 y1 4] = -4*u1^2*u2*v1^6*y1^4 + ... (92 terms) pseudo-remainder: [94 y1 4] = 3*u1^2*u2^2*v1^5*y1^4 + ... (93 terms) pseudo-remainder: [116 y1 6] = u1^3*u2^3*v1^4*y1^6 + ... (115 terms) pseudo-remainder: [116 y1 6] = -u1^3*u2^3*v1^5*y1^6 + ... (115 terms) pseudo-remainder: [122 y1 6] = 2*u1^2*u2*v1^6*y1^6 + ... (121 terms) pseudo-remainder: [160 y1 5] = 5*u1^2*u2*v1^6*y1^5 + ... (159 terms) pseudo-remainder: [170 y1 5] = 3*u1^2*u2^2*v1^5*y1^5 + ... (169 terms) pseudo-remainder: [191 y1 6] = u1^3*u2^2*v1^5*y1^6 + ... (190 terms) pseudo-remainder: [213 y1 6] = -u1^2*u2^2*v1^5*y1^6 + ... (212 terms) pseudo-remainder: [1371 y3 2] = u1^2*u2*v1^2*x1^4*x2*y2*y3^2 + ... (1370 terms) pseudo-remainder: [1180 x3 2] = 2*u1^4*u2*v1^3*x1^3*x3^2*y1*y2 + ... (1179 terms) pseudo-remainder: [1706 y2 6] = -4*u1^5*u2^2*v1^3*x1^3*y2^6 + ... (1705 terms) pseudo-remainder: [39 y1 3] = u1^6*u2^6*v1*x1^3*y1^3 + ... (38 terms) pseudo-remainder: [39 y1 3] = -u1^6*u2^6*v1^2*x1^3*y1^3 + ... (38 terms) pseudo-remainder: [84 y1 4] = -6*u1^5*u2^5*v1^2*x1^2*y1^4 + ... (83 terms) pseudo-remainder: [93 y1 5] = -3*u1^2*u2^2*v1^5*y1^5 + ... (92 terms) pseudo-remainder: [94 y1 5] = -5*u1^2*u2*v1^6*y1^5 + ... (93 terms) pseudo-remainder: [100 y1 4] = 6*u1^5*u2^5*v1^3*x1^2*y1^4 + ... (99 terms) pseudo-remainder: [120 y1 5] = 9*u1^4*u2^4*v1^3*x1*y1^5 + ... (119 terms) pseudo-remainder: [160 y1 5] = -9*u1^4*u2^4*v1^4*x1*y1^5 + ... (159 terms) pseudo-remainder: [166 y1 6] = -8*u1^2*u2*v1^6*y1^6 + ... (165 terms) pseudo-remainder: [180 y1 6] = 4*u1^2*u2^2*v1^5*y1^6 + ... (179 terms) pseudo-remainder: [192 y1 6] = -4*u1^3*u2^3*v1^4*y1^6 + ... (191 terms) pseudo-remainder: [231 y1 6] = 4*u1^3*u2^3*v1^5*y1^6 + ... (230 terms) pseudo-remainder: [236 y1 6] = -4*u1^3*u2^2*v1^5*y1^6 + ... (235 terms) pseudo-remainder: [1568 y3 2] = -u1^2*u2*v1^2*x1^3*y1*y3^2 + ... (1567 terms) pseudo-remainder: [1228 x3 2] = -u1^4*u2*v1^2*x1*x3^2*y1^3 + ... (1227 terms) pseudo-remainder: [1740 y2 6] = -4*u1^5*u2^2*v1^3*x1*y2^6 + ... (1739 terms) pseudo-remainder: [40 y1 3] = u1^2*u2*v1^6*y1^3 + ... (39 terms) pseudo-remainder: [41 y1 3] = u1^2*u2^2*v1^5*y1^3 + ... (40 terms) pseudo-remainder: [100 y1 4] = 8*u1^2*u2*v1^6*y1^4 + ... (99 terms) pseudo-remainder: [102 y1 4] = -6*u1^2*u2^2*v1^5*y1^4 + ... (101 terms) pseudo-remainder: [111 y1 5] = -3*u1^4*u2^4*v1^4*x1*y1^5 + ... (110 terms) pseudo-remainder: [111 y1 5] = 3*u1^4*u2^4*v1^3*x1*y1^5 + ... (110 terms) pseudo-remainder: [160 y1 6] = -4*u1^3*u2^3*v1^4*y1^6 + ... (159 terms) pseudo-remainder: [169 y1 5] = -9*u1^2*u2^2*v1^5*y1^5 + ... (168 terms) pseudo-remainder: [175 y1 5] = -15*u1^2*u2*v1^6*y1^5 + ... (174 terms) pseudo-remainder: [205 y1 6] = 4*u1^3*u2^3*v1^5*y1^6 + ... (204 terms) pseudo-remainder: [213 y1 6] = -8*u1^2*u2*v1^6*y1^6 + ... (212 terms) pseudo-remainder: [242 y1 6] = 4*u1^2*u2^2*v1^5*y1^6 + ... (241 terms) pseudo-remainder: [259 y1 6] = -4*u1^3*u2^2*v1^5*y1^6 + ... (258 terms) pseudo-remainder: [1670 y3 2] = -u1^2*u2*v1^2*x1^4*y2*y3^2 + ... (1669 terms) pseudo-remainder: [1364 x3 2] = u1^4*u2*v1^3*x1^2*x3^2*y1^2 + ... (1363 terms) pseudo-remainder: [1924 y2 6] = 6*u1^5*u2^2*v1^3*x1^2*y2^6 + ... (1923 terms) pseudo-remainder: [72 y1 4] = -4*u1^2*u2*v1^6*y1^4 + ... (71 terms) pseudo-remainder: [79 y1 4] = 3*u1^2*u2^2*v1^5*y1^4 + ... (78 terms) pseudo-remainder: [81 y1 4] = -3*u1^5*u2^5*v1^3*x1^2*y1^4 + ... (80 terms) pseudo-remainder: [81 y1 4] = 3*u1^5*u2^5*v1^2*x1^2*y1^4 + ... (80 terms) pseudo-remainder: [129 y1 5] = -9*u1^4*u2^4*v1^3*x1*y1^5 + ... (128 terms) pseudo-remainder: [151 y1 5] = 9*u1^2*u2^2*v1^5*y1^5 + ... (150 terms) pseudo-remainder: [154 y1 5] = 15*u1^2*u2*v1^6*y1^5 + ... (153 terms) pseudo-remainder: [157 y1 5] = 9*u1^4*u2^4*v1^4*x1*y1^5 + ... (156 terms) pseudo-remainder: [206 y1 6] = 12*u1^2*u2*v1^6*y1^6 + ... (205 terms) pseudo-remainder: [211 y1 6] = 6*u1^3*u2^3*v1^4*y1^6 + ... (210 terms) pseudo-remainder: [227 y1 6] = -6*u1^2*u2^2*v1^5*y1^6 + ... (226 terms) pseudo-remainder: [239 y1 6] = -6*u1^3*u2^3*v1^5*y1^6 + ... (238 terms) pseudo-remainder: [266 y1 6] = 6*u1^3*u2^2*v1^5*y1^6 + ... (265 terms) `The theorem is true under the following subsidiary conditions:` . the three points D, C and E are not collinear . the line CD is not perpendicular to the line DE . the line CD is not perpendicular to the line EF . the line CG is not parallel to the line ED . the line CD is not perpendicular to the line DH . the line CD is not perpendicular to the line FG . x2*y3-x2*y4-y2*x3+y2*x4+v1*x3-x4*v1 <> 0 . -u2*y3*x2*y4+u2*x3*y2*y4-u1*v1*x2*y4-x3*y4*y2*u1+x3*y4*u1*v1+v1*x3*x2*y4+y3*x4*y2*u1-x2*y3*x4*v1-y4^2*x2*x3+y4^2*x2*u2+y4*x2*y3*x4-y2*y3*x4^2+v1*y3*x4^2+u1*x2*y3*v1-x4*x3*y4*v1-u1*v1*y3*x4-u2*v1*x3*y4+y4*v1*u2*x4-y4*y2*x4*u2+x4*y2*x3*y4 <> 0 QED.
Theorem([arbitrary(D,C,E), oncircle(D,C,E,B), oncircle(D,C,E,F), online(D,I,E), online(H,B,D), online(I,C,G), online(B,J,C), intersection(E,J,H,G,F), online(H,J,I)],[oncircle(D,C,E,G)]) Warning: the coordinates of the points from {I, B, C, D, E, F, G, H, J} are reassigned Theorem: If the points D, C, and E are arbitrary, the point B is on the circumcircle of the triangle DCE, the point F is on the circumcircle of the triangle DCE, `the point E is on the line D` || (I) , the point D is on the line HB, `the point G is on the line ` || (I) || C , the point C is on the line BJ, the two lines EJ and HG intersect at F, and `the point ` || (I) || ` is on the line ` || H || J , then the point G is on the circumcircle of the triangle DCE. Proof: char set produced: [7 y1 2] [7 y2 2] [3 y3 1] [38 x4 1] [4 y4 1] [12 x5 1] [4 y5 1] [8 x6 1] [4 y6 1] pseudo-remainder: [12 y5 2] = y5^2*v1*u1 + ... (11 terms) pseudo-remainder: [23 x5 2] = x5^2*v1*u2^2 + ... (22 terms) pseudo-remainder: [268 y4 2] = u2^5*y4^2*u1*v1 + ... (267 terms) pseudo-remainder: [426 x4 2] = y3*x4^2*y2*u1^3*u2*v1 + ... (425 terms) pseudo-remainder: [10557 y3 4] = u1^5*u2^4*v1*x2*y1^2*y3^4 + ... (10556 terms) pseudo-remainder: [832 y2 4] = -u1^7*u2^4*v1^3*y2^4 + ... (831 terms) pseudo-remainder: [72 y1 4] = -u1*u2^3*v1^4*y1^4 + ... (71 terms) pseudo-remainder: [81 y1 4] = -2*u1*u2^2*v1^5*y1^4 + ... (80 terms) pseudo-remainder: [84 y1 4] = -v1^2*u1^4*u2^5*y1^4 + ... (83 terms) pseudo-remainder: [84 y1 4] = u1^4*u2^5*v1^3*y1^4 + ... (83 terms) pseudo-remainder: [102 y1 4] = v1^2*u1^3*u2^5*y1^4 + ... (101 terms) pseudo-remainder: [107 y1 4] = 4*u1^2*u2^3*v1^4*y1^4 + ... (106 terms) pseudo-remainder: [125 y1 4] = -u1^2*u2^4*v1^3*y1^4 + ... (124 terms) pseudo-remainder: [138 y1 4] = -u1^4*u2^4*v1^3*y1^4 + ... (137 terms) pseudo-remainder: [160 y1 4] = 2*u1^3*u2^4*v1^3*y1^4 + ... (159 terms) pseudo-remainder: [898 y2 4] = -u1^6*v1^2*y2^4*u2*x1*y1 + ... (897 terms) pseudo-remainder: [78 y1 4] = -v1^4*u1^4*y1^4 + ... (77 terms) pseudo-remainder: [85 y1 4] = -2*v1^5*u1^3*y1^4 + ... (84 terms) pseudo-remainder: [103 y1 4] = u1^5*u2^4*v1^2*y1^4 + ... (102 terms) pseudo-remainder: [103 y1 4] = -u1^5*u2^4*v1^3*y1^4 + ... (102 terms) pseudo-remainder: [118 y1 4] = u1^6*u2^2*v1^2*y1^4 + ... (117 terms) pseudo-remainder: [132 y1 4] = -u1^5*u2*v1^3*y1^4 + ... (131 terms) pseudo-remainder: [137 y1 4] = u1^5*y1^4*v1^4 + ... (136 terms) pseudo-remainder: [171 y1 4] = -v1^3*u1^6*u2^2*y1^4 + ... (170 terms) pseudo-remainder: [179 y1 4] = v1^3*u1^6*u2*y1^4 + ... (178 terms) pseudo-remainder: [1086 y2 4] = u1^7*u2^3*v1^3*y2^4 + ... (1085 terms) pseudo-remainder: [99 y1 4] = -v1^4*u1^3*u2*y1^4 + ... (98 terms) pseudo-remainder: [111 y1 4] = -v1^5*u1^3*y1^4 + ... (110 terms) pseudo-remainder: [125 y1 4] = u1^5*u2^4*v1^2*y1^4 + ... (124 terms) pseudo-remainder: [125 y1 4] = -u1^5*u2^4*v1^3*y1^4 + ... (124 terms) pseudo-remainder: [137 y1 4] = u1^5*u2^3*v1^2*y1^4 + ... (136 terms) pseudo-remainder: [161 y1 4] = -v1^3*u1^4*u2^2*y1^4 + ... (160 terms) pseudo-remainder: [171 y1 4] = 2*u1^4*v1^4*u2*y1^4 + ... (170 terms) pseudo-remainder: [181 y1 4] = 6*u1^4*u2^4*v1^3*y1^4 + ... (180 terms) pseudo-remainder: [213 y1 4] = u1^5*u2^2*v1^3*y1^4 + ... (212 terms) pseudo-remainder: [1107 y2 4] = u1^7*v1^2*u2*x1*y1*y2^4 + ... (1106 terms) pseudo-remainder: [103 y1 4] = 3*v1^5*u1^3*y1^4 + ... (102 terms) pseudo-remainder: [104 y1 4] = v1^4*u1^4*y1^4 + ... (103 terms) pseudo-remainder: [128 y1 4] = -2*u1^5*u2^4*v1^2*y1^4 + ... (127 terms) pseudo-remainder: [128 y1 4] = 2*u1^5*u2^4*v1^3*y1^4 + ... (127 terms) pseudo-remainder: [143 y1 4] = -u1^6*u2^2*v1^2*y1^4 + ... (142 terms) pseudo-remainder: [156 y1 4] = u1^5*u2*v1^3*y1^4 + ... (155 terms) pseudo-remainder: [176 y1 4] = -u1^5*y1^4*v1^4 + ... (175 terms) pseudo-remainder: [192 y1 4] = v1^3*u1^6*u2^2*y1^4 + ... (191 terms) pseudo-remainder: [212 y1 4] = -v1^3*u1^6*u2*y1^4 + ... (211 terms) `The theorem is true under the following subsidiary conditions:` . the three points D, C and E are not collinear . u2-x3 <> 0 . the line CD is not perpendicular to the line DE . the line BC is not perpendicular to the line CD . the line BD is not perpendicular to the line CD . -u1*y1*y2*u2-y3*y2*u2*x1+x1*u2*y3*v1-y2*x1*y1*x3-y3*y2*u1*x1+y3*y2*x1^2+u2*y2*y1*x3+x1*u1*v1*y3+u1*y3*y2*u2-u1*y3*v1*u2+x2*y1^2*x3-u2*y1^2*x2-x1^2*v1*y3+x1*v1*y1*x3-u1*y1*x2*v1+u1*x2*y1*y3-u2*v1*y1*x3+u2*u1*v1*y1+u2*y1*x2*v1+y1*x1*u2*y2-u2*v1*x1*y1-x2*y1*x1*y3 <> 0 . the line BC is not parallel to the line EF . y2*u2-u2*y4-y2*x3+x3*y4-y3*x4+x2*y3 <> 0 QED.
