1Thu Jan 28 23:37:50 MET 1999 2REDUCE 3.7, 15-Jan-99 ... 3 41: 1: 52: 2: 2: 2: 2: 2: 2: 2: 2: 6 Geometry 1.1 Last update Sept 6, 1998 7 83: 3: % Author H.-G. Graebe | Univ. Leipzig | Version 6.9.1998 9% graebe@informatik.uni-leipzig.de 10 11comment 12 13Test suite for the package GEOMETRY 1.1 14 15end comment; 16 17 18algebraic; 19 20 21load cali,geometry; 22 23 24off nat; 25 26 27on echo; 28 29 30showtime; 31 32 33Time: 190 ms 34 35 36 37% ##################### 38% Some one line proofs 39% ##################### 40 41% A generic triangle ABC 42 43A:=Point(a1,a2); 44 45 46a := {a1,a2}$ 47 B:=Point(b1,b2); 48 49 50b := {b1,b2}$ 51 C:=Point(c1,c2); 52 53 54c := {c1,c2}$ 55 56 57% Its midpoint perpendiculars have a point in common: 58 59 concurrent(mp(a,b),mp(b,c),mp(c,a)); 60 61 620$ 63 64 65% This point 66 67 M:=intersection_point(mp(a,b),mp(b,c)); 68 69 70m := {(a1**2*b2 - a1**2*c2 + a2**2*b2 - a2**2*c2 - a2*b1**2 - a2*b2**2 + a2*c1** 712 + a2*c2**2 + b1**2*c2 + b2**2*c2 - b2*c1**2 - b2*c2**2)/(2*(a1*b2 - a1*c2 - a2 72*b1 + a2*c1 + b1*c2 - b2*c1)), 73( - a1**2*b1 + a1**2*c1 + a1*b1**2 + a1*b2**2 - a1*c1**2 - a1*c2**2 - a2**2*b1 + 74 a2**2*c1 - b1**2*c1 + b1*c1**2 + b1*c2**2 - b2**2*c1)/(2*(a1*b2 - a1*c2 - a2*b1 75 + a2*c1 + b1*c2 - b2*c1))}$ 76 77 78% is the center of the circumscribed circle 79 80 sqrdist(M,A) - sqrdist(M,B); 81 82 830$ 84 85 86% The altitutes intersection theorem 87 88 concurrent(altitude(a,b,c),altitude(b,c,a),altitude(c,a,b)); 89 90 910$ 92 93 94% The median intersection theorem 95 96 concurrent(median(a,b,c),median(b,c,a),median(c,a,b)); 97 98 990$ 100 101 102% Euler's line 103 104 M:=intersection_point(mp(a,b),mp(b,c)); 105 106 107m := {(a1**2*b2 - a1**2*c2 + a2**2*b2 - a2**2*c2 - a2*b1**2 - a2*b2**2 + a2*c1** 1082 + a2*c2**2 + b1**2*c2 + b2**2*c2 - b2*c1**2 - b2*c2**2)/(2*(a1*b2 - a1*c2 - a2 109*b1 + a2*c1 + b1*c2 - b2*c1)), 110( - a1**2*b1 + a1**2*c1 + a1*b1**2 + a1*b2**2 - a1*c1**2 - a1*c2**2 - a2**2*b1 + 111 a2**2*c1 - b1**2*c1 + b1*c1**2 + b1*c2**2 - b2**2*c1)/(2*(a1*b2 - a1*c2 - a2*b1 112 + a2*c1 + b1*c2 - b2*c1))}$ 113 114 H:=intersection_point(altitude(a,b,c),altitude(b,c,a)); 115 116 117h := {( - a1*a2*b1 + a1*a2*c1 + a1*b1*b2 - a1*c1*c2 - a2**2*b2 + a2**2*c2 + a2* 118b2**2 - a2*c2**2 - b1*b2*c1 + b1*c1*c2 - b2**2*c2 + b2*c2**2)/(a1*b2 - a1*c2 - 119a2*b1 + a2*c1 + b1*c2 - b2*c1), 120(a1**2*b1 - a1**2*c1 + a1*a2*b2 - a1*a2*c2 - a1*b1**2 + a1*c1**2 - a2*b1*b2 + a2 121*c1*c2 + b1**2*c1 + b1*b2*c2 - b1*c1**2 - b2*c1*c2)/(a1*b2 - a1*c2 - a2*b1 + a2* 122c1 + b1*c2 - b2*c1)}$ 123 124 S:=intersection_point(median(a,b,c),median(b,c,a)); 125 126 127s := {(a1 + b1 + c1)/3,(a2 + b2 + c2)/3}$ 128 129 130 collinear(M,H,S); 131 132 1330$ 134 135 sqrdist(S,varpoint(M,H,2/3)); 136 137 1380$ 139 140 141% Feuerbach's circle 142 143 % Choose a special coordinate system 144 A:=Point(0,0); 145 146 147a := {0,0}$ 148 B:=Point(u1,0); 149 150 151b := {u1,0}$ 152 C:=Point(u2,u3); 153 154 155c := {u2,u3}$ 156 157 158 M:=intersection_point(mp(a,b),mp(b,c)); 159 160 161m := {u1/2,( - u1*u2 + u2**2 + u3**2)/(2*u3)}$ 162 163 H:=intersection_point(altitude(a,b,c),altitude(b,c,a)); 164 165 166h := {u2,(u2*(u1 - u2))/u3}$ 167 168 N:=midpoint(M,H); 169 170 171n := {(u1 + 2*u2)/4,(u1*u2 - u2**2 + u3**2)/(4*u3)}$ 172 173 174 sqrdist(N,midpoint(A,B))-sqrdist(N,midpoint(B,C)); 175 176 1770$ 178 179 sqrdist(N,midpoint(A,B))-sqrdist(N,midpoint(H,C)); 180 181 1820$ 183 184 185 D:=intersection_point(pp_line(A,B),pp_line(H,C)); 186 187 188d := {u2,0}$ 189 190 191 sqrdist(N,midpoint(A,B))-sqrdist(N,D); 192 193 1940$ 195 196 197clear_ndg(); 198 199 200{}$ 201 clear(A,B,C,D,M,H,S,N); 202 203 204 205% ############################# 206% Non-linear Geometric Objects 207% ############################# 208 209% Bisector intersection theorem 210 211A:=Point(0,0); 212 213 214a := {0,0}$ 215 B:=Point(1,0); 216 217 218b := {1,0}$ 219 C:=Point(u1,u2); 220 221 222c := {u1,u2}$ 223 224P:=Point(x1,x2); 225 226 227p := {x1,x2}$ 228 229 230polys:={ 231 point_on_bisector(P,A,B,C), 232 point_on_bisector(P,B,C,A), 233 point_on_bisector(P,C,A,B)}; 234 235 236polys := { - 2*u1*x1*x2 + 2*u1*x2 + u2*x1**2 - 2*u2*x1 - u2*x2**2 + u2 + 2*x1*x2 237 - 2*x2, 238 - 2*u1**3*x2 + 2*u1**2*u2*x1 - u1**2*u2 + 2*u1**2*x1*x2 + 2*u1**2*x2 - 2*u1*u2 239**2*x2 - 2*u1*u2*x1**2 + 2*u1*u2*x2**2 - 2*u1*x1*x2 + 2*u2**3*x1 - u2**3 - 2*u2 240**2*x1*x2 + 2*u2**2*x2 + u2*x1**2 - u2*x2**2, 2412*u1*x1*x2 - u2*x1**2 + u2*x2**2}$ 242 243 244con1:=num(sqrdist(P,pedalpoint(p,pp_line(A,C)))-x2^2); 245 246 247con1 := u2*( - 2*u1**3*x1*x2 + u1**2*u2*x1**2 - u1**2*u2*x2**2 - 2*u1*u2**2*x1* 248x2 + u2**3*x1**2 - u2**3*x2**2)$ 249 250con2:=num(sqrdist(p,pedalpoint(p,pp_line(B,C)))-x2^2); 251 252 253con2 := u2*( - 2*u1**3*x1*x2 + 2*u1**3*x2 + u1**2*u2*x1**2 - 2*u1**2*u2*x1 - u1 254**2*u2*x2**2 + u1**2*u2 + 6*u1**2*x1*x2 - 6*u1**2*x2 - 2*u1*u2**2*x1*x2 + 2*u1* 255u2**2*x2 - 2*u1*u2*x1**2 + 4*u1*u2*x1 + 2*u1*u2*x2**2 - 2*u1*u2 - 6*u1*x1*x2 + 6 256*u1*x2 + u2**3*x1**2 - 2*u2**3*x1 - u2**3*x2**2 + u2**3 + 2*u2**2*x1*x2 - 2*u2** 2572*x2 + u2*x1**2 - 2*u2*x1 - u2*x2**2 + u2 + 2*x1*x2 - 2*x2)$ 258 259 260setring({x1,x2},{},lex); 261 262 263{{x1,x2},{},lex,{1,1}}$ 264 265setideal(polys,polys); 266 267 268{u2*x1**2 - (2*u1 - 2)*x1*x2 - (2*u2)*x1 - u2*x2**2 + (2*u1 - 2)*x2 + u2, 269 - (2*u1*u2 - u2)*x1**2 + (2*u1**2 - 2*u1 - 2*u2**2)*x1*x2 + (2*u1**2*u2 + 2*u2 270**3)*x1 + (2*u1*u2 - u2)*x2**2 - (2*u1**3 - 2*u1**2 + 2*u1*u2**2 - 2*u2**2)*x2 - 271 (u1**2*u2 + u2**3), 272 - u2*x1**2 + (2*u1)*x1*x2 + u2*x2**2}$ 273 274gbasis polys; 275 276 277{(4*u2)*x2**4 - (8*u1**2 - 8*u1 + 8*u2**2)*x2**3 + (4*u1**2*u2 - 4*u1*u2 + 4*u2 278**3 - 4*u2)*x2**2 + (4*u2**2)*x2 - u2**3, 279(2*u1*u2**2 - u2**2)*x1 + (2*u2)*x2**3 - (4*u1**2 - 4*u1 + 2*u2**2)*x2**2 - (2* 280u1**2*u2 - 2*u1*u2 + 2*u2)*x2 - (u1*u2**2 - u2**2)}$ 281 282{con1,con2} mod gbasis polys; 283 284 285{0,0}$ 286 287 288% Bisector intersection theorem. A constructive proof. 289 290A:=Point(0,0); 291 292 293a := {0,0}$ 294 B:=Point(1,0); 295 296 297b := {1,0}$ 298 P:=Point(u1,u2); 299 300 301p := {u1,u2}$ 302 303l1:=pp_line(A,B); 304 305 306l1 := {0,-1,0}$ 307 308l2:=symline(l1,pp_line(A,P)); 309 310 311l2 := { - 2*u1*u2,u1**2 - u2**2,0}$ 312 313l3:=symline(l1,pp_line(B,P)); 314 315 316l3 := {2*u2*( - u1 + 1), 317u1**2 - 2*u1 - u2**2 + 1, 3182*u2*(u1 - 1)}$ 319 320 321point_on_bisector(P,A,B,intersection_point(l2,l3)); 322 323 3240$ 325 326 327clear_ndg(); 328 329 330{}$ 331 clear(A,B,C,P,l1,l2,l3); 332 333 334 335% Miquel's theorem 336 337on gcd; 338 339 340A:=Point(0,0); 341 342 343a := {0,0}$ 344 B:=Point(1,0); 345 346 347b := {1,0}$ 348 C:=Point(c1,c2); 349 350 351c := {c1,c2}$ 352 353P:=choose_pl(pp_line(A,B),u1); 354 355 356p := {u1,0}$ 357 358Q:=choose_pl(pp_line(B,C),u2); 359 360 361q := {u2,(c2*(u2 - 1))/(c1 - 1)}$ 362 363R:=choose_pl(pp_line(A,C),u3); 364 365 366r := {u3,(c2*u3)/c1}$ 367 368 369X:=other_cc_point(P,p3_circle(A,P,R),p3_circle(B,P,Q))$ 370 371 372 373point_on_circle(X,p3_circle(C,Q,R)); 374 375 3760$ 377 378 379off gcd; 380 381 382clear_ndg(); 383 384 385{}$ 386 clear(A,B,C,P,Q,R,X); 387 388 389 390% ######################## 391% Theorems of linear type 392% ######################## 393 394% Pappus' theorem 395 396A:=Point(u1,u2); 397 398 399a := {u1,u2}$ 400 B:=Point(u3,u4); 401 402 403b := {u3,u4}$ 404 C:=Point(x1,u5); 405 406 407c := {x1,u5}$ 408 409P:=Point(u6,u7); 410 411 412p := {u6,u7}$ 413 Q:=Point(u8,u9); 414 415 416q := {u8,u9}$ 417 R:=Point(u0,x2); 418 419 420r := {u0,x2}$ 421 422 423polys:={collinear(A,B,C), collinear(P,Q,R)}; 424 425 426polys := {u1*u4 - u1*u5 - u2*u3 + u2*x1 + u3*u5 - u4*x1, 427u0*u7 - u0*u9 + u6*u9 - u6*x2 - u7*u8 + u8*x2}$ 428 429 430con:=collinear( 431 intersection_point(pp_line(A,Q),pp_line(P,B)), 432 intersection_point(pp_line(A,R),pp_line(P,C)), 433 intersection_point(pp_line(B,R),pp_line(Q,C)))$ 434 435 436 437vars:={x1,x2}; 438 439 440vars := {x1,x2}$ 441 442sol:=solve(polys,vars); 443 444 445sol := {{x1=( - u1*u4 + u1*u5 + u2*u3 - u3*u5)/(u2 - u4), 446x2=(u0*u7 - u0*u9 + u6*u9 - u7*u8)/(u6 - u8)}}$ 447 448 449sub(sol,con); 450 451 4520$ 453 454 455% Pappus' theorem. A constructive approach 456 457A:=Point(u1,u2); 458 459 460a := {u1,u2}$ 461 B:=Point(u3,u4); 462 463 464b := {u3,u4}$ 465 466P:=Point(u6,u7); 467 468 469p := {u6,u7}$ 470 Q:=Point(u8,u9); 471 472 473q := {u8,u9}$ 474 475 476C:=choose_pl(pp_line(A,B),u5); 477 478 479c := {u5, 480(u1*u4 - u2*u3 + u2*u5 - u4*u5)/(u1 - u3)}$ 481 482R:=choose_pl(pp_line(P,Q),u0); 483 484 485r := {u0, 486(u0*u7 - u0*u9 + u6*u9 - u7*u8)/(u6 - u8)}$ 487 488 489con:=collinear(intersection_point(pp_line(A,Q),pp_line(P,B)), 490 intersection_point(pp_line(A,R),pp_line(P,C)), 491 intersection_point(pp_line(B,R),pp_line(Q,C))); 492 493 494con := 0$ 495 496 497clear_ndg(); 498 499 500{}$ 501 clear(A,B,C,P,Q,R); 502 503 504 505% ########################### 506% Theorems of non linear type 507% ########################### 508 509% Fermat Point 510 511A:=Point(0,0); 512 513 514a := {0,0}$ 515 B:=Point(0,2); 516 517 518b := {0,2}$ 519 C:=Point(u1,u2); 520 521 522c := {u1,u2}$ 523 524P:=Point(x1,x2); 525 526 527p := {x1,x2}$ 528 Q:=Point(x3,x4); 529 530 531q := {x3,x4}$ 532 R:=Point(x5,x6); 533 534 535r := {x5,x6}$ 536 537 538polys1:={sqrdist(P,B)-sqrdist(B,C), sqrdist(P,C)-sqrdist(B,C), 539 sqrdist(Q,A)-sqrdist(A,C), sqrdist(Q,C)-sqrdist(A,C), 540 sqrdist(R,B)-sqrdist(A,B), sqrdist(R,A)-sqrdist(A,B)}; 541 542 543polys1 := { - u1**2 - u2**2 + 4*u2 + x1**2 + x2**2 - 4*x2, 544 - 2*u1*x1 - 2*u2*x2 + 4*u2 + x1**2 + x2**2 - 4, 545 - u1**2 - u2**2 + x3**2 + x4**2, 546 - 2*u1*x3 - 2*u2*x4 + x3**2 + x4**2, 547x5**2 + x6**2 - 4*x6, 548x5**2 + x6**2 - 4}$ 549 550 551con:=concurrent(pp_line(A,P), pp_line(B,Q), pp_line(C,R)); 552 553 554con := - u1*x1*x4*x6 + 2*u1*x1*x6 + u1*x2*x3*x6 - 2*u1*x2*x3 + 2*u2*x1*x3 + u2* 555x1*x4*x5 - 2*u2*x1*x5 - u2*x2*x3*x5 - 2*x1*x3*x6 + 2*x2*x3*x5$ 556 557 558vars:={x1,x2,x3,x4,x5,x6}; 559 560 561vars := {x1, 562x2, 563x3, 564x4, 565x5, 566x6}$ 567 568setring(vars,{},lex); 569 570 571{{x1,x2,x3,x4,x5,x6},{},lex,{1,1,1,1,1,1}}$ 572 573iso:=isolatedprimes polys1; 574 575 576iso := {{x5**2 - 3, 577x6 - 1, 578u1*x5 - u2 + 2*x4, 579 - u1*x5 - u2 + 2*x2 - 2, 580 - u1 - u2*x5 + 2*x3, 581 - u1 + u2*x5 + 2*x1 - 2*x5}, 582{x5**2 - 3, 583x6 - 1, 584 - u1*x5 - u2 + 2*x4, 585u1*x5 - u2 + 2*x2 - 2, 586 - u1 + u2*x5 + 2*x3, 587 - u1 - u2*x5 + 2*x1 + 2*x5}, 588{x5**2 - 3, 589x6 - 1, 590u1*x5 - u2 + 2*x4, 591u1*x5 - u2 + 2*x2 - 2, 592 - u1 - u2*x5 + 2*x3, 593 - u1 - u2*x5 + 2*x1 + 2*x5}, 594{x5**2 - 3, 595x6 - 1, 596 - u1*x5 - u2 + 2*x4, 597 - u1*x5 - u2 + 2*x2 - 2, 598 - u1 + u2*x5 + 2*x3, 599 - u1 + u2*x5 + 2*x1 - 2*x5}}$ 600 601 602for each u in iso collect con mod u; 603 604 605{ - 3*u1**2*u2 + 3*u1**2 - 2*u1*u2*x5 + 2*u1*x5 - 3*u2**3 + 9*u2**2 - 6*u2, 6060, 607(u1**3*x5 + 3*u1**2*u2 - 6*u1**2 + u1*u2**2*x5 - 4*u1*u2*x5 + 3*u2**3 - 18*u2**2 608 + 24*u2)/2, 609( - u1**3*x5 + 3*u1**2*u2 - u1*u2**2*x5 + 4*u1*x5 + 3*u2**3 - 12*u2)/2}$ 610 611 612polys2:={sqrdist(P,B)-sqrdist(P,C), 613 sqrdist(Q,A)-sqrdist(Q,C), 614 sqrdist(R,A)-sqrdist(R,B), 615 num(p3_angle(R,A,B)-p3_angle(P,B,C)), 616 num(p3_angle(Q,C,A)-p3_angle(P,B,C))}; 617 618 619polys2 := { - u1**2 + 2*u1*x1 - u2**2 + 2*u2*x2 - 4*x2 + 4, 620 - u1**2 + 2*u1*x3 - u2**2 + 2*u2*x4, 6214*(x6 - 1), 622 - u1*x1*x5 - u1*x2*x6 + 2*u1*x6 + u2*x1*x6 - u2*x2*x5 + 2*u2*x5 - 2*x1*x6 + 2* 623x2*x5 - 4*x5, 624u1**3*x2 - 2*u1**3 - u1**2*u2*x1 + u1**2*x1*x4 + 2*u1**2*x1 - u1**2*x2*x3 + 2*u1 625**2*x3 + u1*u2**2*x2 - 2*u1*u2**2 - 2*u1*x1*x3 - 2*u1*x2*x4 + 4*u1*x4 - u2**3*x1 626 + u2**2*x1*x4 + 2*u2**2*x1 - u2**2*x2*x3 + 2*u2**2*x3 - 2*u2*x1*x4 + 2*u2*x2*x3 627 - 4*u2*x3}$ 628 629 630sol:=solve(polys2,{x1,x2,x3,x4,x6}); 631 632 633sol := {{x2=( - u1*x5 + u2 + 2)/2, 634x4=(u1*x5 + u2)/2, 635x1=(u1 + u2*x5 - 2*x5)/2, 636x3=(u1 - u2*x5)/2, 637x6=1}}$ 638 639sub(sol,con); 640 641 6420$ 643 644 645clear_ndg(); 646 647 648{}$ 649 clear(A,B,C,P,Q,R); 650 651 652 653% #################### 654% Desargue's theorem 655% #################### 656 657% A constructive proof. 658 659A:=Point(a1,a2); 660 661 662a := {a1,a2}$ 663 B:=Point(b1,b2); 664 665 666b := {b1,b2}$ 667 668C:=Point(c1,c2); 669 670 671c := {c1,c2}$ 672 R:=Point(d1,d2); 673 674 675r := {d1,d2}$ 676 677 678S:=choose_pl(par(R,pp_line(A,B)),u); 679 680 681s := {u, 682(a1*d2 - a2*d1 + a2*u - b1*d2 + b2*d1 - b2*u)/(a1 - b1)}$ 683 684T:=intersection_point(par(R,pp_line(A,C)),par(S,pp_line(B,C))); 685 686 687t := {(a1*u - b1*d1 + c1*d1 - c1*u)/(a1 - b1), 688(a1*d2 - a2*d1 + a2*u - b1*d2 + c2*d1 - c2*u)/(a1 - b1)}$ 689 690 691con:=concurrent(pp_line(A,R),pp_line(B,S),pp_line(C,T)); 692 693 694con := 0$ 695 696 697% Desargue's theorem as theorem of linear type. 698 699A:=Point(u1,u2); 700 701 702a := {u1,u2}$ 703 B:=Point(u3,u4); 704 705 706b := {u3,u4}$ 707 C:=Point(u5,u6); 708 709 710c := {u5,u6}$ 711 712R:=Point(u7,u8); 713 714 715r := {u7,u8}$ 716 S:=Point(u9,x1); 717 718 719s := {u9,x1}$ 720 T:=Point(x2,x3); 721 722 723t := {x2,x3}$ 724 725 726polys:={parallel(pp_line(R,S),pp_line(A,B)), 727 parallel(pp_line(S,T),pp_line(B,C)), 728 parallel(pp_line(R,T),pp_line(A,C))}; 729 730 731polys := { - u1*u8 + u1*x1 + u2*u7 - u2*u9 + u3*u8 - u3*x1 - u4*u7 + u4*u9, 732 - u3*x1 + u3*x3 + u4*u9 - u4*x2 + u5*x1 - u5*x3 - u6*u9 + u6*x2, 733 - u1*u8 + u1*x3 + u2*u7 - u2*x2 + u5*u8 - u5*x3 - u6*u7 + u6*x2}$ 734 735 736con:=concurrent(pp_line(A,R),pp_line(B,S),pp_line(C,T)); 737 738 739con := - u1*u3*u6*u8 + u1*u3*u6*x1 + u1*u3*u8*x3 - u1*u3*x1*x3 + u1*u4*u5*u8 - 740u1*u4*u5*x3 - u1*u4*u6*u9 + u1*u4*u6*x2 - u1*u4*u8*x2 + u1*u4*u9*x3 - u1*u5*u8* 741x1 + u1*u5*x1*x3 + u1*u6*u8*u9 - u1*u6*x1*x2 - u1*u8*u9*x3 + u1*u8*x1*x2 - u2*u3 742*u5*x1 + u2*u3*u5*x3 + u2*u3*u6*u7 - u2*u3*u6*x2 - u2*u3*u7*x3 + u2*u3*x1*x2 - 743u2*u4*u5*u7 + u2*u4*u5*u9 + u2*u4*u7*x2 - u2*u4*u9*x2 + u2*u5*u7*x1 - u2*u5*u9* 744x3 - u2*u6*u7*u9 + u2*u6*u9*x2 + u2*u7*u9*x3 - u2*u7*x1*x2 + u3*u5*u8*x1 - u3*u5 745*u8*x3 - u3*u6*u7*x1 + u3*u6*u8*x2 + u3*u7*x1*x3 - u3*u8*x1*x2 + u4*u5*u7*x3 - 746u4*u5*u8*u9 + u4*u6*u7*u9 - u4*u6*u7*x2 - u4*u7*u9*x3 + u4*u8*u9*x2 - u5*u7*x1* 747x3 + u5*u8*u9*x3 + u6*u7*x1*x2 - u6*u8*u9*x2$ 748 749 750sol:=solve(polys,{x1,x2,x3}); 751 752 753sol := {{x1=(u1*u8 - u2*u7 + u2*u9 - u3*u8 + u4*u7 - u4*u9)/(u1 - u3), 754x2=(u1*u9 - u3*u7 + u5*u7 - u5*u9)/(u1 - u3), 755x3=(u1*u8 - u2*u7 + u2*u9 - u3*u8 + u6*u7 - u6*u9)/(u1 - u3)}}$ 756 757sub(sol,con); 758 759 7600$ 761 762 763% The general theorem of Desargue. 764 765A:=Point(0,0); 766 767 768a := {0,0}$ 769 B:=Point(0,1); 770 771 772b := {0,1}$ 773 C:=Point(u5,u6); 774 775 776c := {u5,u6}$ 777 778R:=Point(u7,u8); 779 780 781r := {u7,u8}$ 782 S:=Point(u9,u1); 783 784 785s := {u9,u1}$ 786 T:=Point(u2,x1); 787 788 789t := {u2,x1}$ 790 791 792con1:=collinear(intersection_point(pp_line(R,S),pp_line(A,B)), 793 intersection_point(pp_line(S,T),pp_line(B,C)), 794 intersection_point(pp_line(R,T),pp_line(A,C))); 795 796 797con1 := (u5*( - u1**2*u2**2*u6*u7 + u1**2*u2*u5*u7*x1 + u1**2*u2*u6*u7**2 - u1** 7982*u5*u7**2*x1 + u1*u2**2*u6*u7*u8 + u1*u2**2*u6*u7 + u1*u2**2*u6*u8*u9 - u1*u2** 7992*u8*u9 - u1*u2*u5*u7*u8*x1 - u1*u2*u5*u7*x1 - u1*u2*u5*u8*u9*x1 + u1*u2*u5*u8* 800u9 - u1*u2*u6*u7**2*x1 - u1*u2*u6*u7**2 - 2*u1*u2*u6*u7*u8*u9 + u1*u2*u6*u7*u9* 801x1 - u1*u2*u6*u7*u9 + u1*u2*u7*u8*u9 + u1*u2*u7*u9*x1 + u1*u5*u7**2*x1**2 + u1* 802u5*u7**2*x1 + 2*u1*u5*u7*u8*u9*x1 - u1*u5*u7*u8*u9 - u1*u5*u7*u9*x1**2 + u1*u6* 803u7**2*u9 - u1*u7**2*u9*x1 - u2**2*u6*u7*u8 - u2**2*u6*u8**2*u9 + u2**2*u8**2*u9 804+ u2*u5*u7*u8*x1 + u2*u5*u8**2*u9*x1 - u2*u5*u8**2*u9 + u2*u6*u7**2*x1 + u2*u6* 805u7*u8*u9*x1 + 2*u2*u6*u7*u8*u9 - u2*u6*u7*u9*x1 + u2*u6*u8**2*u9**2 - u2*u6*u8* 806u9**2*x1 - 2*u2*u7*u8*u9*x1 - u2*u8**2*u9**2 + u2*u8*u9**2*x1 - u5*u7**2*x1**2 - 807 u5*u7*u8*u9*x1**2 + u5*u7*u9*x1**2 - u5*u8**2*u9**2*x1 + u5*u8**2*u9**2 + u5*u8 808*u9**2*x1**2 - u5*u8*u9**2*x1 - u6*u7**2*u9*x1 - u6*u7*u8*u9**2 + u6*u7*u9**2*x1 809 + u7**2*u9*x1**2 + u7*u8*u9**2*x1 - u7*u9**2*x1**2))/(u1*u2*u5*u6*u7 - u1*u2*u5 810*u6*u9 + u1*u5**2*u7*u8 - u1*u5**2*u7*x1 - u1*u5**2*u8*u9 + u1*u5**2*u9*x1 - u1* 811u5*u6*u7**2 + u1*u5*u6*u7*u9 + u2**2*u6**2*u7 - u2**2*u6**2*u9 - u2**2*u6*u7 + 812u2**2*u6*u9 + u2*u5*u6*u7*u8 - 2*u2*u5*u6*u7*x1 - u2*u5*u6*u8*u9 + 2*u2*u5*u6*u9 813*x1 - u2*u5*u7*u8 + u2*u5*u7*x1 + u2*u5*u8*u9 - u2*u5*u9*x1 - u2*u6**2*u7**2 + 814u2*u6**2*u9**2 + u2*u6*u7**2 - u2*u6*u9**2 - u5**2*u7*u8*x1 + u5**2*u7*x1**2 + 815u5**2*u8*u9*x1 - u5**2*u9*x1**2 + u5*u6*u7**2*x1 - u5*u6*u7*u8*u9 + u5*u6*u8*u9 816**2 - u5*u6*u9**2*x1 + u5*u7*u8*u9 - u5*u7*u9*x1 - u5*u8*u9**2 + u5*u9**2*x1 + 817u6**2*u7**2*u9 - u6**2*u7*u9**2 - u6*u7**2*u9 + u6*u7*u9**2)$ 818 819 820con2:=concurrent(pp_line(A,R),pp_line(B,S),pp_line(C,T)); 821 822 823con2 := u1*u2*u6*u7 - u1*u5*u7*x1 - u2*u6*u7 - u2*u6*u8*u9 + u2*u8*u9 + u5*u7*x1 824 + u5*u8*u9*x1 - u5*u8*u9 + u6*u7*u9 - u7*u9*x1$ 825 826 827sol:=solve(con2,x1); 828 829 830sol := {x1=(u1*u2*u6*u7 - u2*u6*u7 - u2*u6*u8*u9 + u2*u8*u9 - u5*u8*u9 + u6*u7* 831u9)/(u1*u5*u7 - u5*u7 - u5*u8*u9 + u7*u9)}$ 832 833sub(sol,con1); 834 835 8360$ 837 838 839clear_ndg(); 840 841 842{}$ 843 clear(A,B,C,R,S,T); 844 845 846 847% ################# 848% Brocard points 849% ################# 850 851A:=Point(0,0); 852 853 854a := {0,0}$ 855 B:=Point(1,0); 856 857 858b := {1,0}$ 859 C:=Point(u1,u2); 860 861 862c := {u1,u2}$ 863 864 865c1:=Circle(1,x1,x2,x3); 866 867 868c1 := {1,x1,x2,x3}$ 869 870c2:=Circle(1,x4,x5,x6); 871 872 873c2 := {1,x4,x5,x6}$ 874 875c3:=Circle(1,x7,x8,x9); 876 877 878c3 := {1,x7,x8,x9}$ 879 880 881polys:={ 882 cl_tangent(c1,pp_line(A,C)), 883 point_on_circle(A,c1), 884 point_on_circle(B,c1), 885 cl_tangent(c2,pp_line(A,B)), 886 point_on_circle(B,c2), 887 point_on_circle(C,c2), 888 cl_tangent(c3,pp_line(B,C)), 889 point_on_circle(A,c3), 890 point_on_circle(C,c3)}; 891 892 893polys := {u1**2*x1**2 - 4*u1**2*x3 + 2*u1*u2*x1*x2 + u2**2*x2**2 - 4*u2**2*x3, 894x3, 895x1 + x3 + 1, 896x4**2 - 4*x6, 897x4 + x6 + 1, 898u1**2 + u1*x4 + u2**2 + u2*x5 + x6, 899u1**2*x7**2 - 4*u1**2*x9 + 2*u1*u2*x7*x8 + 4*u1*u2*x8 - 2*u1*x7**2 + 8*u1*x9 - 4 900*u2**2*x7 + u2**2*x8**2 - 4*u2**2*x9 - 4*u2**2 - 2*u2*x7*x8 - 4*u2*x8 + x7**2 - 9014*x9, 902x9, 903u1**2 + u1*x7 + u2**2 + u2*x8 + x9}$ 904 905 906vars:={x1,x2,x3,x4,x5,x6,x7,x8,x9}; 907 908 909vars := {x1, 910x2, 911x3, 912x4, 913x5, 914x6, 915x7, 916x8, 917x9}$ 918 919sol:=solve(polys,vars); 920 921 922sol := {{x6=1, 923x8=( - u1**3 + u1**2 - u1*u2**2 - u2**2)/u2, 924x2=u1/u2, 925x1=-1, 926x3=0, 927x4=-2, 928x5=( - u1**2 + 2*u1 - u2**2 - 1)/u2, 929x7=u1**2 - 2*u1 + u2**2, 930x9=0}}$ 931 932 933P:=other_cc_point(B,sub(sol,c1),sub(sol,c2)); 934 935 936p := {(u1**3 - u1**2 + u1*u2**2 + u1 + u2**2)/(u1**4 - 2*u1**3 + 2*u1**2*u2**2 + 937 3*u1**2 - 2*u1*u2**2 - 2*u1 + u2**4 + 3*u2**2 + 1), 938(u2*(u1**2 - 2*u1 + u2**2 + 1))/(u1**4 - 2*u1**3 + 2*u1**2*u2**2 + 3*u1**2 - 2* 939u1*u2**2 - 2*u1 + u2**4 + 3*u2**2 + 1)}$ 940 941con:=point_on_circle(P,sub(sol,c3)); 942 943 944con := 0$ 945 946 947clear_ndg(); 948 949 950{}$ 951 clear A,B,C,c1,c2,c3; 952 953 954 955% ################## 956% Simson's theorem 957% ################## 958 959% A constructive proof 960 961 M:=Point(0,0); 962 963 964m := {0,0}$ 965 966 A:=choose_pc(M,r,u1); 967 968 969a := {(r*(u1**2 - 1))/(u1**2 + 1),(2*r*u1)/(u1**2 + 1)}$ 970 971 B:=choose_pc(M,r,u2); 972 973 974b := {(r*(u2**2 - 1))/(u2**2 + 1),(2*r*u2)/(u2**2 + 1)}$ 975 976 C:=choose_pc(M,r,u3); 977 978 979c := {(r*(u3**2 - 1))/(u3**2 + 1),(2*r*u3)/(u3**2 + 1)}$ 980 981 P:=choose_pc(M,r,u4); 982 983 984p := {(r*(u4**2 - 1))/(u4**2 + 1),(2*r*u4)/(u4**2 + 1)}$ 985 986 X:=pedalpoint(P,pp_line(A,B))$ 987 988 989 Y:=pedalpoint(P,pp_line(B,C))$ 990 991 992 Z:=pedalpoint(P,pp_line(A,C))$ 993 994 995 996 collinear(X,Y,Z); 997 998 9990$ 1000 1001 1002clear_ndg(); 1003 1004 1005{}$ 1006 clear(M,A,B,C,P,X,Y,Z); 1007 1008 1009 1010% Simson's theorem almost constructive 1011 1012clear_ndg(); 1013 1014 1015{}$ 1016 1017 1018 A:=Point(0,0); 1019 1020 1021a := {0,0}$ 1022 B:=Point(u1,u2); 1023 1024 1025b := {u1,u2}$ 1026 1027 C:=Point(u3,u4); 1028 1029 1030c := {u3,u4}$ 1031 P:=Point(u5,x1); 1032 1033 1034p := {u5,x1}$ 1035 1036 X:=pedalpoint(P,pp_line(A,B)); 1037 1038 1039x := {(u1*(u1*u5 + u2*x1))/(u1**2 + u2**2), 1040(u2*(u1*u5 + u2*x1))/(u1**2 + u2**2)}$ 1041 1042 Y:=pedalpoint(P,pp_line(B,C)); 1043 1044 1045y := {(u1**2*u5 - u1*u2*u4 + u1*u2*x1 - 2*u1*u3*u5 + u1*u4**2 - u1*u4*x1 + u2**2 1046*u3 - u2*u3*u4 - u2*u3*x1 + u3**2*u5 + u3*u4*x1)/(u1**2 - 2*u1*u3 + u2**2 - 2*u2 1047*u4 + u3**2 + u4**2), 1048(u1**2*u4 - u1*u2*u3 + u1*u2*u5 - u1*u3*u4 - u1*u4*u5 + u2**2*x1 + u2*u3**2 - u2 1049*u3*u5 - 2*u2*u4*x1 + u3*u4*u5 + u4**2*x1)/(u1**2 - 2*u1*u3 + u2**2 - 2*u2*u4 + 1050u3**2 + u4**2)}$ 1051 1052 Z:=pedalpoint(P,pp_line(A,C)); 1053 1054 1055z := {(u3*(u3*u5 + u4*x1))/(u3**2 + u4**2), 1056(u4*(u3*u5 + u4*x1))/(u3**2 + u4**2)}$ 1057 1058 1059 poly:=p4_circle(A,B,C,P); 1060 1061 1062poly := u1**2*u3*x1 - u1**2*u4*u5 - u1*u3**2*x1 - u1*u4**2*x1 + u1*u4*u5**2 + u1 1063*u4*x1**2 + u2**2*u3*x1 - u2**2*u4*u5 + u2*u3**2*u5 - u2*u3*u5**2 - u2*u3*x1**2 1064+ u2*u4**2*u5$ 1065 1066 1067 con:=collinear(X,Y,Z); 1068 1069 1070con := ( - u1**4*u3*u4**2*x1 + u1**4*u4**3*u5 + 2*u1**3*u2*u3**2*u4*x1 - 2*u1**3 1071*u2*u3*u4**2*u5 + u1**3*u3**2*u4**2*x1 + u1**3*u4**4*x1 - u1**3*u4**3*u5**2 - u1 1072**3*u4**3*x1**2 - u1**2*u2**2*u3**3*x1 + u1**2*u2**2*u3**2*u4*u5 - u1**2*u2**2* 1073u3*u4**2*x1 + u1**2*u2**2*u4**3*u5 - 2*u1**2*u2*u3**3*u4*x1 - u1**2*u2*u3**2*u4 1074**2*u5 - 2*u1**2*u2*u3*u4**3*x1 + 3*u1**2*u2*u3*u4**2*u5**2 + 3*u1**2*u2*u3*u4** 10752*x1**2 - u1**2*u2*u4**4*u5 + 2*u1*u2**3*u3**2*u4*x1 - 2*u1*u2**3*u3*u4**2*u5 + 1076u1*u2**2*u3**4*x1 + 2*u1*u2**2*u3**3*u4*u5 + u1*u2**2*u3**2*u4**2*x1 - 3*u1*u2** 10772*u3**2*u4*u5**2 - 3*u1*u2**2*u3**2*u4*x1**2 + 2*u1*u2**2*u3*u4**3*u5 - u2**4*u3 1078**3*x1 + u2**4*u3**2*u4*u5 - u2**3*u3**4*u5 + u2**3*u3**3*u5**2 + u2**3*u3**3*x1 1079**2 - u2**3*u3**2*u4**2*u5)/(u1**4*u3**2 + u1**4*u4**2 - 2*u1**3*u3**3 - 2*u1**3 1080*u3*u4**2 + 2*u1**2*u2**2*u3**2 + 2*u1**2*u2**2*u4**2 - 2*u1**2*u2*u3**2*u4 - 2* 1081u1**2*u2*u4**3 + u1**2*u3**4 + 2*u1**2*u3**2*u4**2 + u1**2*u4**4 - 2*u1*u2**2*u3 1082**3 - 2*u1*u2**2*u3*u4**2 + u2**4*u3**2 + u2**4*u4**2 - 2*u2**3*u3**2*u4 - 2*u2 1083**3*u4**3 + u2**2*u3**4 + 2*u2**2*u3**2*u4**2 + u2**2*u4**4)$ 1084 1085 1086 remainder(num con,poly); 1087 1088 10890$ 1090 1091 1092print_ndg(); 1093 1094 1095{u3**2 + u4**2, 1096u1**2 - 2*u1*u3 + u2**2 - 2*u2*u4 + u3**2 + u4**2, 1097u1**2 + u2**2}$ 1098 1099 1100% Equational proof, first version: 1101 1102M:=Point(0,0); 1103 1104 1105m := {0,0}$ 1106 A:=Point(0,1); 1107 1108 1109a := {0,1}$ 1110 1111B:=Point(u1,x1); 1112 1113 1114b := {u1,x1}$ 1115 C:=Point(u2,x2); 1116 1117 1118c := {u2,x2}$ 1119 P:=Point(u3,x3); 1120 1121 1122p := {u3,x3}$ 1123 1124 1125X:=varpoint(A,B,x4); 1126 1127 1128x := {u1*( - x4 + 1), - x1*x4 + x1 + x4}$ 1129 Y:=varpoint(B,C,x5); 1130 1131 1132y := {u1*x5 - u2*x5 + u2,x1*x5 - x2*x5 + x2}$ 1133 Z:=varpoint(A,C,x6); 1134 1135 1136z := {u2*( - x6 + 1), - x2*x6 + x2 + x6}$ 1137 1138 1139polys:={sqrdist(M,B)-1, sqrdist(M,C)-1, sqrdist(M,P)-1, 1140 orthogonal(pp_line(A,B),pp_line(P,X)), 1141 orthogonal(pp_line(A,C),pp_line(P,Z)), 1142 orthogonal(pp_line(B,C),pp_line(P,Y))}; 1143 1144 1145polys := {u1**2 + x1**2 - 1, 1146u2**2 + x2**2 - 1, 1147u3**2 + x3**2 - 1, 1148 - u1**2*x4 + u1**2 - u1*u3 - x1**2*x4 + x1**2 - x1*x3 + 2*x1*x4 - x1 + x3 - x4, 1149 - u2**2*x6 + u2**2 - u2*u3 - x2**2*x6 + x2**2 - x2*x3 + 2*x2*x6 - x2 + x3 - x6, 1150 - u1**2*x5 + 2*u1*u2*x5 - u1*u2 + u1*u3 - u2**2*x5 + u2**2 - u2*u3 - x1**2*x5 + 1151 2*x1*x2*x5 - x1*x2 + x1*x3 - x2**2*x5 + x2**2 - x2*x3}$ 1152 1153 1154con:=collinear(X,Y,Z); 1155 1156 1157con := u1*x2*x4*x5 - u1*x2*x4*x6 - u1*x2*x5*x6 + u1*x2*x6 - u1*x4*x5 + u1*x4*x6 1158+ u1*x5*x6 - u1*x6 - u2*x1*x4*x5 + u2*x1*x4*x6 + u2*x1*x5*x6 - u2*x1*x6 + u2*x4* 1159x5 - u2*x4*x6 - u2*x5*x6 + u2*x6$ 1160 1161 1162vars:={x4,x5,x6,x1,x2,x3}; 1163 1164 1165vars := {x4, 1166x5, 1167x6, 1168x1, 1169x2, 1170x3}$ 1171 1172setring(vars,{},lex); 1173 1174 1175{{x4,x5,x6,x1,x2,x3},{},lex,{1,1,1,1,1,1}}$ 1176 1177setideal(polys,polys); 1178 1179 1180{x1**2 + (u1**2 - 1), 1181x2**2 + (u2**2 - 1), 1182x3**2 + (u3**2 - 1), 1183 - x4*x1**2 + 2*x4*x1 - (u1**2 + 1)*x4 + x1**2 - x1*x3 - x1 + x3 + (u1**2 - u1* 1184u3), 1185 - x6*x2**2 + 2*x6*x2 - (u2**2 + 1)*x6 + x2**2 - x2*x3 - x2 + x3 + (u2**2 - u2* 1186u3), 1187 - x5*x1**2 + 2*x5*x1*x2 - x5*x2**2 - (u1**2 - 2*u1*u2 + u2**2)*x5 - x1*x2 + x1* 1188x3 + x2**2 - x2*x3 - (u1*u2 - u1*u3 - u2**2 + u2*u3)}$ 1189 1190con mod gbasis polys; 1191 1192 11930$ 1194 1195 1196% Second version: 1197 1198A:=Point(0,0); 1199 1200 1201a := {0,0}$ 1202 1203B:=Point(1,0); 1204 1205 1206b := {1,0}$ 1207 1208C:=Point(u1,u2); 1209 1210 1211c := {u1,u2}$ 1212 1213P:=Point(u3,x1); 1214 1215 1216p := {u3,x1}$ 1217 1218X:=Point(x2,0); 1219 1220 1221x := {x2,0}$ 1222 % => on the line AB 1223Y:=varpoint(B,C,x3); 1224 1225 1226y := { - u1*x3 + u1 + x3,u2*( - x3 + 1)}$ 1227 1228Z:=varpoint(A,C,x4); 1229 1230 1231z := {u1*( - x4 + 1),u2*( - x4 + 1)}$ 1232 1233 1234polys:={orthogonal(pp_line(A,C),pp_line(P,Z)), 1235 orthogonal(pp_line(B,C),pp_line(P,Y)), 1236 orthogonal(pp_line(A,B),pp_line(P,X)), 1237 p4_circle(A,B,C,P)}; 1238 1239 1240polys := { - u1**2*x4 + u1**2 - u1*u3 - u2**2*x4 + u2**2 - u2*x1, 1241 - u1**2*x3 + u1**2 - u1*u3 + 2*u1*x3 - u1 - u2**2*x3 + u2**2 - u2*x1 + u3 - x3, 1242 - u3 + x2, 1243 - u1**2*x1 + u1*x1 - u2**2*x1 + u2*u3**2 - u2*u3 + u2*x1**2}$ 1244 1245 1246con:=collinear(X,Y,Z); 1247 1248 1249con := u2*( - x2*x3 + x2*x4 - x3*x4 + x3)$ 1250 1251 1252vars:={x2,x3,x4,x1}; 1253 1254 1255vars := {x2,x3,x4,x1}$ 1256 1257setring(vars,{},lex); 1258 1259 1260{{x2,x3,x4,x1},{},lex,{1,1,1,1}}$ 1261 1262con mod interreduce polys; 1263 1264 12650$ 1266 1267 1268% The inverse theorem 1269 1270polys:={orthogonal(pp_line(A,C),pp_line(P,Z)), 1271 orthogonal(pp_line(B,C),pp_line(P,Y)), 1272 orthogonal(pp_line(A,B),pp_line(P,X)), 1273 collinear(X,Y,Z)}; 1274 1275 1276polys := { - u1**2*x4 + u1**2 - u1*u3 - u2**2*x4 + u2**2 - u2*x1, 1277 - u1**2*x3 + u1**2 - u1*u3 + 2*u1*x3 - u1 - u2**2*x3 + u2**2 - u2*x1 + u3 - x3, 1278 - u3 + x2, 1279u2*( - x2*x3 + x2*x4 - x3*x4 + x3)}$ 1280 1281 1282con:=p4_circle(A,B,C,P); 1283 1284 1285con := - u1**2*x1 + u1*x1 - u2**2*x1 + u2*u3**2 - u2*u3 + u2*x1**2$ 1286 1287 1288con mod interreduce polys; 1289 1290 12910$ 1292 1293 1294clear_ndg(); 1295 1296 1297{}$ 1298 clear(M,A,B,C,P,Y,Z); 1299 1300 1301 1302% ######################## 1303% The butterfly theorem 1304% ######################## 1305 1306% An equational proof with groebner factorizer and constraints. 1307 1308P:=Point(0,0); 1309 1310 1311p := {0,0}$ 1312 1313O:=Point(u1,0); 1314 1315 1316o := {u1,0}$ 1317 1318A:=Point(u2,u3); 1319 1320 1321a := {u2,u3}$ 1322 1323B:=Point(u4,x1); 1324 1325 1326b := {u4,x1}$ 1327 1328C:=Point(x2,x3); 1329 1330 1331c := {x2,x3}$ 1332 1333D:=Point(x4,x5); 1334 1335 1336d := {x4,x5}$ 1337 1338F:=Point(0,x6); 1339 1340 1341f := {0,x6}$ 1342 1343G:=Point(0,x7); 1344 1345 1346g := {0,x7}$ 1347 1348 1349polys:={sqrdist(O,B)-sqrdist(O,A), 1350 sqrdist(O,C)-sqrdist(O,A), 1351 sqrdist(O,D)-sqrdist(O,A), 1352 point_on_line(P,pp_line(A,C)), 1353 point_on_line(P,pp_line(B,D)), 1354 point_on_line(F,pp_line(A,D)), 1355 point_on_line(G,pp_line(B,C)) 1356}; 1357 1358 1359polys := {2*u1*u2 - 2*u1*u4 - u2**2 - u3**2 + u4**2 + x1**2, 13602*u1*u2 - 2*u1*x2 - u2**2 - u3**2 + x2**2 + x3**2, 13612*u1*u2 - 2*u1*x4 - u2**2 - u3**2 + x4**2 + x5**2, 1362 - u2*x3 + u3*x2, 1363 - u4*x5 + x1*x4, 1364 - u2*x5 + u2*x6 + u3*x4 - x4*x6, 1365 - u4*x3 + u4*x7 + x1*x2 - x2*x7}$ 1366 1367 1368con:=num sqrdist(P,midpoint(F,G)); 1369 1370 1371con := x6**2 + 2*x6*x7 + x7**2$ 1372 1373 1374vars:={x6,x7,x3,x5,x1,x2,x4}; 1375 1376 1377vars := {x6, 1378x7, 1379x3, 1380x5, 1381x1, 1382x2, 1383x4}$ 1384 1385setring(vars,{},lex); 1386 1387 1388{{x6,x7,x3,x5,x1,x2,x4},{},lex,{1,1,1,1,1,1,1}}$ 1389 1390 1391sol:=groebfactor(polys,{sqrdist(A,C),sqrdist(B,D)}); 1392 1393 1394sol := {{x1**2 + (2*u1*u2 - 2*u1*u4 - u2**2 - u3**2 + u4**2), 1395(u2**2 + u3**2)*x3 - (2*u1*u2*u3 - u2**2*u3 - u3**3), 1396(2*u1*u2 - 2*u1*u4 - u2**2 - u3**2)*x5 + (2*u1*u2 - u2**2 - u3**2)*x1, 1397(2*u1*u2 - 2*u1*u4 - u2**2 - u3**2)*x4 + (2*u1*u2*u4 - u2**2*u4 - u3**2*u4), 1398(u2**2 + u3**2)*x2 - (2*u1*u2**2 - u2**3 - u2*u3**2), 1399(2*u1*u2**2 - u2**3 - u2**2*u4 - u2*u3**2 - u3**2*u4)*x7 - (2*u1*u2**2 - u2**3 - 1400 u2*u3**2)*x1 + (2*u1*u2*u3*u4 - u2**2*u3*u4 - u3**3*u4), 1401(2*u1*u2**2 - u2**3 - u2**2*u4 - u2*u3**2 - u3**2*u4)*x6 + (2*u1*u2**2 - u2**3 - 1402 u2*u3**2)*x1 - (2*u1*u2*u3*u4 - u2**2*u3*u4 - u3**3*u4)}}$ 1403 1404 1405for each u in sol collect con mod u; 1406 1407 1408{0}$ 1409 1410 1411% A constructive proof 1412 1413on gcd; 1414 1415 1416 1417O:=Point(0,0); 1418 1419 1420o := {0,0}$ 1421 1422A:=Point(1,0); 1423 1424 1425a := {1,0}$ 1426 1427B:=choose_pc(O,1,u1); 1428 1429 1430b := {(u1**2 - 1)/(u1**2 + 1),(2*u1)/(u1**2 + 1)}$ 1431 1432C:=choose_pc(O,1,u2); 1433 1434 1435c := {(u2**2 - 1)/(u2**2 + 1),(2*u2)/(u2**2 + 1)}$ 1436 1437D:=choose_pc(O,1,u3); 1438 1439 1440d := {(u3**2 - 1)/(u3**2 + 1),(2*u3)/(u3**2 + 1)}$ 1441 1442P:=intersection_point(pp_line(A,C),pp_line(B,D)); 1443 1444 1445p := {(u1*u2 - u1*u3 + u2*u3 - 1)/(u1*u2 - u1*u3 + u2*u3 + 1), 1446(2*u2)/(u1*u2 - u1*u3 + u2*u3 + 1)}$ 1447 1448 1449h:=lot(P,pp_line(O,P)); 1450 1451 1452h := {( - u1*u2 + u1*u3 - u2*u3 + 1)/(u1*u2 - u1*u3 + u2*u3 + 1), 1453( - 2*u2)/(u1*u2 - u1*u3 + u2*u3 + 1), 1454(u1**2*u2**2 - 2*u1**2*u2*u3 + u1**2*u3**2 + 2*u1*u2**2*u3 - 2*u1*u2*u3**2 - 2* 1455u1*u2 + 2*u1*u3 + u2**2*u3**2 + 4*u2**2 - 2*u2*u3 + 1)/(u1**2*u2**2 - 2*u1**2*u2 1456*u3 + u1**2*u3**2 + 2*u1*u2**2*u3 - 2*u1*u2*u3**2 + 2*u1*u2 - 2*u1*u3 + u2**2*u3 1457**2 + 2*u2*u3 + 1)}$ 1458 1459 1460F:=intersection_point(h,pp_line(A,D)); 1461 1462 1463f := {(u1**2*u2**2 - 2*u1**2*u2*u3 + u1**2*u3**2 - 2*u1*u2 + 2*u1*u3 - u2**2*u3 1464**2 + 4*u2**2 - 4*u2*u3 + 1)/(u1**2*u2**2 - 2*u1**2*u2*u3 + u1**2*u3**2 - u2**2* 1465u3**2 - 2*u2*u3 - 1), 1466(2*u3*(u1*u2 - u1*u3 - 2*u2**2 + u2*u3 - 1))/(u1**2*u2**2 - 2*u1**2*u2*u3 + u1** 14672*u3**2 - u2**2*u3**2 - 2*u2*u3 - 1)}$ 1468 1469G:=intersection_point(h,pp_line(B,C)); 1470 1471 1472g := {(u1**2*u2**2 - 2*u1**2*u2*u3 + u1**2*u3**2 - 2*u1*u2 + 2*u1*u3 - u2**2*u3 1473**2 - 4*u2**2 + 4*u2*u3 + 1)/(u1**2*u2**2 - 2*u1**2*u2*u3 + u1**2*u3**2 - u2**2* 1474u3**2 - 2*u2*u3 - 1), 1475(2*(2*u1*u2**2 - 3*u1*u2*u3 + u1*u3**2 - u2*u3**2 - 2*u2 + u3))/(u1**2*u2**2 - 2 1476*u1**2*u2*u3 + u1**2*u3**2 - u2**2*u3**2 - 2*u2*u3 - 1)}$ 1477 1478 1479con:=sqrdist(P,midpoint(F,G)); 1480 1481 1482con := 0$ 1483 1484 1485off gcd; 1486 1487 1488clear_ndg(); 1489 1490 1491{}$ 1492 clear(O,A,B,C,D,P,h,F,G); 1493 1494 1495 1496% ################################ 1497% Tangency of Feuerbach's circle 1498% ################################ 1499 1500A:=Point(0,0); 1501 1502 1503a := {0,0}$ 1504 B:=Point(2,0); 1505 1506 1507b := {2,0}$ 1508 C:=Point(u1,u2); 1509 1510 1511c := {u1,u2}$ 1512 1513M:=intersection_point(mp(A,B),mp(B,C)); 1514 1515 1516m := {1,(u1**2 - 2*u1 + u2**2)/(2*u2)}$ 1517 1518H:=intersection_point(altitude(A,B,C),altitude(B,C,A)); 1519 1520 1521h := {u1,(u1*( - u1 + 2))/u2}$ 1522 1523N:=midpoint(M,H); 1524 1525 1526n := {(u1 + 1)/2,( - u1**2 + 2*u1 + u2**2)/(4*u2)}$ 1527 1528c1:=c1_circle(N,sqrdist(N,midpoint(A,B))); 1529 1530 1531c1 := {1, - (u1 + 1),(u1**2 - 2*u1 - u2**2)/(2*u2),u1}$ 1532 1533 % Feuerbach's circle 1534 1535P:=Point(x1,x2); 1536 1537 1538p := {x1,x2}$ 1539 % => x2 is the radius of the inscribed circle. 1540 1541polys:={point_on_bisector(P,A,B,C), point_on_bisector(P,B,C,A)}; 1542 1543 1544polys := {2*( - 2*u1*x1*x2 + 4*u1*x2 + u2*x1**2 - 4*u2*x1 - u2*x2**2 + 4*u2 + 4* 1545x1*x2 - 8*x2), 15462*( - u1**3*x2 + u1**2*u2*x1 - u1**2*u2 + u1**2*x1*x2 + 2*u1**2*x2 - u1*u2**2*x2 1547 - u1*u2*x1**2 + u1*u2*x2**2 - 2*u1*x1*x2 + u2**3*x1 - u2**3 - u2**2*x1*x2 + 2* 1548u2**2*x2 + u2*x1**2 - u2*x2**2)}$ 1549 1550 1551con:=cc_tangent(c1_circle(P,x2^2),c1); 1552 1553 1554con := (4*( - u1**3*x1*x2 + u1**3*x2 + u1**2*u2*x1**2 - 2*u1**2*u2*x1 - u1**2*u2 1555*x2**2 + u1**2*u2 + u1**2*x1**2*x2 + u1**2*x1*x2 - 2*u1**2*x2 + u1*u2**2*x1*x2 - 1556 u1*u2**2*x2 - 2*u1*u2*x1**3 + 4*u1*u2*x1**2 - 2*u1*u2*x1 + 2*u1*u2*x2**2 - 2*u1 1557*x1**2*x2 + 2*u1*x1*x2 - u2**2*x1**2*x2 + u2**2*x1*x2 + u2*x1**4 - 2*u2*x1**3 + 1558u2*x1**2 - u2*x2**2))/u2$ 1559 1560 1561vars:={x1,x2}; 1562 1563 1564vars := {x1,x2}$ 1565 1566setring(vars,{},lex); 1567 1568 1569{{x1,x2},{},lex,{1,1}}$ 1570 1571setideal(polys,polys); 1572 1573 1574{(2*u2)*x1**2 - (4*u1 - 8)*x1*x2 - (8*u2)*x1 - (2*u2)*x2**2 + (8*u1 - 16)*x2 + 8 1575*u2, 1576 - (2*u1*u2 - 2*u2)*x1**2 + (2*u1**2 - 4*u1 - 2*u2**2)*x1*x2 + (2*u1**2*u2 + 2* 1577u2**3)*x1 + (2*u1*u2 - 2*u2)*x2**2 - (2*u1**3 - 4*u1**2 + 2*u1*u2**2 - 4*u2**2)* 1578x2 - (2*u1**2*u2 + 2*u2**3)}$ 1579 1580num con mod gbasis polys; 1581 1582 15830$ 1584 1585 1586% Now let P be the incenter of the triangle ABH 1587 1588polys1:={point_on_bisector(P,A,B,H), point_on_bisector(P,B,H,A)}; 1589 1590 1591polys1 := {(2*( - u1**2*x1**2 + 4*u1**2*x1 + u1**2*x2**2 - 4*u1**2 - 2*u1*u2*x1* 1592x2 + 4*u1*u2*x2 + 2*u1*x1**2 - 8*u1*x1 - 2*u1*x2**2 + 8*u1 + 4*u2*x1*x2 - 8*u2* 1593x2))/u2, 1594(2*u1*( - u1**5*x1 + u1**5 - u1**4*u2*x2 + 6*u1**4*x1 - 6*u1**4 - u1**3*u2**2*x1 1595 + u1**3*u2**2 - u1**3*u2*x1*x2 + 6*u1**3*u2*x2 - 12*u1**3*x1 + 12*u1**3 - u1**2 1596*u2**3*x2 + u1**2*u2**2*x1**2 + 2*u1**2*u2**2*x1 - u1**2*u2**2*x2**2 - 2*u1**2* 1597u2**2 + 4*u1**2*u2*x1*x2 - 12*u1**2*u2*x2 + 8*u1**2*x1 - 8*u1**2 + u1*u2**3*x1* 1598x2 + 2*u1*u2**3*x2 - 3*u1*u2**2*x1**2 + 3*u1*u2**2*x2**2 - 4*u1*u2*x1*x2 + 8*u1* 1599u2*x2 - 2*u2**3*x1*x2 + 2*u2**2*x1**2 - 2*u2**2*x2**2))/u2**3}$ 1600 1601 1602con1:=cc_tangent(c1_circle(P,x2^2),c1); 1603 1604 1605con1 := (4*( - u1**3*x1*x2 + u1**3*x2 + u1**2*u2*x1**2 - 2*u1**2*u2*x1 - u1**2* 1606u2*x2**2 + u1**2*u2 + u1**2*x1**2*x2 + u1**2*x1*x2 - 2*u1**2*x2 + u1*u2**2*x1*x2 1607 - u1*u2**2*x2 - 2*u1*u2*x1**3 + 4*u1*u2*x1**2 - 2*u1*u2*x1 + 2*u1*u2*x2**2 - 2* 1608u1*x1**2*x2 + 2*u1*x1*x2 - u2**2*x1**2*x2 + u2**2*x1*x2 + u2*x1**4 - 2*u2*x1**3 1609+ u2*x1**2 - u2*x2**2))/u2$ 1610 1611setideal(polys1,polys1); 1612 1613 1614{ - (2*u1**2 - 4*u1)*x1**2 - (4*u1*u2 - 8*u2)*x1*x2 + (8*u1**2 - 16*u1)*x1 + (2* 1615u1**2 - 4*u1)*x2**2 + (8*u1*u2 - 16*u2)*x2 - (8*u1**2 - 16*u1), 1616(2*u1**3*u2**2 - 6*u1**2*u2**2 + 4*u1*u2**2)*x1**2 - (2*u1**4*u2 - 8*u1**3*u2 - 16172*u1**2*u2**3 + 8*u1**2*u2 + 4*u1*u2**3)*x1*x2 - (2*u1**6 - 12*u1**5 + 2*u1**4* 1618u2**2 + 24*u1**4 - 4*u1**3*u2**2 - 16*u1**3)*x1 - (2*u1**3*u2**2 - 6*u1**2*u2**2 1619 + 4*u1*u2**2)*x2**2 - (2*u1**5*u2 - 12*u1**4*u2 + 2*u1**3*u2**3 + 24*u1**3*u2 - 1620 4*u1**2*u2**3 - 16*u1**2*u2)*x2 + (2*u1**6 - 12*u1**5 + 2*u1**4*u2**2 + 24*u1** 16214 - 4*u1**3*u2**2 - 16*u1**3)}$ 1622 1623num con1 mod gbasis polys1; 1624 1625 16260$ 1627 1628 1629clear_ndg(); 1630 1631 1632{}$ 1633 clear A,B,C,P,M,N,H,c1; 1634 1635 1636 1637% ############################# 1638% Solutions to the exercises 1639% ############################# 1640 1641% 1) 1642 1643A:=Point(0,0); 1644 1645 1646a := {0,0}$ 1647 B:=Point(1,0); 1648 1649 1650b := {1,0}$ 1651 C:=Point(1,1); 1652 1653 1654c := {1,1}$ 1655 D:=Point(0,1); 1656 1657 1658d := {0,1}$ 1659 1660P:=Point(x1,x2); 1661 1662 1663p := {x1,x2}$ 1664 Q:=Point(x3,1); 1665 1666 1667q := {x3,1}$ 1668 1669 1670polys:={point_on_line(P,par(C,pp_line(B,D))), 1671 sqrdist(B,D)-sqrdist(B,P), 1672 point_on_line(Q,pp_line(B,P))}; 1673 1674 1675polys := {x1 + x2 - 2, 1676 - x1**2 + 2*x1 - x2**2 + 1, 1677 - x1 + x2*x3 - x2 + 1}$ 1678 1679 1680con:=sqrdist(D,P)-sqrdist(D,Q); 1681 1682 1683con := x1**2 + x2**2 - 2*x2 - x3**2 + 1$ 1684 1685 1686setring({x1,x2,x3},{},lex); 1687 1688 1689{{x1,x2,x3},{},lex,{1,1,1}}$ 1690 1691setideal(polys,polys); 1692 1693 1694{x1 + x2 - 2, 1695 - x1**2 + 2*x1 - x2**2 + 1, 1696 - x1 + x2*x3 - x2 + 1}$ 1697 1698con mod gbasis polys; 1699 1700 17010$ 1702 1703 1704clear_ndg(); 1705 1706 1707{}$ 1708 clear(A,B,C,D,P,Q); 1709 1710 1711 1712% 2) 1713 1714A:=Point(u1,0); 1715 1716 1717a := {u1,0}$ 1718 B:=Point(u2,0); 1719 1720 1721b := {u2,0}$ 1722 C:=Point(0,u3); 1723 1724 1725c := {0,u3}$ 1726 1727Q:=Point(0,0); 1728 1729 1730q := {0,0}$ 1731 % the pedal point on AB 1732R:=pedalpoint(B,pp_line(A,C)); 1733 1734 1735r := {(u1*(u1*u2 + u3**2))/(u1**2 + u3**2), 1736(u1*u3*(u1 - u2))/(u1**2 + u3**2)}$ 1737 1738P:=pedalpoint(A,pp_line(B,C)); 1739 1740 1741p := {(u2*(u1*u2 + u3**2))/(u2**2 + u3**2), 1742(u2*u3*( - u1 + u2))/(u2**2 + u3**2)}$ 1743 1744 1745con1:=point_on_bisector(C,P,Q,R); 1746 1747 1748con1 := 0$ 1749 1750con2:=angle_sum(p3_angle(P,Q,C),p3_angle(R,Q,C)); 1751 1752 1753con2 := 0$ 1754 1755 1756clear_ndg(); 1757 1758 1759{}$ 1760 clear(A,B,C,P,Q,R); 1761 1762 1763 1764% 3) 1765 1766A:=Point(u1,0); 1767 1768 1769a := {u1,0}$ 1770 B:=Point(u2,0); 1771 1772 1773b := {u2,0}$ 1774 C:=Point(0,u3); 1775 1776 1777c := {0,u3}$ 1778 1779P:=pedalpoint(A,pp_line(B,C)); 1780 1781 1782p := {(u2*(u1*u2 + u3**2))/(u2**2 + u3**2), 1783(u2*u3*( - u1 + u2))/(u2**2 + u3**2)}$ 1784 1785Q:=pedalpoint(B,pp_line(A,C)); 1786 1787 1788q := {(u1*(u1*u2 + u3**2))/(u1**2 + u3**2), 1789(u1*u3*(u1 - u2))/(u1**2 + u3**2)}$ 1790 1791R:=pedalpoint(C,pp_line(A,B)); 1792 1793 1794r := {0,0}$ 1795 1796 1797P1:=pedalpoint(P,pp_line(A,B)); 1798 1799 1800p1 := {(u2*(u1*u2 + u3**2))/(u2**2 + u3**2),0}$ 1801 1802P2:=pedalpoint(P,pp_line(A,C)); 1803 1804 1805p2 := {(u1*(u1**2*u2**2 + 2*u1*u2*u3**2 + u3**4))/(u1**2*u2**2 + u1**2*u3**2 + 1806u2**2*u3**2 + u3**4), 1807(u3**3*(u1**2 - 2*u1*u2 + u2**2))/(u1**2*u2**2 + u1**2*u3**2 + u2**2*u3**2 + u3 1808**4)}$ 1809 1810Q1:=pedalpoint(Q,pp_line(A,B)); 1811 1812 1813q1 := {(u1*(u1*u2 + u3**2))/(u1**2 + u3**2),0}$ 1814 1815Q2:=pedalpoint(Q,pp_line(B,C)); 1816 1817 1818q2 := {(u2*(u1**2*u2**2 + 2*u1*u2*u3**2 + u3**4))/(u1**2*u2**2 + u1**2*u3**2 + 1819u2**2*u3**2 + u3**4), 1820(u3**3*(u1**2 - 2*u1*u2 + u2**2))/(u1**2*u2**2 + u1**2*u3**2 + u2**2*u3**2 + u3 1821**4)}$ 1822 1823R1:=pedalpoint(R,pp_line(A,C)); 1824 1825 1826r1 := {(u1*u3**2)/(u1**2 + u3**2),(u1**2*u3)/(u1**2 + u3**2)}$ 1827 1828R2:=pedalpoint(R,pp_line(B,C)); 1829 1830 1831r2 := {(u2*u3**2)/(u2**2 + u3**2),(u2**2*u3)/(u2**2 + u3**2)}$ 1832 1833 1834con:=for each X in {Q2,R1,R2} collect p4_circle(P1,P2,Q1,X); 1835 1836 1837con := {0,0,0}$ 1838 1839 1840clear_ndg(); 1841 1842 1843{}$ 1844 clear(O,A,B,C,P,Q,R,P1,P2,Q1,Q2,R1,R2); 1845 1846 1847 1848% 4) 1849 1850A:=Point(u1,0); 1851 1852 1853a := {u1,0}$ 1854 B:=Point(u2,0); 1855 1856 1857b := {u2,0}$ 1858 C:=Point(0,u3); 1859 1860 1861c := {0,u3}$ 1862 1863 % => Pedalpoint from C is (0,0) 1864M:=intersection_point(mp(A,B),mp(B,C)); 1865 1866 1867m := {(u1 + u2)/2,(u1*u2 + u3**2)/(2*u3)}$ 1868 1869 1870% Prove (2*h_c*R = a*b)^2 1871 1872con:=4*u3^2*sqrdist(M,A)-sqrdist(C,B)*sqrdist(A,C); 1873 1874 1875con := 0$ 1876 1877 1878clear_ndg(); 1879 1880 1881{}$ 1882 clear(A,B,C,M); 1883 1884 1885 1886% 5. A solution of constructive type. 1887 1888on gcd; 1889 1890 1891O:=Point(0,u1); 1892 1893 1894o := {0,u1}$ 1895 A:=Point(0,0); 1896 1897 1898a := {0,0}$ 1899 % hence k has radius u1. 1900B:=Point(u2,0); 1901 1902 1903b := {u2,0}$ 1904 1905M:=midpoint(A,B); 1906 1907 1908m := {u2/2,0}$ 1909 1910D:=choose_pc(O,u1,u3); 1911 1912 1913d := {(u1*(u3**2 - 1))/(u3**2 + 1),(u1*(u3**2 + 2*u3 + 1))/(u3**2 + 1)}$ 1914 1915k:=c1_circle(O,u1^2); 1916 1917 1918k := {1,0, - 2*u1,0}$ 1919 1920C:=other_cl_point(D,k,pp_line(M,D)); 1921 1922 1923c := {(u1*u2*(4*u1*u3**2 + 8*u1*u3 + 4*u1 - u2*u3**2 + u2))/(8*u1**2*u3**2 + 16* 1924u1**2*u3 + 8*u1**2 - 4*u1*u2*u3**2 + 4*u1*u2 + u2**2*u3**2 + u2**2), 1925(u1*u2**2*(u3**2 + 2*u3 + 1))/(8*u1**2*u3**2 + 16*u1**2*u3 + 8*u1**2 - 4*u1*u2* 1926u3**2 + 4*u1*u2 + u2**2*u3**2 + u2**2)}$ 1927 1928Eh:=other_cl_point(D,k,pp_line(B,D)); 1929 1930 1931eh := {(u1*u2*(2*u1*u3**2 + 4*u1*u3 + 2*u1 - u2*u3**2 + u2))/(2*u1**2*u3**2 + 4* 1932u1**2*u3 + 2*u1**2 - 2*u1*u2*u3**2 + 2*u1*u2 + u2**2*u3**2 + u2**2), 1933(u1*u2**2*(u3**2 + 2*u3 + 1))/(2*u1**2*u3**2 + 4*u1**2*u3 + 2*u1**2 - 2*u1*u2*u3 1934**2 + 2*u1*u2 + u2**2*u3**2 + u2**2)}$ 1935 1936F:=other_cl_point(C,k,pp_line(B,C)); 1937 1938 1939f := {(u1*u2*( - 2*u1*u3**2 - 4*u1*u3 - 2*u1 + u2*u3**2 - u2))/(2*u1**2*u3**2 + 19404*u1**2*u3 + 2*u1**2 - 2*u1*u2*u3**2 + 2*u1*u2 + u2**2*u3**2 + u2**2), 1941(u1*u2**2*(u3**2 + 2*u3 + 1))/(2*u1**2*u3**2 + 4*u1**2*u3 + 2*u1**2 - 2*u1*u2*u3 1942**2 + 2*u1*u2 + u2**2*u3**2 + u2**2)}$ 1943 1944 1945con:=parallel(pp_line(A,B),pp_line(Eh,F)); 1946 1947 1948con := 0$ 1949 1950 1951off gcd; 1952 1953 1954clear_ndg(); 1955 1956 1957{}$ 1958 clear(O,A,B,C,D,Eh,F,M,k); 1959 1960 1961 1962% 6) 1963 1964Z:=Point(0,0); 1965 1966 1967z := {0,0}$ 1968 X:=Point(0,1); 1969 1970 1971x := {0,1}$ 1972 Y:=Point(0,-1); 1973 1974 1975y := {0,-1}$ 1976 1977B:=Point(u1,0); 1978 1979 1980b := {u1,0}$ 1981 C:=Point(u2,0); 1982 1983 1984c := {u2,0}$ 1985 P:=Point(0,u3); 1986 1987 1988p := {0,u3}$ 1989 1990M:=Point(x1,x2); 1991 1992 1993m := {x1,x2}$ 1994 N:=Point(x3,x4); 1995 1996 1997n := {x3,x4}$ 1998 1999A:=Point(x5,0); 2000 2001 2002a := {x5,0}$ 2003 D:=Point(x6,0); 2004 2005 2006d := {x6,0}$ 2007 2008 2009polys:={p4_circle(X,Y,B,N), p4_circle(X,Y,C,M), 2010 p4_circle(X,Y,B,D), p4_circle(X,Y,C,A), 2011 collinear(B,P,N), collinear(C,P,M)}; 2012 2013 2014polys := {2*( - u1**2*x3 + u1*x3**2 + u1*x4**2 - u1 + x3), 20152*( - u2**2*x1 + u2*x1**2 + u2*x2**2 - u2 + x1), 20162*( - u1**2*x6 + u1*x6**2 - u1 + x6), 20172*( - u2**2*x5 + u2*x5**2 - u2 + x5), 2018u1*u3 - u1*x4 - u3*x3, 2019u2*u3 - u2*x2 - u3*x1}$ 2020 2021 2022con:=concurrent(pp_line(A,M),pp_line(D,N),pp_line(X,Y)); 2023 2024 2025con := 2*( - x1*x4*x6 + x2*x3*x5 - x2*x5*x6 + x4*x5*x6)$ 2026 2027 2028vars:={x1,x2,x3,x4,x5,x6}; 2029 2030 2031vars := {x1, 2032x2, 2033x3, 2034x4, 2035x5, 2036x6}$ 2037 2038setring(vars,{},lex); 2039 2040 2041{{x1,x2,x3,x4,x5,x6},{},lex,{1,1,1,1,1,1}}$ 2042 2043res:=groebfactor(polys,{x5-u2,x1-u2,x6-u1,x3-u1}); 2044 2045 2046res := {{u1*x6 + 1, 2047(u2**2 + u3**2)*x2 - (u2**2*u3 + u3), 2048(u2**2 + u3**2)*x1 - (u2*u3**2 - u2), 2049(u1**2 + u3**2)*x4 - (u1**2*u3 + u3), 2050(u1**2 + u3**2)*x3 - (u1*u3**2 - u1), 2051u2*x5 + 1}}$ 2052 2053 % constraints A\neq C, M\neq C, D\neq B, N\neq B 2054for each u in res collect con mod u; 2055 2056 2057{0}$ 2058 2059 2060clear_ndg(); 2061 2062 2063{}$ 2064 clear(Z,X,Y,B,C,P,M,N,A,D); 2065 2066 2067 2068% 7) 2069 2070M:=Point(0,0); 2071 2072 2073m := {0,0}$ 2074 2075A:=Point(0,u1); 2076 2077 2078a := {0,u1}$ 2079 B:=Point(-1,0); 2080 2081 2082b := {-1,0}$ 2083 C:=Point(1,0); 2084 2085 2086c := {1,0}$ 2087 2088Eh:=varpoint(A,B,x1); 2089 2090 2091eh := {x1 - 1,u1*x1}$ 2092 F:=varpoint(A,C,x2); 2093 2094 2095f := { - x2 + 1,u1*x2}$ 2096 2097O:=intersection_point(pp_line(A,M),lot(B,pp_line(A,B))); 2098 2099 2100o := {0,( - 1)/u1}$ 2101 2102Q:=intersection_point(pp_line(Eh,F),pp_line(B,C)); 2103 2104 2105q := {( - 2*x1*x2 + x1 + x2)/(x1 - x2),0}$ 2106 2107 2108con1:=num orthogonal(pp_line(O,Q),pp_line(Eh,Q)); 2109 2110 2111con1 := 2*x1*(x1**2*x2 - x1**2 + x1*x2**2 - 2*x1*x2 + x1 - x2**2 + x2)$ 2112 2113con2:=num sqrdist(Q,midpoint(Eh,F)); 2114 2115 2116con2 := u1**2*x1**4 - 2*u1**2*x1**2*x2**2 + u1**2*x2**4 + x1**4 + 4*x1**3*x2 - 4 2117*x1**3 + 6*x1**2*x2**2 - 12*x1**2*x2 + 4*x1**2 + 4*x1*x2**3 - 12*x1*x2**2 + 8*x1 2118*x2 + x2**4 - 4*x2**3 + 4*x2**2$ 2119 2120 2121vars:={x1,x2}; 2122 2123 2124vars := {x1,x2}$ 2125 2126setring(vars,{},lex); 2127 2128 2129{{x1,x2},{},lex,{1,1}}$ 2130 2131p1:=groebfactor({con1},{x1-1,x2-1,x1,x2}); 2132 2133 2134p1 := {{x1 + x2}}$ 2135 2136p2:=groebfactor({con2},{x1-1,x2-1,x1,x2}); 2137 2138 2139p2 := {{x1 + x2}, 2140{(u1**2 + 1)*x1**2 - (2*u1**2 - 2)*x1*x2 - 4*x1 + (u1**2 + 1)*x2**2 - 4*x2 + 4}} 2141$ 2142 2143 % constraint A,C\neq Eh, B,C\neq F 2144 2145for each u in p1 collect con2 mod u; 2146 2147 2148{0}$ 2149 2150for each u in p2 collect con1 mod u; 2151 2152 2153{0, 2154(2*(5*u1**4*x1*x2**3 - 8*u1**4*x1*x2**2 + 3*u1**4*x1*x2 - 3*u1**4*x2**4 + 4*u1** 21554*x2**3 - u1**4*x2**2 - 10*u1**2*x1*x2**3 + 32*u1**2*x1*x2**2 - 30*u1**2*x1*x2 + 2156 8*u1**2*x1 - 2*u1**2*x2**4 + 12*u1**2*x2**3 - 26*u1**2*x2**2 + 20*u1**2*x2 - 4* 2157u1**2 + x1*x2**3 - 8*x1*x2**2 + 15*x1*x2 - 8*x1 + x2**4 - 8*x2**3 + 23*x2**2 - 215828*x2 + 12))/(u1**4 + 2*u1**2 + 1)}$ 2159 2160 2161% Note that the second component of p2 has no relevant *real* roots, 2162% since it factors as u1^2 * (x1 - x2)^2 + (x1 + x2 -2)^2 : 2163 2164u1^2 * (x1 - x2)^2 + (x1 + x2 -2)^2 mod second p2; 2165 2166 21670$ 2168 2169 2170clear_ndg(); 2171 2172 2173{}$ 2174 clear(M,A,B,C,O,Eh,F,Q); 2175 2176 2177 2178% 8) 2179 2180on gcd; 2181 2182 2183 2184A:=Point(u1,0); 2185 2186 2187a := {u1,0}$ 2188 B:=Point(u2,0); 2189 2190 2191b := {u2,0}$ 2192 l1:=pp_line(A,B); 2193 2194 2195l1 := {0,u1 - u2,0}$ 2196 2197M:=Point(0,u3); 2198 2199 2200m := {0,u3}$ 2201 % the incenter, hence u3 = incircle radius 2202 2203C:=intersection_point(symline(l1,pp_line(A,M)), 2204 symline(l1,pp_line(B,M))); 2205 2206 2207c := {(u3**2*(u1 + u2))/(u1*u2 + u3**2), 2208(2*u1*u2*u3)/(u1*u2 + u3**2)}$ 2209 2210 2211N:=intersection_point(mp(A,B),mp(B,C)); 2212 2213 2214n := {(u1 + u2)/2, 2215(u1**2*u2**2 - u1**2*u3**2 + 4*u1*u2*u3**2 - u2**2*u3**2 + u3**4)/(4*u3*(u1*u2 + 2216 u3**2))}$ 2217 % the outcenter 2218 2219sqr_rad:=sqrdist(A,N); 2220 2221 2222sqr_rad := (u1**4*u2**4 + 2*u1**4*u2**2*u3**2 + u1**4*u3**4 + 2*u1**2*u2**4*u3** 22232 + 4*u1**2*u2**2*u3**4 + 2*u1**2*u3**6 + u2**4*u3**4 + 2*u2**2*u3**6 + u3**8)/( 222416*u3**2*(u1**2*u2**2 + 2*u1*u2*u3**2 + u3**4))$ 2225 % the outcircle sqradius. 2226 2227(sqr_rad-sqrdist(M,N))^2-4*u3^2*sqr_rad; 2228 2229 22300$ 2231 2232 2233off gcd; 2234 2235 2236clear_ndg(); 2237 2238 2239{}$ 2240 clear A,B,C,M,N,l1,sqr_rad; 2241 2242 2243 2244% 9) 2245 2246on gcd; 2247 2248 2249 2250A:=Point(0,0); 2251 2252 2253a := {0,0}$ 2254 B:=Point(1,0); 2255 2256 2257b := {1,0}$ 2258 M:=Point(u1,0); 2259 2260 2261m := {u1,0}$ 2262 2263C:=Point(u1,u1); 2264 2265 2266c := {u1,u1}$ 2267 F:=Point(u1,1-u1); 2268 2269 2270f := {u1, - u1 + 1}$ 2271 2272 2273c1:=red_hom_coords p3_circle(A,M,C); 2274 2275 2276c1 := {1, - u1, - u1,0}$ 2277 2278c2:=red_hom_coords p3_circle(B,M,F); 2279 2280 2281c2 := {-1,u1 + 1, - u1 + 1, - u1}$ 2282 2283N:=other_cc_point(M,c1,c2); 2284 2285 2286n := {u1**2/(2*u1**2 - 2*u1 + 1),(u1*( - u1 + 1))/(2*u1**2 - 2*u1 + 1)}$ 2287 2288 2289point_on_line(N,pp_line(A,F)); 2290 2291 22920$ 2293 2294point_on_line(N,pp_line(B,C)); 2295 2296 22970$ 2298 2299 2300l1:=red_hom_coords pp_line(M,N); 2301 2302 2303l1 := {-1,2*u1 - 1,u1}$ 2304 2305l2:=sub(u1=u2,l1); 2306 2307 2308l2 := {-1,2*u2 - 1,u2}$ 2309 2310 2311intersection_point(l1,l2); 2312 2313 2314{1/2,( - 1)/2}$ 2315 % = (1/2,-1/2) 2316 2317off gcd; 2318 2319 2320clear_ndg(); 2321 2322 2323{}$ 2324 clear A,B,C,F,M,N,c1,c2,l1,l2; 2325 2326 2327 2328% #################### 2329% Some more examples 2330% #################### 2331 2332% Origin: D. Wang at 2333% http://cosmos.imag.fr/ATINF/Dongming.Wang/geother.html 2334% -------------------------- 2335% Given triangle ABC, H orthocenter, O circumcenter, A1 circumcenter 2336% of BHC, B1 circumcenter of AHC. 2337% 2338% Claim: OH, AA1, BB1 are concurrent. 2339% -------------------------- 2340 2341A:=Point(u1,0); 2342 2343 2344a := {u1,0}$ 2345 B:=Point(u2,0); 2346 2347 2348b := {u2,0}$ 2349 C:=Point(0,u3); 2350 2351 2352c := {0,u3}$ 2353 2354H:=intersection_point(altitude(C,A,B),altitude(A,B,C)); 2355 2356 2357h := {0,( - u1*u2)/u3}$ 2358 2359O:=circle_center(p3_circle(A,B,C)); 2360 2361 2362o := {(u1 + u2)/2,(u1*u2 + u3**2)/(2*u3)}$ 2363 2364A1:=circle_center(p3_circle(H,B,C)); 2365 2366 2367a1 := {( - u1 + u2)/2,( - u1*u2 + u3**2)/(2*u3)}$ 2368 2369B1:=circle_center(p3_circle(H,A,C)); 2370 2371 2372b1 := {(u1 - u2)/2,( - u1*u2 + u3**2)/(2*u3)}$ 2373 2374 2375con:=concurrent(pp_line(O,H),pp_line(A,A1),pp_line(B,B1)); 2376 2377 2378con := 0$ 2379 2380 2381end; 2382 23834: 4: 4: 4: 4: 4: 4: 4: 4: 2384 2385Time for test: 9680 ms, plus GC time: 880 ms 2386 23875: 5: 2388Quitting 2389Thu Jan 28 23:38:39 MET 1999 2390