---
tag: 012C7GFF20
kind: statement
role: proposition
name: 1 + x is at most exp x
msc: [33B10, 26D15]
uses: [0D7GRZ2ADX, 005JT76HCK]
sources:
  - url: https://en.wikipedia.org/wiki/Exponential_function
    locator: Properties
---

## Statement

For every real $x$,
$$1 + x \le e^x,$$
with equality if and only if $x = 0$.

## Remarks

The line $y = 1 + x$ is the tangent to the graph of $e^x$ at $0$. The graph of a [[convex function|0D7GRZ2ADX]] lies above its tangent lines, by [[the derivative criterion|005JT76HCK]].
For $x \ge 0$ the claim also follows from the series, since the other terms are nonnegative.
Taking logarithms gives [[$\ln y \le y - 1$|04CBRA4JRK]] for $y > 0$. Mathlib states the inequality as `Real.add_one_le_exp`.

## Explanations

### L1 human

The graph of $e^x$ lies above its tangent line at $0$.
That tangent line is $y = 1 + x$.