$x^y=y^x$. Prove that $x^y>e^e$ Let $x>1$, $y>1$ and $x\neq y$ such that $x^y=y^x$. Prove that:
$$x^y>e^e$$
We can assume $y=kx$, where $k>1$. 
Hence, $x=k^{\frac{1}{k-1}}$ and $y=k^{\frac{k}{k-1}}$ and we need to prove that $f(k)>e^e$, where $f(k)=k^{\frac{k^{\frac{k}{k-1}}}{k-1}}$.
We can show that $f'(k)>0$ for $k>1$ and $\lim\limits_{k\rightarrow1^+}f(k)=e^e$ and we are done.
Is there a nice proof for this inequality? Thank you!
 A: We have to minimize the function $$f(x)=x^{y}\tag{1}$$ where $x$ and $y$ are connected by equation $$x^{y}=y^{x}\tag{2}$$ As usual we need to find derivative $f'(x)$ and this is bit tricky here. First we take logarithm of the equation $(2)$ to get $$y\log x = x\log y$$ and then differentiating with respect to $x$ we get $$\frac{y}{x} + y'\log x = \log y + \frac{xy'}{y}$$ or $$y' = \frac{y}{x}\cdot\frac{y - x\log y}{x - y\log x}\tag{3}$$ From $(1)$ we get $$\log f(x) = y\log x$$ and differentiation gives us $$\frac{f'(x)}{f(x)} = \frac{y}{x} + y'\log x$$ and using equation $(3)$ we get $$\frac{f'(x)}{f(x)} = \frac{y}{x}\left(1 + \frac{y\log x - x\log x\log y}{x - y\log x}\right)$$ and  thus $f'(x) = 0$ is possible only when $$\log x\log y = 1\tag{4}$$ so that $y = \exp(1/\log x)$ and $$f(x) = x^{y} = y^{x} = \exp\left(\frac{x}{\log x}\right)$$ It can be easily checked that the function $g(x) = x/\log x$ attains it's minimum value at $x = e$ and therefore $f(x) = e^{g(x)}$ also attains it's minimum value at $x = e$ and therefore the minimum value of $f(x) = x^{y}$ is $e^{e}$.
A: I count this as a partial answer: If you keep to the branch $y \le x$ (which given the symmetry of the problem I think is OK), then using the known properties of the Lambert function you have $y = x$ for $0 \le x \le e$. Now consider $x^y$. For $0 \le x \le e$ you have $x^y = x^x$. This solution can be considered "known" in the sense that elementary means can used to deduce its properties, such as general shape. If you know consider the equation $y = -x \frac{W(-\frac{\ln x}{x})}{\ln x}$ and look at $x^y$ then Maple gives the following far from obvious structure (see attached figure).
To complete the answer you would have to show that $\frac{d x^y}{d x} \ge 0$ for $x \ge e$. This looks a fearsome task but it may be possible using only known properties of Lambert's function (for example) $\frac{d W(z)}{d z} = \frac{W(z)}{z (1 + W(z))}$ (from Wiki).
From the figure you seem to have (for the chosen branch) that $x^y > e^e$ for $x > e$.

A: I think this can be solved by recasting it in the language of Lagrange multipliers.  We wish to maximize the function $f(x,y,z) = z$ subject to the constraints $g_1(x,y,z) = x^y - z= 0$ and $g_2(x,y,z) = y^x - z = 0$.  By the properties of Lagrange multipliers, $f$ will have a local extremum on the surface specified by these constraints if there exists a point where
$$
\nabla f + \lambda_1 \nabla g_1 + \lambda_2 \nabla g_2 = 0.
$$
Taking these gradients, we find that we must have
\begin{align*}
\lambda_1 [y x^{y-1}] + \lambda_2 [(\ln y) y^x] &= 0 \\
\lambda_1 [(\ln x) x^y] + \lambda_2 [x y^{x-1}] &= 0 \\
1 -\lambda_1 - \lambda_2  &= 0
\end{align*} 
We can then eliminate $\lambda_2$ from these equations:
\begin{align*}
\lambda_1 [y x^{y-1}] + (1 - \lambda_1) [(\ln y) y^x] &= 0 \\
\lambda_1 [(\ln x) x^y] + (1 - \lambda_1) [x y^{x-1}] &= 0
\end{align*} 
Then we can solve each equation for $\lambda_1$ to eliminate it from our system:
$$
\lambda_1 = \frac{(\ln y) y^x}{(\ln y) y^x - y x^{y-1}} = \frac{x y^{x-1}}{x y^{x-1} - (\ln x) x^y } 
$$
Inverting both sides of this equation and simplifying yields
$$
\frac{y x^{y-1}}{(\ln y) y^x} = \frac{(\ln x) x^y }{x y^{x-1}},
$$
which further simplifies to
$$
(\ln x) (\ln y) = 1.
$$
Thus, at the extremum (if it exists), we must have $y = e^{1/\ln x}$ and $z = y^x = e^{x/\ln x}.$  But on the interval $(1, \infty)$, the function $x / \ln x$ has a global minimum at $x = e$.  Moreover, since the exponential function is monotonically increasing, the function $z = e^{x/\ln x}$ has a global minimum at $x = e$ as well.  Thus, $z \geq e^e$, with equality at the point $x = y = e$.
A: You certainly have $_{k \to 1^+}k^{\frac{k}{k-1}} = e$. This follows by considering $z = k^{\frac{k}{k-1}}$ so that $\ln z = \frac{k}{k-1} \ln k$, then lim$_{k \to 1^+} \ln z = \frac{1 + \ln k}{1} = 1$ (L'Hopital) i.e. $z = e$ (alternatively, look at the definition of $e = $ lim$_{n \to \infty} (1 + \frac{1}{n})^n$). Then look at $f(k) = z^z$ and write $\ln(f) = z \ln z$ to show lim$_{k \to 1^+} \ln(f) \to e \ln e$, giving lim$_{k \to 1^+} f(k) = e^e$.
