---
tag: 003QDZ4T16
kind: statement
role: corollary
name: A function with zero derivative is constant
msc: [26A24]
uses: [0BARQY52N5]
sources:
  - url: https://en.wikipedia.org/wiki/Mean_value_theorem
    locator: Implications
---

## Statement

Let $I$ be an open interval and let $f \colon I \to \mathbb{R}$ be differentiable with $f'(x) = 0$ for all $x \in I$.
Then $f$ is constant on $I$.

## Remarks

For $x < y$ in $I$, the [[mean value theorem|0BARQY52N5]] gives $f(y) - f(x) = f'(c)(y - x) = 0$.
The domain must be an interval. On $(0, 1) \cup (2, 3)$, a function equal to $0$ on one part and $1$ on the other has zero derivative.
So two antiderivatives of a function on an interval differ by a constant. Mathlib states the result as `is_const_of_deriv_eq_zero`.

## Explanations

### L1 human

A function whose slope is zero everywhere on an interval never rises or falls.
So its graph is a horizontal line.