On the Limit of Stirling's Approximation

I have recently proven the following curious identity: For real $x \geqslant 1$, \begin{align} \lfloor x \rfloor! = x^{\lfloor x \rfloor} e^{1-x} e^{\int_{1}^{x} \text{frac}(t)/t \ dt} \end{align} where $\text{frac}(x)$ denotes the fractional part (function) of $x$. A proof follows from an application of Legendre's Theorem on the order of a prime divisor of the factorial function and an identity involving the de Bruijn function.

An asymptotic expansion of the integral as $x \to \infty$ yields Stirling's Approximation, hence the title of the post. Is this exact result known in the literature?

Thanks!

That works. There are two parts. Write $x = n + \delta,$ with $n \in \mathbb Z$ and $0 \leq \delta < 1.$ Your identity $$ \lfloor x \rfloor! = x^{\lfloor x \rfloor} e^{1-x} e^{\int_{1}^{x} \text{frac}(t)/t \ dt}.$$ becomes $$ n! = (n + \delta)^n \; e^{1-n} \; e^{-\delta} \; e^{\int_{1}^{n} \text{frac}(t)/t \ dt} \; e^{\int_{n}^{n + \delta} \text{frac}(t)/t \ dt} $$ As the left hand side $n!$ is independent of $\delta,$ we need the factor that depends on $\delta$ to be a constant (but depending on $n$). Note that $$ {\int_{n}^{n + \delta} \text{frac}(t)/t \ dt} = \delta + n \log \left( \frac{n}{n+\delta} \right) $$ So the factor $$ (n + \delta)^n \; e^{-\delta} \; e^{\int_{n}^{n + \delta} \text{frac}(t)/t \ dt} = (n + \delta)^n \; e^{-\delta} \; e^{\delta} \; \left( \frac{n}{n+\delta} \right)^n = n^n $$ is indeed independent of $\delta,$ and your identity is $$ n! = n^n \; e^{1-n} \; e^{\int_{1}^{n} \text{frac}(t)/t \ dt} .$$ This is rather cute. Proof by induction: it is true for $n=1,$ both sides are just $1.$ In the induction step, we get the right hand side with $(n+1)$ as $$ RHS_{n+1} = (n+1)^{n+1} \; e^{-n} \; e^{\int_{1}^{n} \text{frac}(t)/t \ dt} \; e^{\int_{n}^{n+1} \text{frac}(t)/t \ dt}. $$ The final factor is what we got with $\delta = 1,$ that is $$ {\int_{n}^{n+1} \text{frac}(t)/t \ dt} = 1 + n \log \left( \frac{n}{n+1} \right) $$ So $$ RHS_{n+1} = (n+1) \; (n+1)^n \; e^{-n} \; e^{\int_{1}^{n} \text{frac}(t)/t \ dt} \; \cdot e \cdot \; \left( \frac{n}{n+1} \right)^n $$ and $$ RHS_{n+1} = (n+1) \; n^n \; e^{1-n} \; e^{\int_{1}^{n} \text{frac}(t)/t \ dt} $$ and the induction hypothesis says $$ RHS_{n+1} = (n+1) \; n! $$

Although my question above concerns whether or not the posted identity is a known result, I'll add the following elementary and direct proof (without recourse to Legendre's Theorem or the de Bruijn function needed for a more general version).

Proposition For real $x \geqslant 1$, the following identity holds \begin{align} \lfloor x \rfloor! = x^{\lfloor x \rfloor} e^{1-x} e^{\int_1^{x} \frac{\text{frac}(t)}{t} \ dt}. \end{align}

Proof. For each positive integer $n$, the function $f(t) = \tfrac{\text{frac}(t)}{t}$ equals $1 - \tfrac{n}{t}$ on $[n,n+1]$. Thus, \begin{align} \int_{1}^{n} f(t) \ d t & = \sum_{k = 1}^{n-1} \int_{k}^{k+1} (1 - \tfrac{k}{t}) \ dt \\ & = n - 1 + \log n! - n \log n. \end{align} By splitting the following integral into two pieces, we compute \begin{align} \int_{1}^{x} f(t) \ d t & =\int_{1}^{\lfloor x \rfloor} f(t) \ d t + \int_{\lfloor x \rfloor }^{x} f(t) \ dt \\ & = \lfloor x \rfloor - 1 + \log \lfloor x \rfloor! - \lfloor x \rfloor \log \lfloor x \rfloor + \int_{\lfloor x \rfloor}^{x } f(t) \ d t. \end{align} We need only to compute the last integral, \begin{align} \int_{\lfloor x \rfloor}^{x } f(t) \ dt & = \int_{0}^{\text{frac}(x) } \frac{\text{frac}(t + \lfloor x \rfloor)}{t + \lfloor x \rfloor} \ d t \\ & = \int_{0}^{ \text{frac}(x) } \frac{t}{t + \lfloor x \rfloor } \ d t \\ & =\text{frac}(x) + \lfloor x \rfloor \log \lfloor x \rfloor - \lfloor x \rfloor \log x \end{align} by a change of variables from $t$ to $t + \lfloor x \rfloor$. Hence, together these identities yield \begin{align} \int_{1}^{x} f(t) \ dt & = x - 1 + \log \lfloor x \rfloor! - \lfloor x \rfloor \log x, \end{align} which completes the proof of the claim.