I was reading the proof of Theorem 6.2.2., Pazy, Semigroups of Linear Operators...Equations and confused.
Essentially we want to show ${\lim}_{x\uparrow a}|f(x)|=\infty$. I believe by definition this means that
For any $K>0$ there exists $\delta>0$ such that ($x\in D(f)$, $0\leq a-x<\delta $ $\implies$ $K<|f(x)|$),
where by $D(f)$ I mean the domain of $f$. (It may be the case that ${\lim}_{x\uparrow a}$ means ${\lim}_{x\uparrow a,x\neq a}$, but it does not seem to matter here. )
So negating this readily gives us
For any $\delta >0$ there exists $K>0$ such that ($x\in D(f)$, $0\leq a-x<\delta $ $\implies$ $K\geq |f(x)|$)
What is confusing me is that in the aforementioned proof, we first negate essentially $\overline{\lim}_{x\uparrow a}|f(x)|=\infty$ to get $|f(x)|\leq K$ for (basically) any $x$. (In the following proof I am looking at $\overline{\lim}_{t\uparrow t_{\mathrm{max}}}\|u(t)\|=\infty$)
and then to show ${\lim}_{t\uparrow t_{\mathrm{max}}}\|u(t)\|<\infty$ we negate ${\lim}_{t\uparrow t_{\mathrm{max}}}\|u(t)\|=\infty$ to get
there is a sequence $t_n\uparrow t_{\mathrm{max}}$ and a constant $K$ such that $\|u(t_n)\|\leq K$ for all $n$
and derive contradiction using the continuity of $t\mapsto \|u(t)\|$.

But don't we have ${\lim}_{t\uparrow t_{\mathrm{max}}}\|u(t)\|=\infty$ already when we say the negation of $\overline{\lim}_{t\uparrow t_{\mathrm{max}}}\|u(t)\|=\infty$ in the proof is absurd?
I thought unlike the usual definition of limit, $\lim...=\infty$ does not require the subtlety of existence of the limit but Pazy seems to be distinguishing limsup and lim for this case as well and I am confused.

Your first quantified statement reads $$\forall K > 0 \quad \exists \delta > 0 \quad \forall x \in D(f) \quad 0 \le x-a < \delta \implies K < |f(x)|.$$
You didn't negate it correctly. The proper negation is $$ \exists K > 0 \quad \forall \delta > 0 \quad \exists x \in D(f) \quad 0 \le x-a < \delta\quad \& \quad K \ge |f(x)|.$$
Your statement "$|f(x)| \le K$ for (basically) any $x$" isn't true due to the existential quantifier on $x$.