Higher regularity of solutions of non-linear elliptic PDE Let $\Omega\subset \mathbb{R}^n$ be a bounded domain with infinitely smooth boundary. Let $u\in C^2(\bar \Omega)$ be a solution of the Dirichlet problem for the non-linear equation
\begin{eqnarray}
F(x,u,\nabla u,\nabla^2 u)=0 \mbox{ in } \Omega,\\
u=\phi \mbox{ in } \partial \Omega.
\end{eqnarray}
Let the equation be elliptic with respect to $u$. Let us assume that $F,\phi$ are infinitely smooth.
QUESTION. Is it true that the assumption $u\in C^{2,\alpha}(\bar \Omega)$ for some $0<\alpha<1$ implies that $u\in C^\infty(\bar \Omega)$? A reference would be very helpful. Special cases are also of interest.
Remark. So far I was able to find in literature two special cases of this statement.
(1) In the above generality in follows that the solution $u\in C^\infty(\Omega)$ (i.e. smooth in the interior of $\Omega$, not including the boundary). This is Lemma 17.16 in the Gilbarg-Trudinger book.
(2) The question has positive answer (including the boundary) for $F$ of the form
$$F(x,u,\nabla u,\nabla^2 u)=G(\nabla^2u)-f(x).$$
This is Prop. 5.1.10 in Qing Han's book.
 A: It is true and well-known (assuming $F$ is e.g. uniformly elliptic). The idea is sketched in ch. 9 of the book by Caffarelli-Cabre, but I am not sure of a precise reference at this level of generality. Interior smoothness follows from interior Schauder estimates (applied to difference quotients of $u$ and its derivatives, successively). To extend to the boundary, one uses boundary Schauder estimates. One can reduce to the case of zero boundary data and flat boundary (that is, $\Omega = B_1^+$ and $u = 0$ on $\{x_n = 0\}$) after subtracting $\phi$ and performing a diffeomorphism, which don't change the class of equations under consideration. The difference quotient method and boundary Schauder estimates show that $u_i$ are $C^{2,\alpha}$ up to the flat part of the boundary for $i < n$. By the uniform ellipticity of the equation, $u_{nn}$ can be written as a smooth function of $u_{ij}$ for $(i,\,j) \neq (n,\,n)$, $\nabla u$, $u$, and $x$. All of these quantities are $C^{1,\,\alpha}$ up to the flat part of the boundary, hence $u \in C^{3,\,\alpha}$ up to the boundary. Higher regularity follows after differentiating the equation (the coefficients of the differentiated equation are now $C^{1,\alpha}$) and applying a similar procedure. (One in fact only needs $u \in C^2\left(\overline{\Omega}\right)$; the first step uses instead the Calderon-Zygmund $W^{2,\,p}$ estimate for the equation solved by the difference quotients to get $C^{2,\alpha}$ regularity via embeddings (take $p > n$), and then proceeds as before).
