2直線のなす角

方針：原点を通る平行な直線 $\ell_0$ の式に、点 $(\cos\alpha,\sin\alpha)$ を代入する。
段 1（1 の証明）。$\ell$ が $y$ 軸に平行なら $\ell_0$ は $y$ 軸 $x=0$ である。点 $(\cos\alpha,\sin\alpha)$ が $x=0$ 上にあることは $\cos\alpha=0$ と同じで、$0^\circ\le\alpha<180^\circ$ の範囲では $\alpha=90^\circ$ と同値である。逆に $\alpha=90^\circ$ なら、$\ell_0$ は点 $(0,1)$ と原点を通るので $y$ 軸であり、$\ell$ は $y$ 軸に平行である。
段 2（2 の証明）。$\ell$ の傾きが $m$ なら、$\ell_0$ は傾き $m$ で原点を通るので $y=mx$ である。点 $(\cos\alpha,\sin\alpha)$ がその上にあるので
$$ \sin\alpha=m\cos\alpha $$
である。もし $\cos\alpha=0$ なら、この式から $\sin\alpha=0$ となり、$\cos^2\alpha+\sin^2\alpha=1$ に反する。よって $\cos\alpha\ne0$ で、両辺を $\cos\alpha$ で割ると $\tan\alpha=\dfrac{\sin\alpha}{\cos\alpha}=m$ である。$\square$

方針：2 本を平行移動して原点を通る直線 $\ell_{1,0}$、$\ell_{2,0}$ にする。なす角は平行移動で変わらないので、原点のまわりの 4 つの角を調べればよい。
段 1（平行な場合）。$\delta=0$ なら $\alpha_1=\alpha_2$ で、$\ell_{1,0}$ と $\ell_{2,0}$ は同じ点 $(\cos\alpha_1,\sin\alpha_1)$ と原点を通るので一致する。つまり $\ell_1$ と $\ell_2$ は平行か一致し、なす角は定義により $0^\circ=|\delta|$ である。逆に $\delta\ne0$ なら、2 本の傾斜角は違い、単位円との交点の組も違うので、$\ell_{1,0}$ と $\ell_{2,0}$ は原点だけで交わる。
段 2（4 つの角）。$\delta\ne0$ とする。$A=(\cos\alpha_1,\sin\alpha_1)$ は $\ell_{1,0}$ 上、$B=(\cos\alpha_2,\sin\alpha_2)$ は $\ell_{2,0}$ 上の点で、どちらも単位円の上半分（角が $0^\circ$ 以上 $180^\circ$ 未満の部分）にある。半直線 $OA$ と $OB$ のなす角 $\angle AOB$ は、$x$ 軸から測った角の差 $|\alpha_1-\alpha_2|=|\delta|$ に等しい。原点のまわりの 4 つの角は $\angle AOB$ とその隣の角なので、大きさは $|\delta|$ と $180^\circ-|\delta|$ である。
段 3（$90^\circ$ 以下のほうを選ぶ）。$|\delta|\le90^\circ$ なら $|\delta|$ のほうが $90^\circ$ 以下で、$\theta=|\delta|$ である。$|\delta|>90^\circ$ なら $180^\circ-|\delta|<90^\circ$ で、$\theta=180^\circ-|\delta|$ である。$\square$

方針：傾斜角を $\alpha_1$、$\alpha_2$、$\delta:=\alpha_1-\alpha_2$ とし、$\cos\delta$ と $\sin\delta$ を加法定理で傾きの式に直す。最後に lem-abl-angle-diff で $\theta$ と $\delta$ を結ぶ。
段 1（準備）。2 本とも傾きをもつので、lem-abl-slope-tan により $\cos\alpha_1\ne0$、$\cos\alpha_2\ne0$、$\tan\alpha_1=m_1$、$\tan\alpha_2=m_2$ である。
段 2（$\cos\delta$）。余弦の加法定理 $\cos(\alpha_1-\alpha_2)=\cos\alpha_1\cos\alpha_2+\sin\alpha_1\sin\alpha_2$ の右辺を $\cos\alpha_1\cos\alpha_2$ でくくると
$$ \cos\delta=\cos\alpha_1\cos\alpha_2\left(1+\frac{\sin\alpha_1}{\cos\alpha_1}\cdot\frac{\sin\alpha_2}{\cos\alpha_2}\right)=\cos\alpha_1\cos\alpha_2\,(1+m_1m_2) $$
である。
段 3（$\sin\delta$）。正弦の加法定理 $\sin(\alpha_1-\alpha_2)=\sin\alpha_1\cos\alpha_2-\cos\alpha_1\sin\alpha_2$ も同じようにくくると
$$ \sin\delta=\cos\alpha_1\cos\alpha_2\left(\frac{\sin\alpha_1}{\cos\alpha_1}-\frac{\sin\alpha_2}{\cos\alpha_2}\right)=\cos\alpha_1\cos\alpha_2\,(m_1-m_2) $$
である。
段 4（1 の証明）。lem-abl-angle-diff により、$\theta=90^\circ$ となるのは $|\delta|=90^\circ$ のときだけである（$|\delta|<90^\circ$ なら $\theta=|\delta|<90^\circ$、$|\delta|>90^\circ$ なら $\theta=180^\circ-|\delta|<90^\circ$）。$-180^\circ<\delta<180^\circ$ の範囲で $|\delta|=90^\circ$ となることは $\cos\delta=0$ と同値である。段 2 と $\cos\alpha_1\cos\alpha_2\ne0$ により、$\cos\delta=0$ は $1+m_1m_2=0$ と同値である。
段 5（$\tan\delta$）。$1+m_1m_2\ne0$ とする。段 2 から $\cos\delta\ne0$ なので、段 3 を段 2 で割って
$$ \tan\delta=\frac{\sin\delta}{\cos\delta}=\frac{\cos\alpha_1\cos\alpha_2\,(m_1-m_2)}{\cos\alpha_1\cos\alpha_2\,(1+m_1m_2)}=\frac{m_1-m_2}{1+m_1m_2} $$
である。
段 6（絶対値がつく理由）。lem-abl-angle-diff により、$\theta$ は $\delta$、$-\delta$、$180^\circ-\delta$、$180^\circ+\delta$ のどれかに等しい（$\delta$ の符号と大きさで決まる）。$\sin(x+180^\circ)=-\sin x$、$\cos(x+180^\circ)=-\cos x$ から $\tan(x+180^\circ)=\tan x$ であり、$\sin(-x)=-\sin x$、$\cos(-x)=\cos x$ から $\tan(-x)=-\tan x$ である。よって $\tan\theta$ は $\tan\delta$ か $-\tan\delta$ のどちらかである。一方、$0^\circ\le\theta<90^\circ$ なので $\tan\theta\ge0$ である。0 以上で、絶対値が $|\tan\delta|$ に等しい数は $|\tan\delta|$ だけなので、$\tan\theta=|\tan\delta|=\left|\dfrac{m_1-m_2}{1+m_1m_2}\right|$ である。$\square$

方針：2 直線の方向ベクトル $u_1=(1,m_1)$、$u_2=(1,m_2)$ のなす角を内積で求め、そこから直線のなす角を読む。正弦は、余弦から $\sin^2+\cos^2=1$ で求める。途中で出る恒等式が、分子 $m_1-m_2$ の正体を教える。
段 1（直線のなす角とベクトルのなす角）。$\ell_1$ は、1 点から $u_1$ の向きに進む直線で、$u_1$ と $-u_1$ のどちらの向きに進んでも同じ直線である（直線の方程式と点と直線の距離 の方向ベクトル）。$\ell_2$ と $u_2$ も同じである。原点から $u_1$、$-u_1$、$u_2$、$-u_2$ の向きに引いた 4 本の半直線が、平行移動した 2 直線の交点のまわりの 4 つの角を作る。$u_1$ と $u_2$ のなす角を $\varphi$（$0^\circ\le\varphi\le180^\circ$）とすると、4 つの角は $\varphi$ と $180^\circ-\varphi$ なので、$\theta$ はそのうち $90^\circ$ 以下のほうである。$\cos(180^\circ-\varphi)=-\cos\varphi$ で、$0^\circ$ 以上 $90^\circ$ 以下の角の余弦は $0$ 以上なので
$$ \cos\theta=|\cos\varphi|=\frac{|u_1\cdot u_2|}{|u_1|\,|u_2|}=\frac{|1+m_1m_2|}{\sqrt{1+m_1^2}\,\sqrt{1+m_2^2}} $$
である。2 つ目の等号で、内積となす角の関係 $u_1\cdot u_2=|u_1||u_2|\cos\varphi$（ベクトルの内積（高校数学））を使った。$u_1$ と $u_2$ が平行（$\varphi=0^\circ$ または $180^\circ$）のときは、2 直線は平行か一致で、4 つの角はできないが、定義により $\theta=0^\circ$ である。このときも $\cos\theta=1=|\cos\varphi|$ なので、上の式は成り立つ。
段 2（恒等式）。展開すると
$$ (1+m_1^2)(1+m_2^2)-(1+m_1m_2)^2=(1+m_1^2+m_2^2+m_1^2m_2^2)-(1+2m_1m_2+m_1^2m_2^2)=m_1^2-2m_1m_2+m_2^2=(m_1-m_2)^2 $$
である。
段 3（$\sin\theta$）。$0^\circ\le\theta\le90^\circ$ なので $\sin\theta\ge0$ で、$\sin\theta=\sqrt{1-\cos^2\theta}$ である。段 1・段 2 から
$$ \sin^2\theta=1-\frac{(1+m_1m_2)^2}{(1+m_1^2)(1+m_2^2)}=\frac{(1+m_1^2)(1+m_2^2)-(1+m_1m_2)^2}{(1+m_1^2)(1+m_2^2)}=\frac{(m_1-m_2)^2}{(1+m_1^2)(1+m_2^2)} $$
なので、$\sin\theta=\dfrac{|m_1-m_2|}{\sqrt{1+m_1^2}\,\sqrt{1+m_2^2}}$ である。
段 4（まとめ）。1：$\theta=90^\circ$ は $\cos\theta=0$ と同値で、段 1 の式の分子を見ると $1+m_1m_2=0$ と同値である。2：$1+m_1m_2\ne0$ なら $\cos\theta>0$ で、段 3 を段 1 で割ると、共通の分母 $\sqrt{1+m_1^2}\sqrt{1+m_2^2}$ が消えて $\tan\theta=\dfrac{|m_1-m_2|}{|1+m_1m_2|}$ となる。$\square$

方針：方向ベクトル $u_i=(-b_i,a_i)$ について prf-abl-slope-vector と同じ計算をし、内積・長さが法線ベクトルのものと一致することを使う。
段 1（内積と長さ）。$u_1\cdot u_2=(-b_1)(-b_2)+a_1a_2=a_1a_2+b_1b_2=n_1\cdot n_2$、$|u_i|=\sqrt{b_i^2+a_i^2}=|n_i|$ である。
段 2（$\cos\theta$）。prf-abl-slope-vector の段 1 は、2 直線の方向ベクトルが何であっても成り立つ。$u_1$、$u_2$ に使うと、段 1 から
$$ \cos\theta=\frac{|u_1\cdot u_2|}{|u_1|\,|u_2|}=\frac{|a_1a_2+b_1b_2|}{|n_1|\,|n_2|} $$
である。
段 3（恒等式）。展開すると
$$ (a_1^2+b_1^2)(a_2^2+b_2^2)-(a_1a_2+b_1b_2)^2=a_1^2b_2^2+b_1^2a_2^2-2a_1a_2b_1b_2=(a_1b_2-a_2b_1)^2 $$
である（左辺の $a_1^2a_2^2$ と $b_1^2b_2^2$ は打ち消し合う）。
段 4（$\sin\theta$ と $\tan\theta$）。$\sin\theta\ge0$ なので、段 2・段 3 から
$$ \sin\theta=\sqrt{1-\cos^2\theta}=\frac{\sqrt{(a_1^2+b_1^2)(a_2^2+b_2^2)-(a_1a_2+b_1b_2)^2}}{|n_1|\,|n_2|}=\frac{|a_1b_2-a_2b_1|}{|n_1|\,|n_2|} $$
である。$a_1a_2+b_1b_2\ne0$ なら $\cos\theta\ne0$ で、割ると $\tan\theta$ の式を得る。$a_1a_2+b_1b_2=0$ は $\cos\theta=0$、つまり $\theta=90^\circ$ と同値である。$\square$

方針：同じ積を 2 通りに計算し、実部と虚部を比べる。
段 1（成分で）。$\overline{w}=p_2-iq_2$ なので、$i^2=-1$ を使って展開すると
$$ (p_1+iq_1)(p_2-iq_2)=p_1p_2-ip_1q_2+iq_1p_2-i^2q_1q_2=(p_1p_2+q_1q_2)+i\,(q_1p_2-p_1q_2) $$
である。
段 2（極形式で）。$z=|z|(\cos\alpha+i\sin\alpha)$、$w=|w|(\cos\beta+i\sin\beta)$ と書けるので、$\overline{w}=|w|(\cos\beta-i\sin\beta)$ である。展開すると
$$ z\,\overline{w}=|z||w|\bigl((\cos\alpha\cos\beta+\sin\alpha\sin\beta)+i\,(\sin\alpha\cos\beta-\cos\alpha\sin\beta)\bigr) $$
で、余弦と正弦の加法定理により、実部の括弧は $\cos(\alpha-\beta)$、虚部の括弧は $\sin(\alpha-\beta)$ である。
段 3（比べる）。段 1 と段 2 の実部どうし、虚部どうしを比べ、$|z|=|u|$、$|w|=|v|$ を使うと最後の 2 式を得る。$\square$