Proving that if a sequence $(a_n)$ is monotonic decreasing and $\lim a_n = l$, then $l=\inf \{a_n:n\in\mathbf{N}\}$ I am self-learning Real Analysis. In proving results about sequences and series of reals, it might useful to use the below fact, so I want to write a rigorous proof for it. But, I'd like to check if the proof is sound. Is there a more clever way to prove this?

Let $(a_n)$ be a sequence such that the following conditions are met:
(1) $a_1 \ge a_2 \ge a_3 \ldots \ge a_n \ge a_{n+1} \ge \ldots$
(2) $(a_n) \to l$
Then,
$$l = \inf \{a_n:n \in \mathbf{N}\}$$

Proof.
Claim I. $l$ is a lower bound for $(a_n)$.
Let $A:=\{a_n:n \in \mathbf{N}\}$. Suppose there exists an $N_1\in \mathbf{N}$, such that $a_{N_1} < l$. Put $l-a_{N_1}=\epsilon$. Since $(a_n) \to l$, there exists an $N_2 \in \mathbf{N}$, such that for all $n \ge N_2$,
$$\vert a_n - l \vert < \frac{\epsilon}{2}$$
Let $N=\max\{N_1,N_2\}$. Then,
$$\vert a_N - l \vert < \frac{\epsilon}{2}=\frac{a_{N_1} - l}{2} \tag{1}$$
Since $N \ge N_1$, we have $a_{N} \le a_{N_1} < l$. Therefore,
$$\lvert\frac{a_{N_1} - l}{2}\rvert \le \lvert \frac{a_N - l}{2}\rvert \tag{2}$$
From (1) and (2),
$$\lvert a_N - l \rvert < \lvert \frac{a_N - l}{2} \rvert$$
This is a contradiction. Consequently, $l \le a_n$ for all $n \in \mathbf{N}$.
Claim II. $l$ is the greatest lower bound.
Pick an arbitrary $\epsilon > 0$. Let's give ourselves an $\epsilon$ of room. Consider $(l,l+\epsilon)$. Because $(a_n) \to l$, there exists $N$ such that for all $n \ge N$, $l < a_n < l + \epsilon$. Since, this is true for all $\epsilon > 0$, $l$ is the greatest lower bound.
 A: Your proof looks correct to me. You can alternatively prove like this also:
Suppose that $\displaystyle A:=\inf \{a_{n} :n\in \mathbb{N} \}$
Fix any $\displaystyle \epsilon  >0.$ By definition of $\displaystyle A$, there exists $\displaystyle M\in \mathbb{N}$ such that $\displaystyle A\leq a_{M} < A+\frac{\epsilon }{2}$. Since $\displaystyle ( a_{n})$ is a decreasing sequence, it follows by definition of $\displaystyle A$ that for all $\displaystyle n\geq M$, $\displaystyle A\leq a_{n} \leq a_{M} < A+\frac{\epsilon }{2}$
It follows that $\displaystyle 0\leq a_{n} -A< \frac{\epsilon }{2}$ for all $\displaystyle n\geq M$
Since $a_n\to L$, there exists $\displaystyle N\in \mathbb{N}$ such that $\displaystyle n\geq \mathbb{N} \Longrightarrow |a_{n} -L|< \frac{\epsilon }{2}$.
Let $\displaystyle K=\max \{N,M\}$, then for all $\displaystyle n\geq K$, we have $\displaystyle |L-A|=|L-a_{n} +a_{n} -A|\leq |L-a_{n} |+|a_{n} -A|< \frac{\epsilon }{2} +\frac{\epsilon }{2} =\epsilon \Longrightarrow |L-A|< \epsilon $
Since $\displaystyle \epsilon  >0$ is arbitrary, it follows that $\displaystyle L=A$.
A: Here is an attempt to shorten the argument.
Suppose there exists one $M$ such that $a_M<l$. This would imply that $|a_n-l|\geq |a_M-l|,\forall n \geq M$, but this contradicts the assumption that $a_n \to l$ so $a_n \geq l, \forall n \in \mathbb{N}$. Therefore $\inf{a_n}\geq l$.
Suppose $\inf a_n > l$, set $\varepsilon_0=\inf a_n -l >0$. But since $a_n \to l$, there exists $N$ such that $\forall n \geq N,|a_n-l|<\varepsilon_0$ but this is a contradiction therefore $\inf a_n = l$.
