※このエントリはSchemeの例題を解くにあたって必要に迫られ、数学3の微分(導関数)をやり直した記録です。
\frac{f(x)}{g(x)}
って
f(x) \times g(x)^{-1}
と書き直すことが出きるので、商の導関数の公式は積の導関数の公式で行けるはずだよね、と思ったのですが、その証明に手間取ったので記録。「そんなんネットに転がってるだろ」とググりまくったんですが、見付けられないものですなぁ。
さてまずの前提。
・積の導関数の公式
y=f(x) \times g(x)
ならば、yの導関数、y'は
y'=f'(x) \times g(x) + f(x) \times g'(x)
・商の導関数の公式は
y= \frac{f(x)}{g(x)}
ならば
y'= \frac{f'(x) \times g(x) - f(x) \times g'(x)}{{g(x)}^2}（式１）
さて証明すべきは
y = \frac{f(x)}{g(x)}
すなわち
y=f(x) \times g(x)^{-1}
を積の導関数の公式で微分した式が、商の導関数の公式（式１）と一致すれば良いわけですな。では積の導関数の公式にしたがって展開してみましょう。
y' = f'(x) \times g(x)^{-1} + f(x) \times [g(x)^{-1}]'（式２）
（式１）の分母、分子に
g(x)^{-2}
を掛けると
y' = f'(x) \times g(x)^{-1} - f(x) \times g'(x) \times g(x)^{-2}（式３）
ところで
y=\frac{1}{g(x)}
のとき
y' = \frac{1' \times g(x) - 1 \times g'(x)}{g(x)^2} = -\frac{g'(x)}{g(x)^2} = -g'(x) \times g(x)^{-2} = [g(x)^{-1}]'（式４）
なので（式３）を
y' = f'(x) \times g(x)^{-1} - f(x) \times g'(x) \times g(x)^{-2}
= f'(x) \times g(x)^{-1} + f(x) \times [-g'(x) \times g(x)^{-2}]
と変形して（式４）を代入すると
y' = f'(x) \times g(x)^{-1} + f(x) \times [g(x)^{-1}]'
よって
y = \frac{f(x)}{g(x)}
を商の導関数の公式にしたがって微分した式、（式１） = （式３）は、積の導関数にしたがって微分した式、（式２）と等しい。
QED.
余談（もしくは、「波よ、俺の苦心を聞いてくれ」）
・2週間くらい暇を見付けては、紙に鉛筆でごにょごにょ書いて、あーでもないこーでもないと試行錯誤した。
・肝は
y=\frac{1}{g(x)}
を微分すると
y' = -\frac{g'(x)}{g(x)^2}
となることに気付いて、（式４）を導き出せたことですな。まあ某古書店で立ち読みした「チャート式数学３」に記してあるのを発見したわけですが実は。
しかし2週間ほど試行錯誤を重ねていたからこそ、この式を見た瞬間、閃いたに違いない。
というわけで誰か頑張った私を褒めてください。（厚かましい）
追記１
@ma-oshita さんがコメントで対数微分法の使用を提案されていたので
「あー、対数微分法ねー。対数微分法ってアレかー、アレだよねー……モスバーガーの新メニューのアレだっけ？」
状態になったのでまたチャート式数学３を立ち読みして勉強し直しました。もう高校数学の軽い復習本くらい買っとこうかしら。
では
y = f(x) \times g(x)^{-1} （式１）
と
y = \frac {f(x)} {g(x)} （式２）
を対数微分法で微分した式が一致したら、商の導関数の公式が積の導関数の公式でも代用可能としましょう。（これでいいのか？）
式１のとき
\log y = \log (f(x) \times g(x)^{-1})\\
\begin{align}
\frac {y'} {y} &= \log (f(x) \times g(x)^{-1})' \\
&= ( \log f(x))' + ( \log g(x)^{-1})' \\
&= ( \log f(x))' - ( \log g(x))' \\
\end{align}
よって
y' = y \times [( \log f(x))' - ( \log g(x))'] ──Ａ
また、式２は
\log y = \log \frac {f(x)} {g(x)}\\
\begin{align}
\frac {y'} {y} &= [\log \frac {f(x)} {g(x)}]' \\
&= ( \log f(x))' - ( \log g(x))' \\
\end{align}
よって
y' = y \times [( \log f(x))' - ( \log g(x))'] ──Ｂ
よって、式１を対数微分した式、Ａと、式２を対数微分した式、Ｂは同値。Q.E.D.
……本当にこれで証明になっているのか疑問ですが、あの、間違っていたらコメント等で指摘していただけると幸いです。
追記２
@7shi さんにコメントで、私のゴチャゴチャした証明を、すっきりと証明しなおしていただきました。
展開した式をどうまとめるかばかりに気が向いてしまい、式の展開に気をつかえば良かったのですね。
ありがとうございました。