Real function/Open interval/Local extrema/Differentiable/Derivative zero/Fact

Let

be a function which attains in a local extremum, and is differentiable there.

Then

holds.