Theorem([arbitrary(A,B,C), perpfoot(B,C,A,G,G), perpfoot(A,C,B,I,I), perpfoot(B,A,C,H,H), midpoint(B,C,F), midpoint(B,A,D), online(B,I,J), midpoint(B,J,L), intersection(A,G,H,C,J), midpoint(C,A,E), midpoint(C,J,M), midpoint(A,J,K), oncircle(G,I,H,F), oncircle(G,I,H,K), oncircle(G,I,H,E), oncircle(G,I,H,M), oncircle(G,I,H,L)],[oncircle(G,I,H,D)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, K, L, M} are reassigned Theorem: If the points A, B, and C are arbitrary, G is the perpendicular foot of the line BC to the line AG, `` || (I) || ` is the perpendicular foot of the line ` || A || C || ` to the line ` || B || (I) , H is the perpendicular foot of the line BA to the line CH, F is the midpoint of B and C, D is the midpoint of B and A, `the point J is on the line B` || (I) , L is the midpoint of B and J, the two lines AG and HC intersect at J, E is the midpoint of C and A, M is the midpoint of C and J, K is the midpoint of A and J, `the point F is on the circumcircle of the triangle G` || (I) || H , `the point K is on the circumcircle of the triangle G` || (I) || H , `the point E is on the circumcircle of the triangle G` || (I) || H , `the point M is on the circumcircle of the triangle G` || (I) || H , and `the point L is on the circumcircle of the triangle G` || (I) || H , then `the point D is on the circumcircle of the triangle G` || (I) || H . Proof: Status: used = 731, alloced = 3072, time = 4.305 Status: used = 3098, alloced = 5407, time = 4.508 char set produced: [4 x1 1] [3 y1 1] [4 x2 1] [3 y2 1] [1 x3 1] [1 y3 1] [2 x4 1] [2 y4 1] [3 x5 1] [1 y5 1] [8 x6 1] [4 y6 1] [3 x7 1] [2 y7 1] [2 x8 1] [2 y8 1] [2 x9 1] [3 y9 1] [3 x10 1] [2 y10 1] pseudo-remainder: [48 y5 2] = -y2*y5^2*x1 + ... (47 terms) pseudo-remainder: [30 x5 2] = -y2*x5^2*x1 + ... (29 terms) pseudo-remainder: [54 y3 2] = 2*u1*y3^2*y1 + ... (53 terms) pseudo-remainder: [30 x3 2] = 2*u1*x3^2*y1 + ... (29 terms) pseudo-remainder: [14 y2 2] = -2*u1*y2^2*y1 + ... (13 terms) pseudo-remainder: [25 x2 2] = -2*u1^3*x2^2*y1 + ... (24 terms) pseudo-remainder: [12 y1 2] = 2*u1^5*v1*y1^2 + ... (11 terms) pseudo-remainder: [13 x1 2] = 2*u1*v1*u2^2*x1^2 + ... (12 terms) `The theorem is true under the following subsidiary conditions:` . the line AC is non-isotropic . the line BA 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 . -y2*x1+u1*y2+x2*y1-u2*y1 <> 0 . the line AG is not perpendicular to the line AB QED.
Theorem([arbitrary(A,B,C), perpfoot(B,C,A,G,G), perpfoot(A,C,B,I,I), perpfoot(B,A,C,H,H), midpoint(B,C,F), midpoint(B,A,D), online(B,I,J), midpoint(B,J,L), intersection(A,G,H,C,J), midpoint(C,A,E), midpoint(C,J,M), midpoint(A,J,K), oncircle(G,I,H,F), oncircle(G,I,H,K), oncircle(G,I,H,E), oncircle(G,I,H,M), oncircle(G,I,H,D)],[oncircle(G,I,H,L)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, K, L, M} are reassigned Theorem: If the points A, B, and C are arbitrary, G is the perpendicular foot of the line BC to the line AG, `` || (I) || ` is the perpendicular foot of the line ` || A || C || ` to the line ` || B || (I) , H is the perpendicular foot of the line BA to the line CH, F is the midpoint of B and C, D is the midpoint of B and A, `the point J is on the line B` || (I) , L is the midpoint of B and J, the two lines AG and HC intersect at J, E is the midpoint of C and A, M is the midpoint of C and J, K is the midpoint of A and J, `the point F is on the circumcircle of the triangle G` || (I) || H , `the point K is on the circumcircle of the triangle G` || (I) || H , `the point E is on the circumcircle of the triangle G` || (I) || H , `the point M is on the circumcircle of the triangle G` || (I) || H , and `the point D is on the circumcircle of the triangle G` || (I) || H , then `the point L is on the circumcircle of the triangle G` || (I) || H . Proof: char set produced: [4 x1 1] [3 y1 1] [4 x2 1] [3 y2 1] [1 x3 1] [1 y3 1] [2 x4 1] [2 y4 1] [3 x5 1] [1 y5 1] [8 x6 1] [4 y6 1] [3 x7 1] [2 y7 1] [2 x8 1] [2 y8 1] [2 x9 1] [3 y9 1] [3 x10 1] [2 y10 1] pseudo-remainder: [48 y7 2] = -y2*y7^2*x1 + ... (47 terms) pseudo-remainder: [48 x7 2] = -4*y2*x7^2*x1 + ... (47 terms) pseudo-remainder: [72 y6 2] = -y6^2*y2*x1 + ... (71 terms) pseudo-remainder: [198 x6 2] = -u1^2*x6^2*y2*x1 + ... (197 terms) pseudo-remainder: [794 y3 2] = -2*y1^2*u1^4*u2*y2*y3^2 + ... (793 terms) pseudo-remainder: [213 x3 2] = -2*u1^2*u2*x3^2*y1^2*y2 + ... (212 terms) pseudo-remainder: [88 y2 4] = -4*u1^2*u2*y1*y2^4 + ... (87 terms) pseudo-remainder: [198 x2 4] = 2*v1*x2^4*u1^5*y1^2 + ... (197 terms) pseudo-remainder: [110 y1 4] = -2*u1^10*u2*v1^3*y1^4 + ... (109 terms) pseudo-remainder: [47 x1 4] = -2*v1^3*u1^3*u2^3*x1^4 + ... (46 terms) `The theorem is true under the following subsidiary conditions:` . the line AC is non-isotropic . the line BA 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 . -y2*x1+u1*y2+x2*y1-u2*y1 <> 0 . the line AG is not perpendicular to the line AB QED.
Theorem([arbitrary(A,B,C), perpfoot(B,C,A,G,G), perpfoot(A,C,B,I,I), perpfoot(B,A,C,H,H), midpoint(B,C,F), midpoint(B,A,D), online(B,I,J), midpoint(B,J,L), intersection(A,G,H,C,J), midpoint(C,A,E), midpoint(C,J,M), midpoint(A,J,K), oncircle(G,I,H,F), oncircle(G,I,H,K), oncircle(G,I,H,E), oncircle(G,I,H,L), oncircle(G,I,H,D)],[oncircle(G,I,H,M)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, K, L, M} are reassigned Theorem: If the points A, B, and C are arbitrary, G is the perpendicular foot of the line BC to the line AG, `` || (I) || ` is the perpendicular foot of the line ` || A || C || ` to the line ` || B || (I) , H is the perpendicular foot of the line BA to the line CH, F is the midpoint of B and C, D is the midpoint of B and A, `the point J is on the line B` || (I) , L is the midpoint of B and J, the two lines AG and HC intersect at J, E is the midpoint of C and A, M is the midpoint of C and J, K is the midpoint of A and J, `the point F is on the circumcircle of the triangle G` || (I) || H , `the point K is on the circumcircle of the triangle G` || (I) || H , `the point E is on the circumcircle of the triangle G` || (I) || H , `the point L is on the circumcircle of the triangle G` || (I) || H , and `the point D is on the circumcircle of the triangle G` || (I) || H , then `the point M is on the circumcircle of the triangle G` || (I) || H . Proof: char set produced: [4 x1 1] [3 y1 1] [4 x2 1] [3 y2 1] [1 x3 1] [1 y3 1] [2 x4 1] [2 y4 1] [3 x5 1] [1 y5 1] [8 x6 1] [4 y6 1] [3 x7 1] [2 y7 1] [2 x8 1] [2 y8 1] [2 x9 1] [3 y9 1] [3 x10 1] [2 y10 1] pseudo-remainder: [48 y9 2] = -y2*y9^2*x1 + ... (47 terms) pseudo-remainder: [72 x9 2] = -4*y2*x9^2*x1 + ... (71 terms) pseudo-remainder: [72 y6 2] = -y6^2*y2*x1 + ... (71 terms) pseudo-remainder: [198 x6 2] = -u1^2*x6^2*y2*x1 + ... (197 terms) pseudo-remainder: [1106 y3 2] = -2*y1^2*u1^4*u2*y2*y3^2 + ... (1105 terms) pseudo-remainder: [318 x3 2] = -2*u1^2*u2*x3^2*y1^2*y2 + ... (317 terms) pseudo-remainder: [126 y2 4] = -2*u1^2*u2*y1*y2^4 + ... (125 terms) pseudo-remainder: [200 x2 4] = 2*v1*x2^4*u1^5*y1^2 + ... (199 terms) pseudo-remainder: [143 y1 4] = -2*u1^10*u2*v1^3*y1^4 + ... (142 terms) pseudo-remainder: [63 x1 4] = -2*u1^4*u2^4*v1^3*x1^4 + ... (62 terms) `The theorem is true under the following subsidiary conditions:` . the line AC is non-isotropic . the line BA 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 . -y2*x1+u1*y2+x2*y1-u2*y1 <> 0 . the line AG is not perpendicular to the line AB QED.
Theorem([arbitrary(A,B,C), perpfoot(B,C,A,G,G), perpfoot(A,C,B,I,I), perpfoot(B,A,C,H,H), midpoint(B,C,F), midpoint(B,A,D), online(B,I,J), midpoint(B,J,L), intersection(A,G,H,C,J), midpoint(C,A,E), midpoint(C,J,M), midpoint(A,J,K), oncircle(G,I,H,F), oncircle(G,I,H,K), oncircle(G,I,H,M), oncircle(G,I,H,L), oncircle(G,I,H,D)],[oncircle(G,I,H,E)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, K, L, M} are reassigned Theorem: If the points A, B, and C are arbitrary, G is the perpendicular foot of the line BC to the line AG, `` || (I) || ` is the perpendicular foot of the line ` || A || C || ` to the line ` || B || (I) , H is the perpendicular foot of the line BA to the line CH, F is the midpoint of B and C, D is the midpoint of B and A, `the point J is on the line B` || (I) , L is the midpoint of B and J, the two lines AG and HC intersect at J, E is the midpoint of C and A, M is the midpoint of C and J, K is the midpoint of A and J, `the point F is on the circumcircle of the triangle G` || (I) || H , `the point K is on the circumcircle of the triangle G` || (I) || H , `the point M is on the circumcircle of the triangle G` || (I) || H , `the point L is on the circumcircle of the triangle G` || (I) || H , and `the point D is on the circumcircle of the triangle G` || (I) || H , then `the point E is on the circumcircle of the triangle G` || (I) || H . Proof: char set produced: [4 x1 1] [3 y1 1] [4 x2 1] [3 y2 1] [1 x3 1] [1 y3 1] [2 x4 1] [2 y4 1] [3 x5 1] [1 y5 1] [8 x6 1] [4 y6 1] [3 x7 1] [2 y7 1] [2 x8 1] [2 y8 1] [2 x9 1] [3 y9 1] [3 x10 1] [2 y10 1] pseudo-remainder: [48 y8 2] = -y2*y8^2*x1 + ... (47 terms) pseudo-remainder: [48 x8 2] = -4*y2*x8^2*x1 + ... (47 terms) pseudo-remainder: [48 y3 2] = 2*u1*y3^2*y1 + ... (47 terms) pseudo-remainder: [30 x3 2] = 2*u1*x3^2*y1 + ... (29 terms) pseudo-remainder: [12 y2 2] = -2*u1*y2^2*y1 + ... (11 terms) pseudo-remainder: [15 x2 2] = -2*u1^3*x2^2*y1 + ... (14 terms) pseudo-remainder: [16 y1 2] = 2*u1^5*v1*y1^2 + ... (15 terms) pseudo-remainder: [18 x1 2] = 2*u1^2*v1*u2^2*x1^2 + ... (17 terms) `The theorem is true under the following subsidiary conditions:` . the line AC is non-isotropic . the line BA 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 . -y2*x1+u1*y2+x2*y1-u2*y1 <> 0 . the line AG is not perpendicular to the line AB QED.
Theorem([arbitrary(A,B,C), perpfoot(B,C,A,G,G), perpfoot(A,C,B,I,I), perpfoot(B,A,C,H,H), midpoint(B,C,F), midpoint(B,A,D), online(B,I,J), midpoint(B,J,L), intersection(A,G,H,C,J), midpoint(C,A,E), midpoint(C,J,M), midpoint(A,J,K), oncircle(G,I,H,F), oncircle(G,I,H,E), oncircle(G,I,H,M), oncircle(G,I,H,L), oncircle(G,I,H,D)],[oncircle(G,I,H,K)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, K, L, M} are reassigned Theorem: If the points A, B, and C are arbitrary, G is the perpendicular foot of the line BC to the line AG, `` || (I) || ` is the perpendicular foot of the line ` || A || C || ` to the line ` || B || (I) , H is the perpendicular foot of the line BA to the line CH, F is the midpoint of B and C, D is the midpoint of B and A, `the point J is on the line B` || (I) , L is the midpoint of B and J, the two lines AG and HC intersect at J, E is the midpoint of C and A, M is the midpoint of C and J, K is the midpoint of A and J, `the point F is on the circumcircle of the triangle G` || (I) || H , `the point E is on the circumcircle of the triangle G` || (I) || H , `the point M is on the circumcircle of the triangle G` || (I) || H , `the point L is on the circumcircle of the triangle G` || (I) || H , and `the point D is on the circumcircle of the triangle G` || (I) || H , then `the point K is on the circumcircle of the triangle G` || (I) || H . Proof: char set produced: [4 x1 1] [3 y1 1] [4 x2 1] [3 y2 1] [1 x3 1] [1 y3 1] [2 x4 1] [2 y4 1] [3 x5 1] [1 y5 1] [8 x6 1] [4 y6 1] [3 x7 1] [2 y7 1] [2 x8 1] [2 y8 1] [2 x9 1] [3 y9 1] [3 x10 1] [2 y10 1] pseudo-remainder: [48 y10 2] = -y2*y10^2*x1 + ... (47 terms) pseudo-remainder: [48 x10 2] = -4*y2*x10^2*x1 + ... (47 terms) pseudo-remainder: [72 y6 2] = -y6^2*y2*x1 + ... (71 terms) pseudo-remainder: [166 x6 2] = -u1^2*x6^2*y2*x1 + ... (165 terms) pseudo-remainder: [725 y3 2] = 2*u1^5*y2^2*y3^2*y1 + ... (724 terms) pseudo-remainder: [213 x3 2] = 2*u1^3*y2^2*y1*x3^2 + ... (212 terms) pseudo-remainder: [88 y2 4] = -2*u1^3*y1*y2^4 + ... (87 terms) pseudo-remainder: [213 x2 4] = -2*v1^2*x2^4*u1^4*y1 + ... (212 terms) pseudo-remainder: [101 y1 4] = -2*v1^3*u1^9*u2*y1^4 + ... (100 terms) pseudo-remainder: [47 x1 4] = 2*u1*u2^5*v1^3*x1^4 + ... (46 terms) `The theorem is true under the following subsidiary conditions:` . the line AC is non-isotropic . the line BA 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 . -y2*x1+u1*y2+x2*y1-u2*y1 <> 0 . the line AG is not perpendicular to the line AB QED.
Theorem([arbitrary(A,B,C), perpfoot(B,C,A,G,G), perpfoot(A,C,B,I,I), perpfoot(B,A,C,H,H), midpoint(B,C,F), midpoint(B,A,D), online(B,I,J), midpoint(B,J,L), intersection(A,G,H,C,J), midpoint(C,A,E), midpoint(C,J,M), midpoint(A,J,K), oncircle(G,I,H,K), oncircle(G,I,H,E), oncircle(G,I,H,M), oncircle(G,I,H,L), oncircle(G,I,H,D)],[oncircle(G,I,H,F)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, K, L, M} are reassigned Theorem: If the points A, B, and C are arbitrary, G is the perpendicular foot of the line BC to the line AG, `` || (I) || ` is the perpendicular foot of the line ` || A || C || ` to the line ` || B || (I) , H is the perpendicular foot of the line BA to the line CH, F is the midpoint of B and C, D is the midpoint of B and A, `the point J is on the line B` || (I) , L is the midpoint of B and J, the two lines AG and HC intersect at J, E is the midpoint of C and A, M is the midpoint of C and J, K is the midpoint of A and J, `the point K is on the circumcircle of the triangle G` || (I) || H , `the point E is on the circumcircle of the triangle G` || (I) || H , `the point M is on the circumcircle of the triangle G` || (I) || H , `the point L is on the circumcircle of the triangle G` || (I) || H , and `the point D is on the circumcircle of the triangle G` || (I) || H , then `the point F is on the circumcircle of the triangle G` || (I) || H . Proof: char set produced: [4 x1 1] [3 y1 1] [4 x2 1] [3 y2 1] [1 x3 1] [1 y3 1] [2 x4 1] [2 y4 1] [3 x5 1] [1 y5 1] [8 x6 1] [4 y6 1] [3 x7 1] [2 y7 1] [2 x8 1] [2 y8 1] [2 x9 1] [3 y9 1] [3 x10 1] [2 y10 1] pseudo-remainder: [48 y4 2] = -y2*y4^2*x1 + ... (47 terms) pseudo-remainder: [48 x4 2] = -4*y2*x4^2*x1 + ... (47 terms) pseudo-remainder: [48 y3 2] = 2*u2*y3^2*y1 + ... (47 terms) pseudo-remainder: [30 x3 2] = 2*u2*x3^2*y1 + ... (29 terms) pseudo-remainder: [12 y2 2] = -2*u2*y2^2*y1 + ... (11 terms) pseudo-remainder: [18 x2 2] = -2*u1^2*u2*x2^2*y1 + ... (17 terms) pseudo-remainder: [12 y1 2] = -2*u1^3*u2^2*v1*y1^2 + ... (11 terms) pseudo-remainder: [7 x1 2] = -2*v1*u2^2*x1^2 + ... (6 terms) `The theorem is true under the following subsidiary conditions:` . the line AC is non-isotropic . the line BA 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 . -y2*x1+u1*y2+x2*y1-u2*y1 <> 0 . the line AG is not perpendicular to the line AB QED.
Theorem([arbitrary(B,A,C), perpfoot(B,C,A,G,G), perpfoot(A,C,B,I,I), perpfoot(B,A,C,H,H), midpoint(B,C,F), midpoint(B,A,D), midpoint(B,J,L), intersection(A,G,H,C,J), midpoint(C,A,E), midpoint(C,J,M), midpoint(A,J,K), oncircle(G,I,H,F), oncircle(G,I,H,K), oncircle(G,I,H,E), oncircle(G,I,H,M), oncircle(G,I,H,L), oncircle(G,I,H,D)],[online(B,I,J)]) Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J, K, L, M} 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, `` || (I) || ` is the perpendicular foot of the line ` || A || C || ` to the line ` || B || (I) , H is the perpendicular foot of the line BA to the line CH, F is the midpoint of B and C, D is the midpoint of B and A, L is the midpoint of B and J, the two lines AG and HC intersect at J, E is the midpoint of C and A, M is the midpoint of C and J, K is the midpoint of A and J, `the point F is on the circumcircle of the triangle G` || (I) || H , `the point K is on the circumcircle of the triangle G` || (I) || H , `the point E is on the circumcircle of the triangle G` || (I) || H , `the point M is on the circumcircle of the triangle G` || (I) || H , `the point L is on the circumcircle of the triangle G` || (I) || H , and `the point D is on the circumcircle of the triangle G` || (I) || H , then `the point J is on the line B` || (I) . Proof: Status: used = 12246, alloced = 12588, time = 5.334999999999999 char set produced: [4 x1 1] [3 y1 1] [4 x2 1] [3 y2 1] [1 x3 1] [1 y3 1] [2 x4 1] [2 y4 1] [3 x5 1] [1 y5 1] [8 x6 1] [4 y6 1] [3 x7 1] [2 y7 1] [2 x8 1] [2 y8 1] [2 x9 1] [3 y9 1] [3 x10 1] [2 y10 1] pseudo-remainder: [4 y6 1] = -u1*y6 + ... (3 terms) pseudo-remainder: [8 x6 1] = -y1*x6*u1 + ... (7 terms) pseudo-remainder: [25 y3 1] = u2^2*y3*y1*u1 + ... (24 terms) pseudo-remainder: [10 x3 1] = v1*x3*y1*u1 + ... (9 terms) pseudo-remainder: [4 y2 1] = u2*v1*u1*y2 + ... (3 terms) pseudo-remainder: [6 x2 1] = v1^2*x2*u2*u1 + ... (5 terms) pseudo-remainder: [6 y1 1] = -v1^3*u2^2*y1*u1 + ... (5 terms) pseudo-remainder: [4 x1 1] = -v1^2*u1^2*x1 + ... (3 terms) `The theorem is true under the following subsidiary conditions:` . the line AC is non-isotropic . the line BA is non-isotropic . the line BC is non-isotropic . the line AG is not parallel to the line HC . the line AB is not perpendicular to the line BC . the line AC is not perpendicular to the line AB . the line AG is not perpendicular to the line AB QED.
