How to prove $\exp(1)=e$ if $\exp$ is defined in a series expansion

calculuseulers-number-eexponential function

Right now I'm on a journey to clear up my confusion about exponential functions.
Thanks to your help in this stack, I was able to derive the basic properties of the ln function from the "position of defining ln in terms of integrals".

In this stack, the definitions of exp and e are as follows;

  • $$\exp(x):= 1+\frac{x}{1!}+\frac{x^2}{2!}+\frac{x^3}{3!}+\ldots,\ $$
  • $$e:=\lim_{n\to \infty} \left( 1+\frac{1}{n} \right)^{n} , n\in \mathbb{N}.$$

When defined in this way, the relationship between $\exp(x)$ and $e$ seems to be non-trivial .
We further assume that;

  • The theory on limit operations such as the scissors-out theorem and the theory on convergence conditions for power series are assumed to exist separately and independently.
  • For any integer $a>0$ where $n$ is an integer, $a^n$ is assumed to be defined in an inductive way.

My question.

Under these assumptions, how can we mathematically prove the following?
$$\exp(1)=e$$

There is a similar stack, but it does not seem to go into the definition of Napier-number.
If possible, we focus my questions on the following "How to evaluate from the lower side.

As far as I tried, I was probably able to suppress it from the upper side.
In other words, I believe I was able to prove the following.

$$e\le \exp(1)$$

Therefore, perhaps the question is how to find the series to suppress from below.

This means that the most desirable answer is to show
$$e\ge \exp(1)$$

Proof of $e\le exp(1)$
From the binomial theorem,

$$\left( 1+\frac{1}{n} \right)^{n}
=\sum_{k=0}^{n} {}_{n} \mathrm{C}_{k} \frac{1}{n^k}\\
=\sum_{k=0}^{n} \frac{1}{k!} \left( 1- \frac{1}{n} \right)\cdots \left( 1- \frac{1-k}{n} \right)\\
\le \sum_{k=0}^{n} \frac{1}{k!}
\le \exp(1)
$$

Best Answer

Let $N\in\Bbb N$. Then, for $n\geqslant N$,\begin{align}\left(1+\frac1n\right)^n&=\sum_{k=0}^n\frac1{k!}\left(1-\frac1n\right)\cdots\left(1-\frac{k-1}n\right)\\&\geqslant\sum_{k=0}^N\frac1{k!}\left(1-\frac1n\right)\cdots\left(1-\frac{k-1}n\right).\end{align}Therefore,$$e\geqslant\sum_{k=0}^N\frac1{k!}\left(1-\frac1n\right)\cdots\left(1-\frac{k-1}n\right)$$and so$$e\geqslant\lim_{n\to\infty}\sum_{k=0}^N\frac1{k!}\left(1-\frac1n\right)\cdots\left(1-\frac{k-1}n\right)=\sum_{k=0}^N\frac1{k!}.$$Since this takes place for each $N\in\Bbb N$,$$e\geqslant\sum_{k=0}^\infty\frac1{k!}=\exp(1).$$

Related Question