円の方程式

方針：「距離が $r$」を「距離の 2 乗が $r^2$」に言いかえ、2 乗しても同値であることを確かめる。
段 1（距離を式で書く）。2 点の距離の公式から $CP=\sqrt{(x-p)^2+(y-q)^2}$ である。$P$ が円の上にあるとは $CP=r$ のことである。
段 2（2 乗する）。$CP=r$ なら、両辺を 2 乗して $CP^2=r^2$ である。逆に $CP^2=r^2$ なら $(CP-r)(CP+r)=0$ で、$CP\ge0$、$r>0$ から $CP+r>0$ なので $CP-r=0$、つまり $CP=r$ である。
段 3（まとめる）。$CP^2=(x-p)^2+(y-q)^2$ なので、$CP=r$ と $(x-p)^2+(y-q)^2=r^2$ は同値である。$\square$

方針：平方完成して「2 乗の和 $=$ 定数」の形にし、右辺の符号で場合を分ける。
段 1（平方完成）。$x^2+lx=\left(x+\dfrac l2\right)^2-\dfrac{l^2}4$、$y^2+my=\left(y+\dfrac m2\right)^2-\dfrac{m^2}4$ なので、方程式は
$$ \left(x+\frac l2\right)^2+\left(y+\frac m2\right)^2=\frac{l^2+m^2-4n}4 $$
と同値である。右辺を $k$ とおく。
段 2（$k>0$）。$k=\left(\dfrac{\sqrt{l^2+m^2-4n}}2\right)^2$ と書けるので、thm-ceq-standard により、これは中心 $\left(-\dfrac l2,-\dfrac m2\right)$、半径 $\dfrac{\sqrt{l^2+m^2-4n}}2$ の円である。
段 3（$k=0$）。実数の 2 乗は $0$ 以上なので、2 乗の和が $0$ になるのは両方が $0$ のとき、つまり $x=-\dfrac l2$ かつ $y=-\dfrac m2$ のときだけである。
段 4（$k<0$）。左辺はいつも $0$ 以上なので、負の数 $k$ に等しくなることはない。$\square$

方針：十分性は $A$ で割って thm-ceq-general に戻す。必要性は、円の中心を原点に移したうえで、円の上の特別な点を代入して係数を 1 つずつ決める。左辺を $G(x,y)$ と書く。
段 1（十分性）。$B=0$、$A=C$ なら、$(A,B,C)\ne(0,0,0)$ から $A\ne0$ である。両辺を $A$ で割ると $x^2+y^2+\frac DAx+\frac EAy+\frac FA=0$ で、thm-ceq-general の量は
$$ \Bigl(\frac DA\Bigr)^2+\Bigl(\frac EA\Bigr)^2-\frac{4F}A=\frac{D^2+E^2-4AF}{A^2} $$
である。$A^2>0$ なので、これが正であることと $D^2+E^2-4AF>0$ は同値である。よって thm-ceq-general の 1 から円を表す。
段 2（必要性：中心を原点に移す）。逆に、$G=0$ を満たす点全体が中心 $(p,q)$、半径 $r>0$ の円 $K$ だとする。$x=p+u$、$y=q+v$ とおいて $G(p+u,q+v)$ を展開すると、$A(p+u)^2=Au^2+2Apu+Ap^2$、$B(p+u)(q+v)=Buv+Bqu+Bpv+Bpq$、$C(q+v)^2=Cv^2+\cdots$ となり、2 次の項は $Au^2+Buv+Cv^2$ のまま変わらない。そこで
$$ H(u,v):=G(p+u,q+v)=Au^2+Buv+Cv^2+D'u+E'v+F' $$
と書ける（$D'$、$E'$、$F'$ はある実数）。$(x,y)$ が $K$ の上にあることは $u^2+v^2=r^2$ と同じなので、$u^2+v^2=r^2$ を満たすどの $(u,v)$ でも $H(u,v)=0$ である。
段 3（$u$ 軸上の 2 点）。$(u,v)=(r,0)$、$(-r,0)$ を代入すると
$$ Ar^2+D'r+F'=0,\qquad Ar^2-D'r+F'=0 $$
である。引くと $2D'r=0$ で、$r>0$ から $D'=0$ である。すると $F'=-Ar^2$ である。
段 4（$v$ 軸上の 2 点）。同じく $(0,r)$、$(0,-r)$ を代入すると $E'=0$、$F'=-Cr^2$ である。段 3 と合わせて $-Ar^2=-Cr^2$ で、$r^2>0$ から $A=C$ である。
段 5（斜めの点）。$\left(\frac r{\sqrt2},\frac r{\sqrt2}\right)$ も $u^2+v^2=r^2$ を満たすので、代入して
$$ A\cdot\frac{r^2}2+B\cdot\frac{r^2}2+C\cdot\frac{r^2}2+F'=0 $$
である。$A=C$、$F'=-Ar^2$ を使うと左辺は $\frac{Br^2}2$ になるので、$B=0$ である。
段 6（元に戻す）。以上で $H(u,v)=A(u^2+v^2-r^2)$ で、$(A,B,C)\ne(0,0,0)$ と $B=0$、$A=C$ から $A\ne0$ である。$u=x-p$、$v=y-q$ に戻すと
$$ G(x,y)=A\bigl((x-p)^2+(y-q)^2-r^2\bigr) $$
である。展開すると $D=-2Ap$、$E=-2Aq$、$F=A(p^2+q^2-r^2)$ なので
$$ D^2+E^2-4AF=4A^2(p^2+q^2)-4A^2(p^2+q^2-r^2)=4A^2r^2>0 $$
である。$\square$

方針：$\Delta$ が「一直線上にあるか」を表すことを先に示し、次に連立方程式を解く。$s_i=x_i^2+y_i^2$ とおく。
段 1（$\Delta$ と一直線）。$\overrightarrow{P_1P_2}=(a,b)$、$\overrightarrow{P_1P_3}=(c,d)$ とおくと $\Delta=ad-bc$ で、$P_1\ne P_2$ から $(a,b)\ne(0,0)$ である。3 点が一直線上にあるのは、$(c,d)=t(a,b)$ となる実数 $t$ があるときである。そうなら $ad-bc=a\cdot tb-b\cdot ta=0$ である。逆に $ad-bc=0$ とする。$a\ne0$ なら $t=\frac ca$ とおくと $d=\frac{bc}a=tb$ である。$a=0$ なら $b\ne0$ で、$-bc=0$ から $c=0$、$t=\frac db$ とおけば $(c,d)=t(a,b)$ である。よって $\Delta=0$ と「一直線上にある」は同値である。
段 2（連立方程式を作る）。円が 3 点を通ることは、$l$、$m$、$n$ が
$$ x_il+y_im+n=-s_i\qquad(i=1,2,3) $$
を満たすことである。2 番目と 3 番目の式から 1 番目の式を引くと、$n$ が消えて
$$ al+bm=-(s_2-s_1),\qquad cl+dm=-(s_3-s_1) $$
となる。逆にこの 2 式と 1 番目の式が成り立てば、元の 3 式が成り立つ。
段 3（$\Delta\ne0$ なら解はただ 1 つ）。右辺を $e$、$f$ と書く。第 1 式を $d$ 倍して第 2 式の $b$ 倍を引くと $(ad-bc)l=de-bf$、第 2 式を $a$ 倍して第 1 式の $c$ 倍を引くと $(ad-bc)m=af-ce$ である。$\Delta=ad-bc\ne0$ なので、$l=\frac{de-bf}\Delta$、$m=\frac{af-ce}\Delta$ と決まり、実際に 2 式を満たす（代入して確かめられる）。すると 1 番目の式から $n=-s_1-x_1l-y_1m$ も決まる。
段 4（それが円であること）。こうして得た方程式を満たす点には、相異なる 3 点が含まれる。thm-ceq-general の 2 と 3 では満たす点が 1 個以下なので、1 の場合であり、円である。3 点を通る円はどれも一般形に書けて、その係数は段 3 のただ 1 つの解に等しいので、円はちょうど 1 つである。
段 5（$\Delta=0$ のとき）。段 1 から 3 点は 1 本の直線の上にある。直線と円の共有点は 2 個以下なので（円と直線の位置関係 の定理「円と直線の位置関係」）、3 点を通る円はない。$\square$

$(x-x_1)(x-x_2)=x^2-(x_1+x_2)x+x_1x_2=\left(x-\frac{x_1+x_2}2\right)^2-\left(\frac{x_1-x_2}2\right)^2$ である（右辺を展開すると定数項が $\frac{(x_1+x_2)^2-(x_1-x_2)^2}4=x_1x_2$ になる）。$y$ も同じなので、方程式は
$$ \left(x-\frac{x_1+x_2}2\right)^2+\left(y-\frac{y_1+y_2}2\right)^2=\frac{(x_1-x_2)^2+(y_1-y_2)^2}4=\Bigl(\frac{AB}2\Bigr)^2 $$
と同値である。$A\ne B$ から $AB>0$ なので、thm-ceq-standard によりこれは中点を中心、半径 $\frac{AB}2$ の円である。$\square$

prf-ceq-general の段 1 により、すべての $(x,y)$ で $f(x,y)=\left(x+\frac l2\right)^2+\left(y+\frac m2\right)^2-r^2$ である（$r^2=\frac{l^2+m^2-4n}4$）。$C=\left(-\frac l2,-\frac m2\right)$ なので、右辺の 2 乗の和に $P$ を入れたものは $CP^2$ である。$\square$