Theorem([arbitrary(F,B,C,A), equiangle(A,B,F,F,B,C), equiangle(C,A,E,E,A,B), equiangle(B,C,D,D,C,A), online(A,C,F), intersection(A,E,B,F,G), online(B,A,D), online(D,C,G)],[online(B,C,E)]) Warning: the coordinates of the points from {A, B, C, D, E, F, G} are reassigned Theorem: If the points F, B, C, and A are arbitrary, the angle ABF is equal to the angle FBC, the angle CAE is equal to the angle EAB, the angle BCD is equal to the angle DCA, the point F is on the line AC, the two lines AE and BF intersect at G, the point D is on the line BA, and the point G is on the line DC, then the point E is on the line BC. Proof: char set produced: [1 v1 1] [3 v2 1] [4 x1 3] [9 y1 1] [12 x2 1] [4 y2 1] [4 x3 1] [1 y3 1] Status: used = 3446, alloced = 5571, time = 5.1160000000000005 char set recomputed: [1 v1 1] [3 v2 1] [1 y1 1] [4 y2 1] [1 y3 1] pseudo-remainder: [3 y1 1] = -u2*y1 + ... (2 terms) pseudo-remainder: [2 v2 0] = u2*v1 + ... (1 terms) pseudo-remainder: [2 v1 1] = u2*v1 + ... (1 terms) `The theorem is true under the following subsidiary conditions:` . the line AE is not parallel to the line BF . the line BF is not perpendicular to the line CF . -u3*u1+2*u1*u2-u3*u2 <> 0 . the line AB is not perpendicular to the line BF . (-x1+u3)*u3 <> 0 QED.
Theorem([arbitrary(F,C,A,B), equiangle(A,B,F,F,B,C), equiangle(C,A,E,E,A,B), online(A,C,F), intersection(A,E,B,F,G), online(B,A,D), online(B,C,E), online(D,C,G)],[equiangle(B,C,D,D,C,A)]) Warning: the coordinates of the points from {A, B, C, D, E, F, G} are reassigned Theorem: If the points F, C, A, and B are arbitrary, the angle ABF is equal to the angle FBC, the angle CAE is equal to the angle EAB, the point F is on the line AC, the two lines AE and BF intersect at G, the point D is on the line BA, the point E is on the line BC, and the point G is on the line DC, then the angle BCD is equal to the angle DCA. Proof: char set produced: [1 v1 1] [15 v2 3] [14 x1 2] [4 y1 1] [8 x2 1] [4 y2 1] [8 x3 1] [4 y3 1] pseudo-remainder: [18 y3 2] = -u2*y3^2*v1 + ... (17 terms) pseudo-remainder: [23 x3 2] = -2*v1*x3^2*u3*u2^2 + ... (22 terms) pseudo-remainder: [32 y2 2] = -u3^2*u2^2*y2^2*v1^2 + ... (31 terms) pseudo-remainder: [41 x2 2] = v1*x2^2*u1^2*u2 + ... (40 terms) pseudo-remainder: [210 y1 2] = u1^4*y1^2*v1*u2^3 + ... (209 terms) pseudo-remainder: [158 x1 2] = v1^3*u1^2*u2^3*x1^2 + ... (157 terms) pseudo-remainder: [81 v2 4] = 4*v2^4*u2^4*u1 + ... (80 terms) pseudo-remainder: [85 v2 4] = -2*u2^5*v2^4*u1 + ... (84 terms) `The theorem is true under the following subsidiary conditions:` . the line AE is not parallel to the line BF . 2*u1-u2 <> 0 . the line CF is non-isotropic . u2^2+2*v1*v2-u3^2-v2^2 <> 0 . the three points A, B and C are not collinear . the line AB is not perpendicular to the line CF . the line BC is not perpendicular to the line CF . the line BF is not perpendicular to the line CF . the line AB is not parallel to the line CG QED.
Theorem([arbitrary(F,A,B,C), equiangle(A,B,F,F,B,C), equiangle(B,C,D,D,C,A), online(A,C,F), intersection(A,E,B,F,G), online(B,A,D), online(B,C,E), online(D,C,G)],[equiangle(C,A,E,E,A,B)]) Warning: the coordinates of the points from {A, B, C, D, E, F, G} are reassigned Theorem: If the points F, A, B, and C are arbitrary, the angle ABF is equal to the angle FBC, the angle BCD is equal to the angle DCA, the point F is on the line AC, the two lines AE and BF intersect at G, the point D is on the line BA, the point E is on the line BC, and the point G is on the line DC, then the angle CAE is equal to the angle EAB. Proof: char set produced: [6 v1 3] [1 v2 1] [12 x1 2] [3 y1 1] [24 x2 1] [4 y2 1] [8 x3 1] [3 y3 1] pseudo-remainder: [18 y2 2] = -u2*y2^2*v1 + ... (17 terms) pseudo-remainder: [23 x2 2] = -2*v1*u3*u2^2*x2^2 + ... (22 terms) pseudo-remainder: [198 y1 2] = -u1^2*y1^2*v1^2*u2^4*u3^2 + ... (197 terms) pseudo-remainder: [99 x1 2] = 2*v1^2*u1^2*u2^3*x1^2*v2 + ... (98 terms) pseudo-remainder: [104 v2 4] = u2^4*v2^4*u1^2 + ... (103 terms) pseudo-remainder: [28 v1 3] = 2*u1*v1^3*u2^3 + ... (27 terms) `The theorem is true under the following subsidiary conditions:` . the line AF is non-isotropic . the line AF is not perpendicular to the line AB . the line AF is not perpendicular to the line BF . -u2+2*u1-u3 <> 0 . u2^2-2*u3*u2-v1^2+2*v1*v2 <> 0 . the three points A, B and C are not collinear . the line AF is not perpendicular to the line CB . -u2*v1^2*x1+v1^2*u3*u2+v2*x1*u2*v1+v1*u3*x1*v2+u1*v2^2*x1-v2^2*u1*u2+y1*u2*v2*u1-u1*y1*v1*u2-u3^2*y1*v1-u3*y1*v2*u1+2*u1*y1*v1*u3-v1*u3*u2*v2+u1*v1^2*x1-v1^2*u3*u1-2*u1*v1*x1*v2+v1*u2*v2*u1 <> 0 . the line BF is not parallel to the line DC QED.
Theorem([arbitrary(E,B,C,A), equiangle(C,A,E,E,A,B), equiangle(B,C,D,D,C,A), online(A,C,F), intersection(A,E,B,F,G), online(B,A,D), online(B,C,E), online(D,C,G)],[equiangle(A,B,F,F,B,C)]) Warning: the coordinates of the points from {A, B, C, D, E, F, G} are reassigned Theorem: If the points E, B, C, and A are arbitrary, the angle CAE is equal to the angle EAB, the angle BCD is equal to the angle DCA, the point F is on the line AC, the two lines AE and BF intersect at G, the point D is on the line BA, the point E is on the line BC, and the point G is on the line DC, then the angle ABF is equal to the angle FBC. Proof: char set produced: [1 v1 1] [15 v2 3] [14 x1 2] [4 y1 1] [25 x2 1] [4 y2 1] [8 x3 1] [4 y3 1] pseudo-remainder: [18 y2 2] = -u2*y2^2*v1 + ... (17 terms) pseudo-remainder: [23 x2 2] = -2*v1*u3*u2^2*x2^2 + ... (22 terms) pseudo-remainder: [174 y1 2] = u1^2*y1^2*v1^2*u2^4*u3^2 + ... (173 terms) pseudo-remainder: [158 x1 2] = v1^3*u1^2*u2^3*x1^2 + ... (157 terms) pseudo-remainder: [81 v2 4] = 4*v2^4*u2^4*u1 + ... (80 terms) pseudo-remainder: [85 v2 4] = -2*u2^5*v2^4*u1 + ... (84 terms) `The theorem is true under the following subsidiary conditions:` . 2*u1-u2 <> 0 . the line BE is non-isotropic . u2^2+2*v1*v2-u3^2-v2^2 <> 0 . the three points A, B and C are not collinear . the line AB is not perpendicular to the line BE . the line AC is not perpendicular to the line BE . the line AE is not perpendicular to the line BE . 2*u1*v1*x1*v2+u3*y1*v2*u1-u1*v2*v1*u3-u1*y1*v1*u2-v2*x1*u2*v1+u2*u3*y1*v1+y1*u2*v2*u1-v1*u2*v2*u1+v1*u3*u2*v2-v2*y1*u3*u2-u1*v1^2*x1+u1*u2*v1^2-v1^2*u3*u2+u3*v1^2*x1+v2^2*x1*u2-u1*v2^2*x1 <> 0 . the line AE is not parallel to the line DC QED.
