Theorems
-
Theorem([arbitrary(G,D), online(G,D,A), intersection(A,H,G,E,B), intersection(A,I,G,F,C), intersection(J,E,I,D,F), online(J,H,I), online(H,D,E)],[online(B,J,C)])
Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J} are reassigned
Theorem: If the points G and D are arbitrary, the point A is on the line GD, the two lines AH and GE intersect at B, `the two lines A` || (I) || ` and ` || G || F || ` intersect at ` || C , `the two lines JE and ` || (I) || D || ` intersect at ` || F , `the point ` || (I) || ` is on the line ` || J || H , and the point E is on the line HD, then the point C is on the line BJ.
Proof:
char set produced: [1 y1 1] [4 y3 1] [6 x4 1] [6 y4 1] [4 y6 1] [6 x7 1] [6 y7 1] [16 x8 1] [6 y8 1]
pseudo-remainder: [6 y8 1] = y8*x4 + ... (5 terms)
pseudo-remainder: [16 x8 1] = x2*x8*y4 + ... (15 terms)
pseudo-remainder: [88 y7 1] = x2^2*y5*x3*y7 + ... (87 terms)
pseudo-remainder: [120 x7 1] = -x1*x2*x7*y3*y4 + ... (119 terms)
pseudo-remainder: [200 y6 2] = x1^2*y6^2*x2*x3*y4 + ... (199 terms)
pseudo-remainder: [2 y4 1] = y1*y3*y4 + ... (1 terms)
pseudo-remainder: [4 x4 1] = -y3*y1^2*x4 + ... (3 terms)
pseudo-remainder: [8 y3 2] = -x1*y3^2*y1^2*x2 + ... (7 terms)
pseudo-remainder: [8 y1 2] = -y2^2*u1^2*x2*y1^2 + ... (7 terms)
pseudo-remainder: [2 y4 1] = -y1*y3*y4 + ... (1 terms)
pseudo-remainder: [4 x4 1] = y3*y1^2*x4 + ... (3 terms)
pseudo-remainder: [8 y3 2] = x1*y3^2*y1^2*x2 + ... (7 terms)
pseudo-remainder: [8 y1 2] = y2^2*u1^2*x2*y1^2 + ... (7 terms)
pseudo-remainder: [2 y4 1] = -u1^2*x2*y1*y3*y4 + ... (1 terms)
pseudo-remainder: [4 x4 1] = -y1*y3*y2*x4*x1 + ... (3 terms)
pseudo-remainder: [8 y3 2] = -x1^2*y3^2*x2*y1*y2 + ... (7 terms)
pseudo-remainder: [8 y1 2] = y2^2*u1^2*x2^2*y1^2 + ... (7 terms)
pseudo-remainder: [2 y4 1] = u1^2*x2*y1*y3*y4 + ... (1 terms)
pseudo-remainder: [4 x4 1] = y1*y3*y2*x4*x1 + ... (3 terms)
pseudo-remainder: [8 y3 2] = x1^2*y3^2*x2*y1*y2 + ... (7 terms)
pseudo-remainder: [8 y1 2] = -y2^2*u1^2*x2^2*y1^2 + ... (7 terms)
pseudo-remainder: [4 y4 1] = y2*x3*u1*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = -x1*y3*y1*x4 + ... (7 terms)
pseudo-remainder: [8 y3 1] = -x2*y1^2*x3*x1*y3 + ... (7 terms)
pseudo-remainder: [4 y1 2] = -u1*x2*y1^2*x3*y2 + ... (3 terms)
pseudo-remainder: [4 y4 1] = u1^2*y1*y3*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = -y1^2*x4*u1*y3 + ... (7 terms)
pseudo-remainder: [16 y3 2] = -x1*y3^2*x2*y1^2*u1 + ... (15 terms)
pseudo-remainder: [15 y1 2] = -y2^2*u1^3*x2*y1^2 + ... (14 terms)
pseudo-remainder: [4 y4 1] = 2*u1*y1*y3*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = -2*y1^2*x4*u1*y3 + ... (7 terms)
pseudo-remainder: [16 y3 2] = -2*x1*y3^2*x2*y1^2*u1 + ... (15 terms)
pseudo-remainder: [15 y1 2] = -2*y2^2*u1^3*x2*y1^2 + ... (14 terms)
pseudo-remainder: [4 y4 1] = -2*u1*y1*y3*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = 2*y1^2*x4*u1*y3 + ... (7 terms)
pseudo-remainder: [16 y3 2] = 2*x1*y3^2*x2*y1^2*u1 + ... (15 terms)
pseudo-remainder: [15 y1 2] = 2*y2^2*u1^3*x2*y1^2 + ... (14 terms)
pseudo-remainder: [4 y4 1] = -u1^2*y1*y3*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = y1^2*x4*u1*y3 + ... (7 terms)
pseudo-remainder: [16 y3 2] = x1*y3^2*x2*y1^2*u1 + ... (15 terms)
pseudo-remainder: [15 y1 2] = y2^2*u1^3*x2*y1^2 + ... (14 terms)
pseudo-remainder: [4 y4 1] = -y2*x1*u1^2*x3*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = -x1^2*y3*y2*x4 + ... (7 terms)
pseudo-remainder: [8 y3 1] = -x2*y1*x3*y3*y2*x1^2 + ... (7 terms)
pseudo-remainder: [4 y1 2] = y2*u1*x2^2*y1^2*x3 + ... (3 terms)
pseudo-remainder: [4 y4 1] = y2*x1*u1^2*x3*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = x1^2*y3*y2*x4 + ... (7 terms)
pseudo-remainder: [8 y3 1] = x2*y1*x3*y3*y2*x1^2 + ... (7 terms)
pseudo-remainder: [4 y1 2] = -y2*u1*x2^2*y1^2*x3 + ... (3 terms)
pseudo-remainder: [6 x4 1] = -x1*u1*x4 + ... (5 terms)
pseudo-remainder: [12 y3 1] = -x1^2*y3*x3*u1 + ... (11 terms)
pseudo-remainder: [2 y1 1] = -x2*x3*u1*y1 + ... (1 terms)
pseudo-remainder: [6 x4 1] = x1*u1*x4 + ... (5 terms)
pseudo-remainder: [12 y3 1] = x1^2*y3*x3*u1 + ... (11 terms)
pseudo-remainder: [2 y1 1] = x2*x3*u1*y1 + ... (1 terms)
pseudo-remainder: [6 x4 1] = u1^2*x1*x4 + ... (5 terms)
pseudo-remainder: [12 y3 1] = x1^2*y3*x3*u1 + ... (11 terms)
pseudo-remainder: [2 y1 1] = x2*x3*u1*y1 + ... (1 terms)
pseudo-remainder: [6 x4 1] = -u1^2*x1*x4 + ... (5 terms)
pseudo-remainder: [12 y3 1] = -x1^2*y3*x3*u1 + ... (11 terms)
pseudo-remainder: [2 y1 1] = -x2*x3*u1*y1 + ... (1 terms)
pseudo-remainder: [8 y4 1] = -u1^2*x3*y2*y4 + ... (7 terms)
pseudo-remainder: [16 x4 1] = x1*u1*y1*y3*x4 + ... (15 terms)
pseudo-remainder: [16 y3 1] = x2*y1^2*x3*x1*y3*u1 + ... (15 terms)
pseudo-remainder: [8 y1 2] = y2*u1^2*x2*y1^2*x3 + ... (7 terms)
pseudo-remainder: [10 y4 1] = -u1*y1*y4 + ... (9 terms)
pseudo-remainder: [21 x4 1] = y1^2*x4*u1 + ... (20 terms)
pseudo-remainder: [29 y3 2] = x1^2*y3^2*u1*y1 + ... (28 terms)
pseudo-remainder: [17 y1 2] = y2*u1^3*x2*y1^2 + ... (16 terms)
pseudo-remainder: [10 y4 1] = u1*y1*y4 + ... (9 terms)
pseudo-remainder: [21 x4 1] = -y1^2*x4*u1 + ... (20 terms)
pseudo-remainder: [29 y3 2] = -x1^2*y3^2*u1*y1 + ... (28 terms)
pseudo-remainder: [17 y1 2] = -y2*u1^3*x2*y1^2 + ... (16 terms)
pseudo-remainder: [10 y4 1] = u1^2*x3*y4 + ... (9 terms)
pseudo-remainder: [16 x4 1] = -x1*y1*x4*u1 + ... (15 terms)
pseudo-remainder: [24 y3 1] = -x1^2*y3*x3*u1*y1 + ... (23 terms)
pseudo-remainder: [10 y1 2] = -x2*y1^2*x3*u1^2 + ... (9 terms)
pseudo-remainder: [10 y4 1] = -u1^2*x1*x3*y4 + ... (9 terms)
pseudo-remainder: [17 x4 1] = -y2*x1^2*u1*x4 + ... (16 terms)
pseudo-remainder: [23 y3 1] = -x1^3*x3*y2*y3*u1 + ... (22 terms)
pseudo-remainder: [10 y1 2] = x2^2*y1^2*x3*u1^2 + ... (9 terms)
pseudo-remainder: [10 y4 1] = u1^2*x1*x3*y4 + ... (9 terms)
pseudo-remainder: [17 x4 1] = y2*x1^2*u1*x4 + ... (16 terms)
pseudo-remainder: [23 y3 1] = x1^3*x3*y2*y3*u1 + ... (22 terms)
pseudo-remainder: [10 y1 2] = -x2^2*y1^2*x3*u1^2 + ... (9 terms)
pseudo-remainder: [10 y4 1] = u1^2*x1*y2*y4 + ... (9 terms)
pseudo-remainder: [20 x4 1] = -y1*x4*y2*x1*u1 + ... (19 terms)
pseudo-remainder: [29 y3 2] = -x1^3*y3^2*y2*u1 + ... (28 terms)
pseudo-remainder: [18 y1 2] = y2*u1^3*x2^2*y1^2 + ... (17 terms)
pseudo-remainder: [11 y4 1] = -u1^2*x1*y2*y4 + ... (10 terms)
pseudo-remainder: [27 x4 1] = y1*x4*y2*x1*u1 + ... (26 terms)
pseudo-remainder: [25 y3 2] = x1^3*y3^2*y2*u1 + ... (24 terms)
pseudo-remainder: [17 y1 2] = -y2*u1^3*x2^2*y1^2 + ... (16 terms)
pseudo-remainder: [14 y4 1] = u1*x1*y4 + ... (13 terms)
pseudo-remainder: [26 x4 1] = -2*x1*y1*x4*u1 + ... (25 terms)
pseudo-remainder: [36 y3 2] = -x1^3*y3^2*u1 + ... (35 terms)
pseudo-remainder: [12 y1 2] = -x2*y1^2*x3*u1^2 + ... (11 terms)
pseudo-remainder: [14 y4 1] = -u1*x1*y4 + ... (13 terms)
pseudo-remainder: [26 x4 1] = 2*x1*y1*x4*u1 + ... (25 terms)
pseudo-remainder: [36 y3 2] = x1^3*y3^2*u1 + ... (35 terms)
pseudo-remainder: [12 y1 2] = x2*y1^2*x3*u1^2 + ... (11 terms)
pseudo-remainder: [14 y4 1] = -u1^2*x1*y4 + ... (13 terms)
pseudo-remainder: [29 x4 1] = y1*x4*u1^2*x1 + ... (28 terms)
pseudo-remainder: [38 y3 2] = x1^3*y3^2*u1^2 + ... (37 terms)
pseudo-remainder: [14 y1 2] = x2^2*y1^2*x3*u1^2 + ... (13 terms)
pseudo-remainder: [17 y4 1] = u1^2*x1*y4 + ... (16 terms)
pseudo-remainder: [30 x4 1] = -u1^2*x1*x4*y3 + ... (29 terms)
pseudo-remainder: [49 y3 2] = -x1^3*y3^2*u1^2 + ... (48 terms)
pseudo-remainder: [15 y1 2] = x2*y1^2*x3*u1^3 + ... (14 terms)
pseudo-remainder: [18 y4 1] = u1^2*y1*y4 + ... (17 terms)
pseudo-remainder: [36 x4 1] = -y1^2*x4*u1^2 + ... (35 terms)
pseudo-remainder: [51 y3 2] = -x1^2*y3^2*u1^2*y1 + ... (50 terms)
pseudo-remainder: [22 y1 2] = -y2*u1^4*x2*y1^2 + ... (21 terms)
pseudo-remainder: [18 y4 1] = -u1^2*y1*y4 + ... (17 terms)
pseudo-remainder: [41 x4 1] = y1^2*x4*u1^2 + ... (40 terms)
pseudo-remainder: [47 y3 2] = x1^2*y3^2*u1^2*y1 + ... (46 terms)
pseudo-remainder: [22 y1 2] = y2*u1^4*x2*y1^2 + ... (21 terms)
`The theorem is true under the following subsidiary conditions:`
. the line GD is non-isotropic
. `the line A` || (I) || ` is not parallel to the line ` || G || F
. the line AH is not parallel to the line GE
. u1-x5 <> 0
. -x5+x1 <> 0
. -x5+x2 <> 0
. the line DH is not perpendicular to the line DG
. the line AH is not perpendicular to the line GD
. -x5*y3+x5*y6+x2*y3-x2*y6+y2*x6-y2*x3-y5*x6+y5*x3 <> 0
QED.
-
Theorem([arbitrary(G,D), online(G,D,A), intersection(A,H,G,E,B), intersection(A,I,G,F,C), intersection(J,E,I,D,F), online(B,J,C), online(H,D,E)],[online(J,H,I)])
Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J} are reassigned
Theorem: If the points G and D are arbitrary, the point A is on the line GD, the two lines AH and GE intersect at B, `the two lines A` || (I) || ` and ` || G || F || ` intersect at ` || C , `the two lines JE and ` || (I) || D || ` intersect at ` || F , the point C is on the line BJ, and the point E is on the line HD, then `the point ` || (I) || ` is on the line ` || J || H .
Proof:
char set produced: [1 y1 1] [4 y3 1] [6 x4 1] [6 y4 1] [4 y6 1] [6 x7 1] [6 y7 1] [16 x8 1] [6 y8 1]
pseudo-remainder: [6 y8 1] = -x2*y8 + ... (5 terms)
pseudo-remainder: [16 x8 1] = x2*y3*x8 + ... (15 terms)
pseudo-remainder: [88 y7 1] = -x3^2*y7*x2*y5 + ... (87 terms)
pseudo-remainder: [120 x7 1] = x1*x2*x7*y3*y4 + ... (119 terms)
pseudo-remainder: [200 y6 2] = -x1^2*y6^2*x2*x3*y4 + ... (199 terms)
pseudo-remainder: [2 y4 1] = y1*y3*y4 + ... (1 terms)
pseudo-remainder: [4 x4 1] = -y3*y1^2*x4 + ... (3 terms)
pseudo-remainder: [8 y3 2] = -x1*y3^2*y1^2*x2 + ... (7 terms)
pseudo-remainder: [8 y1 2] = -y2^2*u1^2*x2*y1^2 + ... (7 terms)
pseudo-remainder: [2 y4 1] = -y1*y3*y4 + ... (1 terms)
pseudo-remainder: [4 x4 1] = y3*y1^2*x4 + ... (3 terms)
pseudo-remainder: [8 y3 2] = x1*y3^2*y1^2*x2 + ... (7 terms)
pseudo-remainder: [8 y1 2] = y2^2*u1^2*x2*y1^2 + ... (7 terms)
pseudo-remainder: [2 y4 1] = -u1^2*x2*y1*y3*y4 + ... (1 terms)
pseudo-remainder: [4 x4 1] = -y1*y3*y2*x4*x1 + ... (3 terms)
pseudo-remainder: [8 y3 2] = -x1^2*y3^2*x2*y1*y2 + ... (7 terms)
pseudo-remainder: [8 y1 2] = y2^2*u1^2*x2^2*y1^2 + ... (7 terms)
pseudo-remainder: [2 y4 1] = u1^2*x2*y1*y3*y4 + ... (1 terms)
pseudo-remainder: [4 x4 1] = y1*y3*y2*x4*x1 + ... (3 terms)
pseudo-remainder: [8 y3 2] = x1^2*y3^2*x2*y1*y2 + ... (7 terms)
pseudo-remainder: [8 y1 2] = -y2^2*u1^2*x2^2*y1^2 + ... (7 terms)
pseudo-remainder: [4 y4 1] = u1^2*y1*y3*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = -y1^2*x4*u1*y3 + ... (7 terms)
pseudo-remainder: [16 y3 2] = -x1*y3^2*x2*y1^2*u1 + ... (15 terms)
pseudo-remainder: [15 y1 2] = -y2^2*u1^3*x2*y1^2 + ... (14 terms)
pseudo-remainder: [4 y4 1] = 2*u1*y1*y3*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = -2*y1^2*x4*u1*y3 + ... (7 terms)
pseudo-remainder: [16 y3 2] = -2*x1*y3^2*x2*y1^2*u1 + ... (15 terms)
pseudo-remainder: [15 y1 2] = -2*y2^2*u1^3*x2*y1^2 + ... (14 terms)
pseudo-remainder: [4 y4 1] = -2*u1*y1*y3*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = 2*y1^2*x4*u1*y3 + ... (7 terms)
pseudo-remainder: [16 y3 2] = 2*x1*y3^2*x2*y1^2*u1 + ... (15 terms)
pseudo-remainder: [15 y1 2] = 2*y2^2*u1^3*x2*y1^2 + ... (14 terms)
pseudo-remainder: [4 y4 1] = -y2*x3*u1*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = x1*y3*y1*x4 + ... (7 terms)
pseudo-remainder: [8 y3 1] = x2*y1^2*x3*x1*y3 + ... (7 terms)
pseudo-remainder: [4 y1 2] = u1*x2*y1^2*x3*y2 + ... (3 terms)
pseudo-remainder: [4 y4 1] = -u1^2*y1*y3*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = y1^2*x4*u1*y3 + ... (7 terms)
pseudo-remainder: [16 y3 2] = x1*y3^2*x2*y1^2*u1 + ... (15 terms)
pseudo-remainder: [15 y1 2] = y2^2*u1^3*x2*y1^2 + ... (14 terms)
pseudo-remainder: [4 y4 1] = -y2*x1*u1^2*x3*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = -x1^2*y3*y2*x4 + ... (7 terms)
pseudo-remainder: [8 y3 1] = -x2*y1*x3*y3*y2*x1^2 + ... (7 terms)
pseudo-remainder: [4 y1 2] = y2*u1*x2^2*y1^2*x3 + ... (3 terms)
pseudo-remainder: [4 y4 1] = y2*x1*u1^2*x3*y4 + ... (3 terms)
pseudo-remainder: [8 x4 1] = x1^2*y3*y2*x4 + ... (7 terms)
pseudo-remainder: [8 y3 1] = x2*y1*x3*y3*y2*x1^2 + ... (7 terms)
pseudo-remainder: [4 y1 2] = -y2*u1*x2^2*y1^2*x3 + ... (3 terms)
pseudo-remainder: [6 x4 1] = -x1*u1*x4 + ... (5 terms)
pseudo-remainder: [12 y3 1] = -x1^2*y3*x3*u1 + ... (11 terms)
pseudo-remainder: [2 y1 1] = -x2*x3*u1*y1 + ... (1 terms)
pseudo-remainder: [6 x4 1] = x1*u1*x4 + ... (5 terms)
pseudo-remainder: [12 y3 1] = x1^2*y3*x3*u1 + ... (11 terms)
pseudo-remainder: [2 y1 1] = x2*x3*u1*y1 + ... (1 terms)
pseudo-remainder: [6 x4 1] = u1^2*x1*x4 + ... (5 terms)
pseudo-remainder: [12 y3 1] = x1^2*y3*x3*u1 + ... (11 terms)
pseudo-remainder: [2 y1 1] = x2*x3*u1*y1 + ... (1 terms)
pseudo-remainder: [6 x4 1] = -u1^2*x1*x4 + ... (5 terms)
pseudo-remainder: [12 y3 1] = -x1^2*y3*x3*u1 + ... (11 terms)
pseudo-remainder: [2 y1 1] = -x2*x3*u1*y1 + ... (1 terms)
pseudo-remainder: [8 y4 1] = u1^2*x3*y2*y4 + ... (7 terms)
pseudo-remainder: [16 x4 1] = -x1*u1*y1*y3*x4 + ... (15 terms)
pseudo-remainder: [16 y3 1] = -x2*y1^2*x3*x1*y3*u1 + ... (15 terms)
pseudo-remainder: [8 y1 2] = -y2*u1^2*x2*y1^2*x3 + ... (7 terms)
pseudo-remainder: [10 y4 1] = -u1*y1*y4 + ... (9 terms)
pseudo-remainder: [21 x4 1] = y1^2*x4*u1 + ... (20 terms)
pseudo-remainder: [29 y3 2] = x1^2*y3^2*u1*y1 + ... (28 terms)
pseudo-remainder: [17 y1 2] = y2*u1^3*x2*y1^2 + ... (16 terms)
pseudo-remainder: [10 y4 1] = u1*y1*y4 + ... (9 terms)
pseudo-remainder: [21 x4 1] = -y1^2*x4*u1 + ... (20 terms)
pseudo-remainder: [29 y3 2] = -x1^2*y3^2*u1*y1 + ... (28 terms)
pseudo-remainder: [17 y1 2] = -y2*u1^3*x2*y1^2 + ... (16 terms)
pseudo-remainder: [10 y4 1] = -u1^2*x3*y4 + ... (9 terms)
pseudo-remainder: [16 x4 1] = x1*y1*x4*u1 + ... (15 terms)
pseudo-remainder: [24 y3 1] = x1^2*y3*x3*u1*y1 + ... (23 terms)
pseudo-remainder: [10 y1 2] = x2*y1^2*x3*u1^2 + ... (9 terms)
pseudo-remainder: [10 y4 1] = -u1^2*x1*x3*y4 + ... (9 terms)
pseudo-remainder: [17 x4 1] = -y2*x1^2*u1*x4 + ... (16 terms)
pseudo-remainder: [23 y3 1] = -x1^3*x3*y2*y3*u1 + ... (22 terms)
pseudo-remainder: [10 y1 2] = x2^2*y1^2*x3*u1^2 + ... (9 terms)
pseudo-remainder: [10 y4 1] = u1^2*x1*x3*y4 + ... (9 terms)
pseudo-remainder: [17 x4 1] = y2*x1^2*u1*x4 + ... (16 terms)
pseudo-remainder: [23 y3 1] = x1^3*x3*y2*y3*u1 + ... (22 terms)
pseudo-remainder: [10 y1 2] = -x2^2*y1^2*x3*u1^2 + ... (9 terms)
pseudo-remainder: [10 y4 1] = -u1^2*x1*y2*y4 + ... (9 terms)
pseudo-remainder: [20 x4 1] = y1*x4*y2*x1*u1 + ... (19 terms)
pseudo-remainder: [29 y3 2] = x1^3*y3^2*y2*u1 + ... (28 terms)
pseudo-remainder: [18 y1 2] = -y2*u1^3*x2^2*y1^2 + ... (17 terms)
pseudo-remainder: [11 y4 1] = u1^2*x1*y2*y4 + ... (10 terms)
pseudo-remainder: [27 x4 1] = -y1*x4*y2*x1*u1 + ... (26 terms)
pseudo-remainder: [25 y3 2] = -x1^3*y3^2*y2*u1 + ... (24 terms)
pseudo-remainder: [17 y1 2] = y2*u1^3*x2^2*y1^2 + ... (16 terms)
pseudo-remainder: [14 y4 1] = u1*x1*y4 + ... (13 terms)
pseudo-remainder: [26 x4 1] = -2*x1*y1*x4*u1 + ... (25 terms)
pseudo-remainder: [36 y3 2] = -x1^3*y3^2*u1 + ... (35 terms)
pseudo-remainder: [12 y1 2] = -x2*y1^2*x3*u1^2 + ... (11 terms)
pseudo-remainder: [14 y4 1] = -u1*x1*y4 + ... (13 terms)
pseudo-remainder: [26 x4 1] = 2*x1*y1*x4*u1 + ... (25 terms)
pseudo-remainder: [36 y3 2] = x1^3*y3^2*u1 + ... (35 terms)
pseudo-remainder: [12 y1 2] = x2*y1^2*x3*u1^2 + ... (11 terms)
pseudo-remainder: [14 y4 1] = u1^2*x1*y4 + ... (13 terms)
pseudo-remainder: [29 x4 1] = -y1*x4*u1^2*x1 + ... (28 terms)
pseudo-remainder: [38 y3 2] = -x1^3*y3^2*u1^2 + ... (37 terms)
pseudo-remainder: [14 y1 2] = -x2^2*y1^2*x3*u1^2 + ... (13 terms)
pseudo-remainder: [17 y4 1] = -u1^2*x1*y4 + ... (16 terms)
pseudo-remainder: [30 x4 1] = u1^2*x1*x4*y3 + ... (29 terms)
pseudo-remainder: [49 y3 2] = x1^3*y3^2*u1^2 + ... (48 terms)
pseudo-remainder: [15 y1 2] = -x2*y1^2*x3*u1^3 + ... (14 terms)
pseudo-remainder: [18 y4 1] = -u1^2*y1*y4 + ... (17 terms)
pseudo-remainder: [36 x4 1] = y1^2*x4*u1^2 + ... (35 terms)
pseudo-remainder: [51 y3 2] = x1^2*y3^2*u1^2*y1 + ... (50 terms)
pseudo-remainder: [22 y1 2] = y2*u1^4*x2*y1^2 + ... (21 terms)
pseudo-remainder: [18 y4 1] = u1^2*y1*y4 + ... (17 terms)
pseudo-remainder: [41 x4 1] = -y1^2*x4*u1^2 + ... (40 terms)
pseudo-remainder: [47 y3 2] = -x1^2*y3^2*u1^2*y1 + ... (46 terms)
pseudo-remainder: [22 y1 2] = -y2*u1^4*x2*y1^2 + ... (21 terms)
`The theorem is true under the following subsidiary conditions:`
. the line GD is non-isotropic
. `the line A` || (I) || ` is not parallel to the line ` || G || F
. the line AH is not parallel to the line GE
. u1-x5 <> 0
. -x5+x1 <> 0
. the line DH is not perpendicular to the line DG
. the line AH is not perpendicular to the line GD
. the line DG is not perpendicular to the line FE
. the line BC is not parallel to the line EF
QED.
-
Theorem([arbitrary(A,G,H,E), intersection(A,H,G,E,B), intersection(A,I,G,F,C), intersection(J,E,I,D,F), online(J,H,I), online(B,J,C), online(H,D,E)],[online(G,D,A)])
Warning: the coordinates of the points from {I, A, B, C, D, E, F, G, H, J} are reassigned
Theorem: If the points A, G, H, and E are arbitrary, the two lines AH and GE intersect at B, `the two lines A` || (I) || ` and ` || G || F || ` intersect at ` || C , `the two lines JE and ` || (I) || D || ` intersect at ` || F , `the point ` || (I) || ` is on the line ` || J || H , the point C is on the line BJ, and the point E is on the line HD, then the point A is on the line GD.
Proof:
char set produced: [6 x1 1] [3 y1 1] [96 y3 2] [8 x4 1] [4 y4 1] [10 x5 1] [4 y5 1] [10 x6 1] [4 y6 1]
pseudo-remainder: [2 y6 1] = -y6*u1 + ... (1 terms)
pseudo-remainder: [6 x6 1] = -x6*v1*u1 + ... (5 terms)
pseudo-remainder: [12 y3 1] = u3^2*y3*u1*v1 + ... (11 terms)
pseudo-remainder: [12 y1 0] = -u1*y2*u3*v1 + ... (11 terms)
pseudo-remainder: [12 x1 0] = -u1*y2*u3*v1 + ... (11 terms)
the thoerem is possibly false: further decomposition in progress
char set produced: [1 u1 1] [1 x1 1] [3 y1 1] [24 y3 2] [4 x4 1] [4 y4 1] [10 x5 1] [12 y5 1] [10 x6 1] [12 y6 1]
char set produced: [1 u3 1] [4 x1 1] [4 y1 1] [6 y3 2] [8 x4 1] [6 y4 1] [6 x5 1] [8 y5 1] [1 x6 1] [4 y6 1]
char set produced: [6 x1 1] [5 y1 1] [1 x2 1] [16 y3 2] [6 x4 1] [5 y4 1] [1 x5 1] [4 y5 1] [6 x6 1] [8 y6 1]
char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [8 x4 1] [5 y4 1] [10 x5 1] [12 y5 1] [10 x6 1] [12 y6 1]
pseudo-remainder: [2 y6 1] = -y6*u1 + ... (1 terms)
pseudo-remainder: [6 x2 1] = x2*y3*v1 + ... (5 terms)
pseudo-remainder: [6 y1 0] = -y3*u1*v1 + ... (5 terms)
pseudo-remainder: [6 x1 0] = -y3*u1*v1 + ... (5 terms)
the thoerem is possibly false: further decomposition in progress
Status: used = 38132, alloced = 23530, time = 7.441000000000001
char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [24 y3 2] [2 x4 1] [4 y4 1] [10 x5 1] [12 y5 1] [10 x6 1] [12 y6 1]
char set produced: [6 x1 1] [5 y1 1] [3 y2 1] [6 x4 1] [5 y4 1] [8 x5 1] [8 y5 1] [10 x6 1] [16 y6 1]
pseudo-remainder: [2 y6 1] = -y6*u1 + ... (1 terms)
pseudo-remainder: [18 y2 0] = u1^2*u3*v1^2 + ... (17 terms)
pseudo-remainder: [18 y1 0] = u1^2*u3*v1^2 + ... (17 terms)
pseudo-remainder: [18 x1 0] = u1^2*u3*v1^2 + ... (17 terms)
the thoerem is possibly false: further decomposition in progress
char set produced: [6 x1 1] [5 y1 1] [4 y3 1] [8 x4 1] [6 y4 1] [8 x5 1] [8 y5 1] [18 x6 1] [22 y6 1]
pseudo-remainder: [2 y6 1] = -y6*u1 + ... (1 terms)
pseudo-remainder: [24 y3 0] = u2*u1*v2*v1*u3 + ... (23 terms)
pseudo-remainder: [24 y1 0] = u2*u1*v2*v1*u3 + ... (23 terms)
pseudo-remainder: [24 x1 0] = u2*u1*v2*v1*u3 + ... (23 terms)
the thoerem is possibly false: further decomposition in progress
char set produced: [6 x1 1] [5 y1 1] [6 y3 1] [18 x4 1] [14 y4 1] [6 x5 1] [8 y5 1] [3 x6 1] [1 y6 1]
pseudo-remainder: [2 y6 1] = -y6*u1 + ... (1 terms)
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [2 u2 1] [2 x1 1] [1 y1 1] [2 x4 1] [1 y4 1] [10 x5 1] [12 y5 1] [10 x6 1] [12 y6 1]
pseudo-remainder: [2 y6 1] = -y6*u1 + ... (1 terms)
pseudo-remainder: [12 y4 0] = u1*y2*u3*v1 + ... (11 terms)
pseudo-remainder: [12 x4 0] = u1*y2*u3*v1 + ... (11 terms)
pseudo-remainder: [12 y1 0] = u1*y2*u3*v1 + ... (11 terms)
pseudo-remainder: [12 x1 0] = u1*y2*u3*v1 + ... (11 terms)
pseudo-remainder: [12 u2 1] = -y2*u2*u3*v1 + ... (11 terms)
char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [24 y3 2] [2 x4 1] [4 y4 1] [10 x5 1] [12 y5 1] [10 x6 1] [12 y6 1]
char set produced: [1 O 0]
char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [2 x3 1] [6 y3 1] [2 x4 1] [4 y4 1] [29 x5 1] [8 y5 1] [26 x6 1] [14 y6 1]
char set produced: [6 x1 1] [5 y1 1] [2 x2 1] [3 x3 1] [14 x4 1] [9 y4 1] [8 x5 1] [16 y5 1] [15 x6 1] [8 y6 1]
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [6 x1 1] [5 y1 1] [3 y2 1] [2 x3 1] [6 x4 1] [5 y4 1] [2 x5 1] [3 y5 1] [8 x6 1] [10 y6 1]
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [1 O 0]
char set produced: [6 x1 1] [5 y1 1] [1 y2 1] [2 x3 1] [1 y3 1] [2 x4 1] [1 y4 1] [6 x5 1] [5 y5 1] [3 x6 1] [1 y6 1]
char set produced: [1 O 0]
char set produced: [1 O 0]
`The theorem is true under the following subsidiary conditions:`
. the line AH is not parallel to the line GE
. x2 <> 0
. u1-x2 <> 0
. v1*u1-y2*u1-v1*x2 <> 0
. the line AH is not perpendicular to the line AG
. v1*u3-v1*x2+x2*v2 <> 0
. -y2*u2+y2*u3-x2*v2+u1*v2 <> 0
. y2*u3-x2*v2-v1*u3+v1*u2-y2*u2 <> 0
. the line AG is not parallel to the line EH
. the line AG is not perpendicular to the line EG
. the line AG is not perpendicular to the line EH
. the line AH is not parallel to the line GF
. the line AG is not perpendicular to the line FG
. y2*u1*v2-u1*v2*y4-y2*u3*y4+y2*u2*y4+x2*v2*y4-u2*v2*y2 <> 0
. -y2*u1*u2+y2*x4*u2-v2*u2*x2+u1*v2*u2+u1*u3*y2-u3*y2*x4+v2*x2*x4-u1*v2*x4 <> 0
. -v1*u2*y3+u2*v1*y4-u1*y3*y4-v1*x3*y4+y3*u1*v1 <> 0
. -v1*x3*u1+y3*u1*x4+v1*u1*u2-u1*y3*u2+v1*x3*x4-v1*u2*x4 <> 0
. v1*u3-v1*x3+x2*v2 <> 0
. x2*v2-x2*y3-v1*x3+v1*u3+y2*x3-y2*u3 <> 0
. y2*u3-u3*y3-x2*v2+v2*x3+v1*x2-v1*x3 <> 0
. -u3*y3*u1-u1*v2*x2+v2*x3*u1+u1*v1*x2-v1*x3*u1+u1*u3*v1-v1*u3*x2 <> 0
. v1*u3*x3-u2*u3*v1+v1*x2*u2-v2*u2*x2-v1*u3*x2+u1*u3*v1+v2*x3*u1-v1*x3*u1 <> 0
. u3^2*y2-v2*u3*x2+v1*u3*x2-v1*u3*x3-y2*u2*u3+v2*u2*x2-u2*v2*x3-v1*x2*u2+u2*v1*x3+u2*u3*v2 <> 0
. the three points E, F and G are not collinear
. the line AH is not parallel to the line FE
. -v1*u3*x2+v1*x5*u3-y2*x5*u3-v2*u2*x2+x2*v2*x5+v1*x2*u2-v1*u2*x5+u2*y2*x5 <> 0
. -y2*u3*y5-v1*x2*v2+x2*v2*y5+v1*u3*y5-v1*u2*y5+y2*u2*y5+v1*v2*u2-u2*v2*y2 <> 0
. -u1*u3*x2*y3+u1*u3*y3*x6+u1*u3*v1*x2+u1*x6*v2*x2-u1*x6*v2*x3-u1*x6*v1*x2+u1*x6*v1*x3-v1*u1*u3*x6+v1*x2*u3*x6-u3*v1*x2*x3 <> 0
. u1*u3*y3*y6-u1*u3*y3*v1+u1*v2*x2*y6-u1*v2*x3*y6+u1*v2*x3*v1-u1*v1*x2*y6+v1*u1*x3*y6-u1*v1^2*x3-u3*v1*u1*y6+u1*u3*v1^2+v1*u3*x2*y6-u3*v1^2*x2-x2*y3*u1*v2+u1*x2*y3*v1-v1*x2*x3*v2+v1^2*x2*x3 <> 0
. u3^2*y2*x6-u3^2*x3*y2-u3^2*v1*x2+v1*u3^2*x3-u3*x6*v2*x2+v1*x2*u3*x6-u3*x6*v1*x3-u2*u3*y2*x6+u2*u3*y2*x3+x2*u2*u3*v1-v1*x3*u2*u3+u2*x6*v2*x2-u2*x6*v2*x3-u2*x6*v1*x2+u2*x6*v1*x3+v2*x3*u3*x2-v2*u2*u3*x2+v2*u2*u3*x6 <> 0
. -u3^2*y2*y6-v1*u3*x3*v2+u3*y2*x3*v2-v2*u2*x2*v1-v2*u2*x2*y6+u2*v2*x3*y6+v1*x2*u2*y6-u2*v1*x3*y6-v1*u3*x2*y6+v1*x2*x3*v2+v1*v2*u2*u3+v1*u3^2*y2-v2^2*x3*x2+v2*u3*x2*y6+u3*v1*x3*y6-u2*u3*v2*y6+v2^2*u2*x2-y2*u2*u3*v1-y2*x3*v2*u2+y2*x3*v1*u2+u2*u3*y2*y6-u3*y2*x3*v1 <> 0
. u1*v2*v1-u1*v2*y5-y3*u1*v1+y3*u1*y5+v1*x3*y5-v1*u3*y5+u3*y3*v1-v2*x3*v1 <> 0
. v2*x3*u1-u1*v2*x5+v1*x5*x3-v1*x5*u3-v1*x3*u1+u1*u3*v1-u3*y3*u1+y3*u1*x5 <> 0
QED.