Theorem([arbitrary(A,D,C,B), intersection(A,D,C,B,E), equidistance(C,A,D,B), equidistance(A,E,E,B), equidistance(E,D,C,E), parallel(C,D,A,B)],[equidistance(A,D,C,B)]) Warning: the coordinates of the points from {A, B, C, D, E} are reassigned Theorem: If the points A, D, C, and B are arbitrary, the two lines AD and CB intersect at E, the distance between C and A is equal to the distance between D and B, the distance between A and E is equal to the distance between E and B, the distance between E and D is equal to the distance between C and E, and the line CD is parallel to the line AB, then the distance between A and D is equal to the distance between C and B. Proof: char set produced: [6 v1 2] [3 v2 1] [3 x1 1] [1 y1 1] pseudo-remainder: [7 v2 2] = -v2^2 + ... (6 terms) pseudo-remainder: [10 v1 2] = -u1^2*v1^2 + ... (9 terms) `The theorem is true under the following subsidiary conditions:` . the line AD is not parallel to the line CB . the line AD is not perpendicular to the line CD . u1-u2-u3 <> 0 . u2+u1-u3 <> 0 QED.
Theorem([arbitrary(A,D,C,B), intersection(A,D,C,B,E), equidistance(C,A,D,B), equidistance(A,E,E,B), equidistance(E,D,C,E), equidistance(A,D,C,B)],[parallel(C,D,A,B)]) Warning: the coordinates of the points from {A, B, C, D, E} are reassigned Theorem: If the points A, D, C, and B are arbitrary, the two lines AD and CB intersect at E, the distance between C and A is equal to the distance between D and B, the distance between A and E is equal to the distance between E and B, the distance between E and D is equal to the distance between C and E, and the distance between A and D is equal to the distance between C and B, then the line CD is parallel to the line AB. Proof: char set produced: [6 v1 2] [5 v2 1] [3 x1 1] [1 y1 1] pseudo-remainder: [3 v2 1] = u2*v2 + ... (2 terms) pseudo-remainder: [6 v1 3] = -v1^3*u1 + ... (5 terms) `The theorem is true under the following subsidiary conditions:` . the line AD is not parallel to the line CB . -v1^2+u2^2 <> 0 . the line AD is not perpendicular to the line CD . u1-u2-u3 <> 0 . the line AD is not perpendicular to the line CB QED.
Theorem([arbitrary(D,C,A,B), intersection(A,D,C,B,E), equidistance(C,A,D,B), equidistance(A,E,E,B), parallel(C,D,A,B), equidistance(A,D,C,B)],[equidistance(E,D,C,E)]) Warning: the coordinates of the points from {A, B, C, D, E} are reassigned Theorem: If the points D, C, A, and B are arbitrary, the two lines AD and CB intersect at E, the distance between C and A is equal to the distance between D and B, the distance between A and E is equal to the distance between E and B, the line CD is parallel to the line AB, and the distance between A and D is equal to the distance between C and B, then the distance between E and D is equal to the distance between C and E. Proof: char set produced: [3 u3 1] [1 v1 1] [2 v2 1] [6 x1 1] [3 y1 1] char set recomputed: [3 u3 1] [2 v2 1] [3 x1 1] [3 y1 1] pseudo-remainder: [4 x1 1] = -2*u1*x1 + ... (3 terms) `The theorem is true under the following subsidiary conditions:` . u2+u1 <> 0 . the line CD is non-isotropic . the line AD is not perpendicular to the line CD QED.
Theorem([arbitrary(A,B,D,C), intersection(A,D,C,B,E), equidistance(C,A,D,B), equidistance(E,D,C,E), parallel(C,D,A,B), equidistance(A,D,C,B)],[equidistance(A,E,E,B)]) Warning: the coordinates of the points from {A, B, C, D, E} are reassigned Theorem: If the points A, B, D, and C are arbitrary, the two lines AD and CB intersect at E, the distance between C and A is equal to the distance between D and B, the distance between E and D is equal to the distance between C and E, the line CD is parallel to the line AB, and the distance between A and D is equal to the distance between C and B, then the distance between A and E is equal to the distance between E and B. Proof: char set produced: [3 u3 1] [1 v1 1] [2 v2 1] [6 x1 1] [3 y1 1] char set recomputed: [3 u3 1] [2 v2 1] [3 x1 1] [3 y1 1] pseudo-remainder: [4 x1 1] = -2*u1*x1 + ... (3 terms) `The theorem is true under the following subsidiary conditions:` . u2+u1 <> 0 . the line AB is non-isotropic . the line AD is not perpendicular to the line AB QED.
Theorem([arbitrary(A,D,C,B), intersection(A,D,C,B,E), equidistance(A,E,E,B), equidistance(E,D,C,E), parallel(C,D,A,B), equidistance(A,D,C,B)],[equidistance(C,A,D,B)]) Warning: the coordinates of the points from {A, B, C, D, E} are reassigned Theorem: If the points A, D, C, and B are arbitrary, the two lines AD and CB intersect at E, the distance between A and E is equal to the distance between E and B, the distance between E and D is equal to the distance between C and E, the line CD is parallel to the line AB, and the distance between A and D is equal to the distance between C and B, then the distance between C and A is equal to the distance between D and B. Proof: char set produced: [6 v1 2] [3 v2 1] [3 x1 1] [1 y1 1] pseudo-remainder: [6 v2 2] = -v2^2 + ... (5 terms) pseudo-remainder: [8 v1 2] = -u1^2*v1^2 + ... (7 terms) `The theorem is true under the following subsidiary conditions:` . the line AD is not parallel to the line CB . the line AD is not perpendicular to the line CD . u1-u2-u3 <> 0 QED.
