Example 3 

 

 

Image 

 

Triangle rectangular in (a, b) 

(x,y) circumcenter, ie.

H:
       x^2+y^2-(x-e)^2-y^2=0
       x^2+y^2-(x-a)^2-(y-b)^2=0
 

       a(a-e)+b^2=0

Now we claim circumcenter lies on the horizontal side, say,

T
: y=0 

 

 

> with(Groebner):H:=Basis({x^2+y^2-(x-e)^2-y^2,x^2+y^2-(x-a)^2-(y-b)^2, a*(a-e)+b^2 },tdeg(x,y,e,a,b));
NormalForm(y, H, tdeg(x,y,e,a,b));
 

 

[`+`(`-`(`*`(`^`(a, 2))), `*`(a, `*`(e)), `-`(`*`(`^`(b, 2)))), `+`(`*`(2, `*`(x, `*`(a))), `-`(`*`(`^`(a, 2))), `*`(2, `*`(y, `*`(b))), `-`(`*`(`^`(b, 2)))), `+`(`*`(2, `*`(x, `*`(e))), `-`(`*`(`^`(e...
[`+`(`-`(`*`(`^`(a, 2))), `*`(a, `*`(e)), `-`(`*`(`^`(b, 2)))), `+`(`*`(2, `*`(x, `*`(a))), `-`(`*`(`^`(a, 2))), `*`(2, `*`(y, `*`(b))), `-`(`*`(`^`(b, 2)))), `+`(`*`(2, `*`(x, `*`(e))), `-`(`*`(`^`(e...
y (4.1.1)
 

>
 

 

So the theorem is not true. Let us see when this happens, negation of (H ==> T) yields (H & not T). 

 

 

> HH:=Basis({x^2+y^2-(x-e)^2-y^2,x^2+y^2-(x-a)^2-(y-b)^2, a*(a-e)+b^2, y*t-1 },plex(x,y,t,e,a,b));
 

[`+`(`*`(`^`(a, 2), `*`(b)), `*`(`^`(b, 3))), `*`(e, `*`(b)), `+`(`-`(`*`(`^`(a, 2))), `*`(a, `*`(e)), `-`(`*`(`^`(b, 2)))), `+`(`*`(y, `*`(t)), `-`(1)), `+`(`-`(`*`(y, `*`(a, `*`(b)))), `*`(x, `*`(`^...
[`+`(`*`(`^`(a, 2), `*`(b)), `*`(`^`(b, 3))), `*`(e, `*`(b)), `+`(`-`(`*`(`^`(a, 2))), `*`(a, `*`(e)), `-`(`*`(`^`(b, 2)))), `+`(`*`(y, `*`(t)), `-`(1)), `+`(`-`(`*`(y, `*`(a, `*`(b)))), `*`(x, `*`(`^...
(4.1.2)
 

>
 

 

In particular, if theorem is false implies 

 

eb=0 

a^2b+b^3=0 

a^2-ae+b^2=0 

 

 

Thus the negation of one of these yields a true statement: 

 

> HHH:=Basis({x^2+y^2-(x-e)^2-y^2,x^2+y^2-(x-a)^2-(y-b)^2, a*(a-e)+b^2, e*b*t-1 },tdeg(x,y,t,e,a,b));
NormalForm(y, HHH, tdeg(x,y,e,a,b));
 

 

[y, `+`(`*`(2, `*`(x)), `-`(e)), `+`(`-`(`*`(`^`(a, 2))), `*`(a, `*`(e)), `-`(`*`(`^`(b, 2)))), `+`(`*`(e, `*`(b, `*`(t))), `-`(1)), `+`(`*`(t, `*`(`^`(a, 2), `*`(b))), `*`(t, `*`(`^`(b, 3))), `-`(a))...
0 (4.1.3)
 

> HHHH:=Basis({x^2+y^2-(x-e)^2-y^2,x^2+y^2-(x-a)^2-(y-b)^2, a*(a-e)+b^2, (a^2*b+b^3)*t-1 },tdeg(x,y,t,e,a,b));
NormalForm(y, HHHH, tdeg(x,y,e,a,b));
 

 

[y, `+`(`*`(2, `*`(x)), `-`(e)), `+`(`-`(`*`(`^`(a, 2))), `*`(a, `*`(e)), `-`(`*`(`^`(b, 2)))), `+`(`*`(t, `*`(`^`(a, 2), `*`(b))), `*`(t, `*`(`^`(b, 3))), `-`(1)), `+`(`*`(t, `*`(e, `*`(`^`(b, 3)))),...
0 (4.1.4)
 

> H_5:=Basis({x^2+y^2-(x-e)^2-y^2,x^2+y^2-(x-a)^2-(y-b)^2, a*(a-e)+b^2, (-a^2+a*e-b^2)*t-1 },tdeg(x,y,t,e,a,b));
NormalForm(y, H_5, tdeg(x,y,e,a,b));
 

 

[1]
0 (4.1.5)
 

>