補題
K を実数体または複素数体とする。
f: [a, b] → K を連続写像とする。
f が (a, b) で微分可能で (a, b) 上で f’(t) = 0 とする。

このとき f は [a, b] 上で定数である。

証明
f(t) = a(t) + b(t) とする。

f’(t) = a’(t) + b’(t) であるから、
a’(t) = 0 かつ b’(t) = 0 である。

よって、本補題は K が実数体のときに帰着する。
しかし、K が実数体のときは平均値の定理より本補題は直ちに得られる。
証明終