Ptolemyの定理

方針：対角線 $BD$ の上に、$\angle BAE=\angle CAD$ となる点 $E$ をとる。すると相似な三角形が 2 組でき、$BD$ を $BE$ と $ED$ に分けて、それぞれの長さが辺の積で表せる。
段 1（点 $E$ をとる）。四角形は凸なので、対角線 $AC$ は $\angle BAD$ の内部を通る。したがって $\angle CAD<\angle BAD$ である。辺 $AB$ から $\angle BAD$ の内側に向かって $\angle CAD$ だけ回した半直線は、$\angle BAD$ の内部にあるので、線分 $BD$ と $B$、$D$ 以外の点で交わる。その点を $E$ とする。作り方から
$$ \angle BAE=\angle CAD $$
である。
段 2（1 組目の相似）。三角形 $ABE$ と三角形 $ACD$ を比べる。段 1 より $\angle BAE=\angle CAD$ である。また $\angle ABE=\angle ABD$ と $\angle ACD$ は、どちらも弧 $AD$（$B$、$C$ を含まない側）に対する円周角なので等しい。2 つの角が等しいので $\triangle ABE\sim\triangle ACD$ である。対応する辺の比から
$$ \frac{AB}{AC}=\frac{BE}{CD},\qquad\text{つまり}\qquad AB\cdot CD=AC\cdot BE $$
である。
段 3（2 組目の相似）。三角形 $ADE$ と三角形 $ACB$ を比べる。$E$ は $\angle BAD$ の内部にあり、$C$ も $\angle BAD$ の内部にあるので
$$ \angle DAE=\angle BAD-\angle BAE=\angle BAD-\angle CAD=\angle BAC $$
である（2 つ目の等号で段 1 を使った）。また $\angle ADE=\angle ADB$ と $\angle ACB$ は、どちらも弧 $AB$（$C$、$D$ を含まない側）に対する円周角なので等しい。よって $\triangle ADE\sim\triangle ACB$ であり
$$ \frac{AD}{AC}=\frac{DE}{CB},\qquad\text{つまり}\qquad AD\cdot BC=AC\cdot DE $$
である。
段 4（足す）。$E$ は線分 $BD$ の上にあるので $BE+ED=BD$ である。段 2 と段 3 の式を足して
$$ AB\cdot CD+AD\cdot BC=AC\cdot BE+AC\cdot DE=AC\,(BE+ED)=AC\cdot BD $$
を得る。$\square$

方針：4 点 $A$、$B$、$P$、$C$ はこの順に円周上に並ぶので、四角形 $ABPC$ に thm-ptol-main を使う。
正三角形の 1 辺の長さを $s$ とする。四角形 $ABPC$ の対角線は $AP$ と $BC$、向かい合う辺の組は $AB$ と $PC$、$BP$ と $CA$ である。thm-ptol-main により
$$ AP\cdot BC=AB\cdot PC+BP\cdot CA $$
である。$BC=AB=CA=s$ を代入すると $s\cdot PA=s\cdot PC+s\cdot PB$ で、両辺を $s>0$ で割って $PA=PB+PC$ を得る。$\square$

方針：両辺を展開する。
段 1（左辺）。$(a-b)(c-d)=ac-ad-bc+bd$、$(a-d)(b-c)=ab-ac-bd+cd$ である。足すと $ac$ と $-ac$、$bd$ と $-bd$ が消えて
$$ (a-b)(c-d)+(a-d)(b-c)=ab-ad-bc+cd $$
である。
段 2（右辺）。$(a-c)(b-d)=ab-ad-bc+cd$ である。段 1 と一致する。$\square$

方針：両辺は $0$ 以上なので、2 乗して比べる。複素数 $w$ について $|w|^2=w\bar w$、$\overline{w_1+w_2}=\bar w_1+\bar w_2$、$|w_1w_2|=|w_1|\,|w_2|$、$|\bar w|=|w|$ を使う（複素数平面と図形）。
段 1（左辺の 2 乗）。$w=u\bar v$ とおくと $\bar uv=\bar w$ なので
$$ |u+v|^2=(u+v)(\bar u+\bar v)=u\bar u+v\bar v+u\bar v+\bar uv=|u|^2+|v|^2+(w+\bar w) $$
である。$w=x+yi$（$x,y$ は実数）と書くと $w+\bar w=2x$ なので、$|u+v|^2=|u|^2+|v|^2+2x$ である。
段 2（右辺の 2 乗）。$|w|=|u|\,|\bar v|=|u|\,|v|$ なので、$(|u|+|v|)^2=|u|^2+|v|^2+2|w|$ である。
段 3（比べる）。$x\le|x|=\sqrt{x^2}\le\sqrt{x^2+y^2}=|w|$ なので、段 1 と段 2 から $|u+v|^2\le(|u|+|v|)^2$ である。$|u+v|$ と $|u|+|v|$ はどちらも $0$ 以上なので、$|u+v|\le|u|+|v|$ を得る。
段 4（等号）。等号が成り立つのは $x=\sqrt{x^2+y^2}$ のとき、つまり $y=0$ かつ $x\ge0$ のとき、すなわち $w=u\bar v$ が $0$ 以上の実数のときに限る。$u,v\ne0$ なら $w\ne0$ であり、$\dfrac uv=\dfrac{u\bar v}{v\bar v}=\dfrac w{|v|^2}$ なので、これは $\dfrac uv$ が正の実数であることと同じである。$\square$

方針：lem-ptol-identity の両辺の絶対値をとり、右辺に三角不等式（lem-ptol-triangle）を使う。
段 1（恒等式の絶対値）。4 点を複素数 $a,b,c,d$ で表す。lem-ptol-identity の両辺の絶対値をとると
$$ |(a-c)(b-d)|=|(a-b)(c-d)+(a-d)(b-c)| $$
である。
段 2（三角不等式）。複素数 $u,v$ について $|u+v|\le|u|+|v|$ である（lem-ptol-triangle）。$u=(a-b)(c-d)$、$v=(a-d)(b-c)$ として段 1 の右辺に使うと
$$ |(a-c)(b-d)|\le|(a-b)(c-d)|+|(a-d)(b-c)| $$
である。
段 3（距離に直す）。積の絶対値は絶対値の積なので、$|(a-c)(b-d)|=|a-c|\,|b-d|=AC\cdot BD$ である。同じように $|(a-b)(c-d)|=AB\cdot CD$、$|(a-d)(b-c)|=AD\cdot BC$ である。段 2 に代入して $AC\cdot BD\le AB\cdot CD+AD\cdot BC$ を得る。$\square$

方針：prf-ptol-ineq で等号が成り立つのは、$u$ と $v$ の比 $\dfrac uv$ が正の実数のときである。$\dfrac uv$ の偏角を計算すると $180^\circ-(\angle A+\angle C)$ になる。
段 1（三角不等式の等号）。$u=(a-b)(c-d)$、$v=(a-d)(b-c)$ とする。4 点は異なるので $u,v\ne0$ である。prf-ptol-ineq の段 1 と段 3 は等式なので、Ptolemy の不等式で等号が成り立つのは、段 2 の $|u+v|\le|u|+|v|$ で等号が成り立つときに限る。lem-ptol-triangle により、それは $\dfrac uv$ が正の実数のときに限る。
段 2（$\dfrac uv$ を角で表す）。四角形 $ABCD$ の頂点が反時計回りに並ぶように座標を選ぶ（時計回りなら、裏返した図形で考えればよい。距離は変わらない）。凸四角形の頂点 $A$ では、ベクトル $\overrightarrow{AB}$ を反時計回りに $\angle A$ だけ回すと $\overrightarrow{AD}$ の向きになる。複素数の掛け算は回転と拡大なので（複素数の掛け算は回転と拡大）
$$ \frac{d-a}{b-a}=\frac{AD}{AB}\,(\cos A+i\sin A) $$
である。同じように頂点 $C$ では $\overrightarrow{CD}$ を反時計回りに $\angle C$ だけ回すと $\overrightarrow{CB}$ の向きになるので、$\dfrac{b-c}{d-c}=\dfrac{CB}{CD}(\cos C+i\sin C)$ である。
段 3（比を計算する）。$(a-b)(c-d)=(b-a)(d-c)$、$(a-d)(b-c)=-(d-a)(b-c)$ なので
$$ \frac uv=-\frac{b-a}{d-a}\cdot\frac{d-c}{b-c}=-\frac{AB}{AD}\cdot\frac{CD}{CB}\,\bigl(\cos(-A)+i\sin(-A)\bigr)\bigl(\cos(-C)+i\sin(-C)\bigr) $$
である（段 2 の式の逆数をとった）。$-1=\cos180^\circ+i\sin180^\circ$ と、偏角の足し算の規則から
$$ \frac uv=\frac{AB\cdot CD}{AD\cdot CB}\Bigl(\cos\bigl(180^\circ-(A+C)\bigr)+i\sin\bigl(180^\circ-(A+C)\bigr)\Bigr) $$
である。
段 4（結論）。凸四角形なので $0^\circ< A+C<360^\circ$ で、$-180^\circ<180^\circ-(A+C)<180^\circ$ である。この範囲で $\dfrac uv$ が正の実数になるのは $180^\circ-(A+C)=0^\circ$、つまり $\angle A+\angle C=180^\circ$ のときに限る。段 1 と合わせて、等号が成り立つことは $\angle A+\angle C=180^\circ$ と同値である。凸四角形で対角の和が $180^\circ$ であることは、円に内接することと同値である（証明は 円に内接する四角形 にある。この記事では証明しない）。$\square$

方針：両辺の 2 乗を、内積の性質 $|\boldsymbol v|^2=\boldsymbol v\cdot\boldsymbol v$ と分配法則で展開して比べる（ベクトルの内積（高校数学））。
段 1（左辺の 2 乗）。
$$ |\boldsymbol x^*-\boldsymbol y^*|^2=\frac{\boldsymbol x\cdot\boldsymbol x}{|\boldsymbol x|^4}-2\,\frac{\boldsymbol x\cdot\boldsymbol y}{|\boldsymbol x|^2|\boldsymbol y|^2}+\frac{\boldsymbol y\cdot\boldsymbol y}{|\boldsymbol y|^4}=\frac1{|\boldsymbol x|^2}-\frac{2\,\boldsymbol x\cdot\boldsymbol y}{|\boldsymbol x|^2|\boldsymbol y|^2}+\frac1{|\boldsymbol y|^2} $$
である。2 つ目の等号で $\boldsymbol x\cdot\boldsymbol x=|\boldsymbol x|^2$、$\boldsymbol y\cdot\boldsymbol y=|\boldsymbol y|^2$ を使った。
段 2（通分）。分母を $|\boldsymbol x|^2|\boldsymbol y|^2$ にそろえると
$$ |\boldsymbol x^*-\boldsymbol y^*|^2=\frac{|\boldsymbol y|^2-2\,\boldsymbol x\cdot\boldsymbol y+|\boldsymbol x|^2}{|\boldsymbol x|^2|\boldsymbol y|^2}=\frac{|\boldsymbol x-\boldsymbol y|^2}{|\boldsymbol x|^2|\boldsymbol y|^2} $$
である。最後の等号は $|\boldsymbol x-\boldsymbol y|^2=|\boldsymbol x|^2-2\,\boldsymbol x\cdot\boldsymbol y+|\boldsymbol y|^2$ による。
段 3（平方根）。両辺は $0$ 以上なので、正の平方根をとって主張を得る。$\square$

方針：$D$ を原点にとり、$A$、$B$、$C$ を反転した 3 点に三角不等式を使う。反転で距離がどう変わるかは lem-ptol-inversion で分かる。
段 1（特別な場合）。$D$ が $A$、$B$、$C$ のどれかと一致する場合を先に片づける。$D=A$ なら左辺は $AC\cdot BA$、右辺は $AB\cdot CA+0$ で等しい。$D=C$ なら左辺は $AC\cdot BC$、右辺は $0+AC\cdot BC$ で等しい。$D=B$ なら左辺は $0$ で、右辺は $0$ 以上である。以下、$D$ は $A$、$B$、$C$ のどれとも異なるとする。
段 2（反転）。$D$ を原点とし、$A$、$B$、$C$ の位置ベクトルを $\boldsymbol a$、$\boldsymbol b$、$\boldsymbol c$ とする。どれも $\vec0$ でないので、反転した点 $\boldsymbol a^*$、$\boldsymbol b^*$、$\boldsymbol c^*$ が定まる。3 点 $\boldsymbol a^*$、$\boldsymbol b^*$、$\boldsymbol c^*$ に三角不等式を使うと
$$ |\boldsymbol a^*-\boldsymbol c^*|\le|\boldsymbol a^*-\boldsymbol b^*|+|\boldsymbol b^*-\boldsymbol c^*| $$
である。
段 3（距離に戻す）。lem-ptol-inversion により、段 2 の式は
$$ \frac{|\boldsymbol a-\boldsymbol c|}{|\boldsymbol a||\boldsymbol c|}\le\frac{|\boldsymbol a-\boldsymbol b|}{|\boldsymbol a||\boldsymbol b|}+\frac{|\boldsymbol b-\boldsymbol c|}{|\boldsymbol b||\boldsymbol c|} $$
となる。両辺に正の数 $|\boldsymbol a||\boldsymbol b||\boldsymbol c|$ を掛けると
$$ |\boldsymbol a-\boldsymbol c|\,|\boldsymbol b|\le|\boldsymbol a-\boldsymbol b|\,|\boldsymbol c|+|\boldsymbol b-\boldsymbol c|\,|\boldsymbol a| $$
である。$D$ が原点なので $|\boldsymbol a-\boldsymbol c|=AC$、$|\boldsymbol b|=BD$、$|\boldsymbol a-\boldsymbol b|=AB$、$|\boldsymbol c|=CD$、$|\boldsymbol b-\boldsymbol c|=BC$、$|\boldsymbol a|=AD$ であり、$AC\cdot BD\le AB\cdot CD+BC\cdot AD$ を得る。$\square$

方針：$C$ と $F$ を直線 $BE$ について折り返した点 $C'$、$F'$ をとると、三角形 $ABC'$ と $DEF'$ が正三角形になる。cor-ptol-equilateral で $AG+GB=GC'$、$DH+HE=HF'$ となり、左辺は折れ線 $C'GHF'$ の長さになる。
段 1（正三角形 $BCD$、$EFA$）。三角形 $BCD$ は $BC=CD$、$\angle BCD=60^\circ$ の二等辺三角形なので、底角も $\dfrac{180^\circ-60^\circ}2=60^\circ$ で、正三角形である。よって $BD=BC=AB$ である。同じように三角形 $EFA$ は正三角形で、$AE=EF=DE$ である。
段 2（直線 $BE$ は線分 $AD$ の垂直二等分線）。段 1 より $BA=BD$、$EA=ED$ である。2 点 $A$、$D$ から等距離にある点の全体は線分 $AD$ の垂直二等分線なので、$B$ と $E$ はその上にある。$B\ne E$ なので、直線 $BE$ は線分 $AD$ の垂直二等分線である。したがって直線 $BE$ についての折り返し（鏡映）は $A$ と $D$ を入れ替え、$B$、$E$ を動かさない。
段 3（$C'$、$F'$ と正三角形）。直線 $BE$ について $C$、$F$ を折り返した点を $C'$、$F'$ とする。折り返しは長さを変えないので、正三角形 $BCD$ は、$B\mapsto B$、$D\mapsto A$、$C\mapsto C'$ により正三角形 $BAC'$ に移る。同じように正三角形 $EFA$ は正三角形 $EF'D$ に移る。また $C'F'=CF$ である。
段 4（$C'$ と $G$ は直線 $AB$ の反対側）。六角形は凸なので、$C$ は対角線 $BD$ について $A$ と反対側にある。折り返しで直線 $BD$ は直線 $BA$ に、$A$ は $D$ に移るので、$C'$ は直線 $AB$ について $D$ と反対側にある。六角形は凸で $AB$ はその辺なので、六角形の内部の点 $G$ と頂点 $D$ は直線 $AB$ の同じ側にある。よって $C'$ と $G$ は直線 $AB$ の反対側にある。同じように、$F'$ と $H$ は直線 $DE$ の反対側にある。
段 5（$G$ は外接円の上）。正三角形 $ABC'$ の外接円を考える。直線 $AB$ について $C'$ と反対側の弧 $AB$ の上の点 $X$ では、四角形 $AXBC'$ が円に内接するので $\angle AXB=180^\circ-\angle AC'B=180^\circ-60^\circ=120^\circ$ である。線分 $AB$ を $120^\circ$ で見込む点のうち、直線 $AB$ について同じ側にあるものは、円周角の定理の逆（円周角の定理（高校数学））によりこの弧の上にある。段 4 より $G$ はこの側にあり $\angle AGB=120^\circ$ なので、$G$ は $C'$ を含まない弧 $AB$ の上にある。cor-ptol-equilateral を正三角形 $C'AB$ と点 $G$ に使って
$$ GC'=GA+GB $$
である。同じように $HF'=HD+HE$ である。
段 6（三角不等式）。段 5 より
$$ AG+GB+GH+DH+HE=C'G+GH+HF' $$
である。三角不等式を 2 回使うと $C'G+GH\ge C'H$、$C'H+HF'\ge C'F'$ なので、右辺は $C'F'$ 以上である。段 3 より $C'F'=CF$ なので、$AG+GB+GH+DH+HE\ge CF$ である。$\square$