命題 不等式 \[ x_0 \leq y_0 < y_1 \leq x_1 \]を満たす実数\(x_0,x_1,y_0,y_1\)を考え、\(X = [x_0,x_1], Y = [y_0, y_1]\)とおく。微分可能な関数\(f: X \to Y\)を考えたとき、 \[ |f'(a)| \leq 1 \] を満たす\(X\)の要素\(a\)が存在する。
証明 もし\(f'(a) = 0\)を満たす\(X\)の要素\(a\)が存在するならば、\(|f'(a)| \leq 1\)がいえる。\(X\)の任意の要素\(x\)に関して\(f'(x) \neq 0\)とすると、中間値の定理より\(f'(x)\)は常に\(0\)以上か常に\(0\)以下である。常に\(0\)以上として一般性を失わない。このとき関数\(f\)は広義単調増加で、\(Y\)の任意の要素\(y\)に対して、 \[ y_0 \leq f(y_0) \leq f(y) \leq f(y_1) \leq y_1 \] がいえる。平均値の定理から、 \[ |f'(a)| = \left|\dfrac{f(y_1) - f(y_0)}{y_1 - y_0}\right| \] を満たす\(Y\)の要素\(a\)が存在する（\(a\)は\(X\)の要素でもある）。大小関係を考えると、 \[ \left|\dfrac{f(y_1) - f(y_0)}{y_1 - y_0}\right| \leq \left|\dfrac{y_1 - y_0}{y_1 - y_0}\right| = 1 \] なので、\(|f'(a)| \leq 1\)がいえる。（証明終わり）※上の証明は葛貫森信（くずにゃん）さんの以下のツイートをもとにしています。 https://twitter.com/morinobukuzunu1/status/937248237810958336 https://twitter.com/morinobukuzunu1/status/937253566984495104
