Theorems

1. Theorem([arbitrary(L,C,B), perpfoot(B,C,L,I,I), midpoint(B,C,I), perpfoot(B,A,L,D,D), midpoint(B,A,D), perpfoot(A,C,L,F,F)],[midpoint(A,C,F)])
   Warning: the coordinates of the points from {I, A, B, C, D, F, L} are reassigned
   
   
   Theorem: If the points L, C, and B are arbitrary, `` || (I) || ` is the perpendicular foot of the line ` || B || C || ` to the line ` || L || (I) , `` || (I) || ` is the midpoint of ` || B || ` and ` || C , D is the perpendicular foot of the line BA to the line LD, D is the midpoint of B and A, and F is the perpendicular foot of the line AC to the line LF, then F is the midpoint of A and C.
   
   Proof:
   
   char set produced: [3 v1 2] [2 x1 1] [2 y1 1] [4 y2 2] [2 x3 1] [3 y3 1] [8 x4 1] [4 y4 1]
   pseudo-remainder: [3 x4 1] = 2*x4 + ... (2 terms)
   pseudo-remainder: [9 y2 2] = -u2*y2^2 + ... (8 terms)
   pseudo-remainder: [3 v1 2] = v1^2 + ... (2 terms)
   pseudo-remainder: [2 y4 1] = 2*y4 + ... (1 terms)
   pseudo-remainder: [3 x4 1] = -2*y2*x4 + ... (2 terms)
   pseudo-remainder: [9 y2 3] = u2*y2^3 + ... (8 terms)
   pseudo-remainder: [3 y1 0] = -2*y2*u1*u2 + ... (2 terms)
   pseudo-remainder: [3 x1 0] = -2*y2*u1*u2 + ... (2 terms)
   pseudo-remainder: [3 v1 2] = -y2*v1^2 + ... (2 terms)
   
   `The theorem is true under the following subsidiary conditions:`
   . the line AC is non-isotropic
   . the line AC is not perpendicular to the line CL
   
   QED.


2. Theorem([arbitrary(L,C,B), perpfoot(B,C,L,I,I), midpoint(B,C,I), perpfoot(B,A,L,D,D), midpoint(B,A,D), midpoint(A,C,F)],[perpfoot(A,C,L,F,F)])
   Warning: the coordinates of the points from {I, A, B, C, D, F, L} are reassigned
   
   
   Theorem: If the points L, C, and B are arbitrary, `` || (I) || ` is the perpendicular foot of the line ` || B || C || ` to the line ` || L || (I) , `` || (I) || ` is the midpoint of ` || B || ` and ` || C , D is the perpendicular foot of the line BA to the line LD, D is the midpoint of B and A, and F is the midpoint of A and C, then F is the perpendicular foot of the line AC to the line LF.
   
   Proof:
   
   char set produced: [3 v1 2] [2 x1 1] [2 y1 1] [4 y2 2] [2 x3 1] [3 y3 1] [3 x4 1] [2 y4 1]
   pseudo-remainder: [5 y4 1] = -y2*y4 + ... (4 terms)
   pseudo-remainder: [5 x4 1] = 2*u2*x4 + ... (4 terms)
   pseudo-remainder: [5 y2 2] = -y2^2 + ... (4 terms)
   pseudo-remainder: [3 v1 2] = v1^2 + ... (2 terms)
   pseudo-remainder: [4 y4 1] = u2*y4 + ... (3 terms)
   pseudo-remainder: [3 x4 1] = 2*y2*x4 + ... (2 terms)
   
   `The theorem is true.`
   
   QED.


3. Theorem([arbitrary(L,B,C), perpfoot(B,C,L,I,I), midpoint(B,C,I), perpfoot(B,A,L,D,D), perpfoot(A,C,L,F,F), midpoint(A,C,F)],[midpoint(B,A,D)])
   Warning: the coordinates of the points from {I, A, B, C, D, F, L} are reassigned
   
   
   Theorem: If the points L, B, and C are arbitrary, `` || (I) || ` is the perpendicular foot of the line ` || B || C || ` to the line ` || L || (I) , `` || (I) || ` is the midpoint of ` || B || ` and ` || C , D is the perpendicular foot of the line BA to the line LD, F is the perpendicular foot of the line AC to the line LF, and F is the midpoint of A and C, then D is the midpoint of B and A.
   
   Proof:
   
   char set produced: [3 v1 2] [2 x1 1] [2 y1 1] [4 y2 2] [8 x3 1] [4 y3 1] [2 x4 1] [3 y4 1]
   pseudo-remainder: [3 x3 1] = 2*x3 + ... (2 terms)
   pseudo-remainder: [9 y2 2] = -u2*y2^2 + ... (8 terms)
   pseudo-remainder: [3 v1 2] = v1^2 + ... (2 terms)
   pseudo-remainder: [2 y3 1] = 2*y3 + ... (1 terms)
   pseudo-remainder: [3 x3 1] = 2*y2*x3 + ... (2 terms)
   pseudo-remainder: [9 y2 3] = -u2*y2^3 + ... (8 terms)
   pseudo-remainder: [3 y1 0] = 2*y2*u1*u2 + ... (2 terms)
   pseudo-remainder: [3 x1 0] = 2*y2*u1*u2 + ... (2 terms)
   pseudo-remainder: [3 v1 2] = y2*v1^2 + ... (2 terms)
   
   `The theorem is true under the following subsidiary conditions:`
   . the line BA is non-isotropic
   . the line AB is not perpendicular to the line BL
   
   QED.


4. Theorem([arbitrary(L,B,C), perpfoot(B,C,L,I,I), midpoint(B,C,I), midpoint(B,A,D), perpfoot(A,C,L,F,F), midpoint(A,C,F)],[perpfoot(B,A,L,D,D)])
   Warning: the coordinates of the points from {I, A, B, C, D, F, L} are reassigned
   
   
   Theorem: If the points L, B, and C are arbitrary, `` || (I) || ` is the perpendicular foot of the line ` || B || C || ` to the line ` || L || (I) , `` || (I) || ` is the midpoint of ` || B || ` and ` || C , D is the midpoint of B and A, F is the perpendicular foot of the line AC to the line LF, and F is the midpoint of A and C, then D is the perpendicular foot of the line BA to the line LD.
   
   Proof:
   
   char set produced: [3 v1 2] [2 x1 1] [2 y1 1] [4 y2 2] [3 x3 1] [2 y3 1] [2 x4 1] [3 y4 1]
   pseudo-remainder: [5 y3 1] = y3*y2 + ... (4 terms)
   pseudo-remainder: [5 x3 1] = -2*u2*x3 + ... (4 terms)
   pseudo-remainder: [5 y2 2] = y2^2 + ... (4 terms)
   pseudo-remainder: [3 v1 2] = -v1^2 + ... (2 terms)
   pseudo-remainder: [4 y3 1] = -u2*y3 + ... (3 terms)
   pseudo-remainder: [3 x3 1] = -2*y2*x3 + ... (2 terms)
   
   `The theorem is true.`
   
   QED.


5. Theorem([arbitrary(L,B,C), perpfoot(B,C,L,I,I), perpfoot(B,A,L,D,D), midpoint(B,A,D), perpfoot(A,C,L,F,F), midpoint(A,C,F)],[midpoint(B,C,I)])
   Warning: the coordinates of the points from {I, A, B, C, D, F, L} are reassigned
   
   
   Theorem: If the points L, B, and C are arbitrary, `` || (I) || ` is the perpendicular foot of the line ` || B || C || ` to the line ` || L || (I) , D is the perpendicular foot of the line BA to the line LD, D is the midpoint of B and A, F is the perpendicular foot of the line AC to the line LF, and F is the midpoint of A and C, then `` || (I) || ` is the midpoint of ` || B || ` and ` || C .
   
   Proof:
   
   char set produced: [3 v1 2] [4 x1 1] [3 y1 1] [5 y2 2] [3 x3 1] [2 y3 1] [2 x4 1] [3 y4 1]
   pseudo-remainder: [2 x1 1] = 2*x1 + ... (1 terms)
   pseudo-remainder: [3 v1 2] = -u2*v1^2 + ... (2 terms)
   pseudo-remainder: [2 y1 1] = 2*y1 + ... (1 terms)
   pseudo-remainder: [2 x1 1] = 2*v1*x1 + ... (1 terms)
   pseudo-remainder: [3 v1 3] = -u2*v1^3 + ... (2 terms)
   
   `The theorem is true under the following subsidiary conditions:`
   . the line BC is non-isotropic
   . the line BL is not perpendicular to the line BC
   
   QED.


6. Theorem([arbitrary(B,C), midpoint(B,C,I), perpfoot(B,A,L,D,D), midpoint(B,A,D), perpfoot(A,C,L,F,F), midpoint(A,C,F)],[perpfoot(B,C,L,I,I)])
   Warning: the coordinates of the points from {I, A, B, C, D, F, L} are reassigned
   
   Status: used = 838, alloced = 3072, time = 6.848
   
   Theorem: If the points B and C are arbitrary, `` || (I) || ` is the midpoint of ` || B || ` and ` || C , D is the perpendicular foot of the line BA to the line LD, D is the midpoint of B and A, F is the perpendicular foot of the line AC to the line LF, and F is the midpoint of A and C, then `` || (I) || ` is the perpendicular foot of the line ` || B || C || ` to the line ` || L || (I) .
   
   Proof:
   
   char set produced: [2 x1 1] [1 y1 1] [2 x3 1] [4 y3 1] [2 x4 1] [2 y4 1] [3 x5 1] [2 y5 1]
   pseudo-remainder: [2 x3 1] = -u1*x3 + ... (1 terms)
   pseudo-remainder: [2 x1 1] = -2*x1 + ... (1 terms)
   pseudo-remainder: [1 y1 1] = u1*y1
   
   `The theorem is true under the following subsidiary conditions:`
   . the line BC is non-isotropic
   . the three points A, B and C are not collinear
   
   QED.