Applications of model theory to analysis Some of the more organic theories considered in model theory (other than set theory, which, from what I've seen, seems to be quite distinct from "mainstream" model theory) are those which arise from algebraic structures (theories of abstract groups, rings, fields) and real and complex analysis (theories of expansions of real and complex fields, and sometimes both).
While relationships with algebra seem quite apparent, I wonder what are some interesting results in real and complex analysis that have nice model-theoretical proofs (or better yet, only model-theoretical proofs are known!)? 
Of course, there's nonstandard analysis, but I hope to see some different examples. That said, I wouldn't mind seeing a particularly interesting application of nonstandard analysis. :)
I hope the question is at least a little interesting. I have only the very basic knowledge of model theory of that type (and the same applies to nonstandard analysis), so it may seem a little naive, but I got curious, hence the question.
 A: Using continuous model theory, Ilijas Farah, Brad Hart and David Sherman proved `blind man's version' of the Connes Embedding Problem:

There exists a separable ${\rm II}_1$-factor $M$ such that every other separable ${\rm II}_1$-factor embeds into an ultrapower of $M$.

I find this result pretty amusing. On the C*-algebra side, I like results à la the Löwenheim–Skolem theorem: build a non-separable C*-algebra with your favourite axiomatisable properties and go to a separable C*-algebra which inherits those properties.
A: There is a result in functional analysis whose first known proof uses non-standard techniques:

Theorem If a bounded linear operator $ T $ on a Hilbert space $ \mathcal{H} $ is polynomially compact, i.e., $ P(T) $ is compact for some non-zero polynomial $ P $, then $ T $ has an invariant subspace. This means that there is a non-trivial proper subspace $ W $ of $ \mathcal{H} $ such that $ p(T)[W] \subseteq W $.

The proof was given by Allen Bernstein and Abraham Robinson. Their result is significant because it is related to the so-called Invariant-Subspace Conjecture, an important unsolved problem in functional analysis. Paul Halmos, a staunch critic of non-standard analysis, supplied a standard proof of the result almost immediately after reading the pre-print of the Bernstein-Robinson paper. In fact, both proofs were published in the same issue of the Pacific Journal of Mathematics!
A: Ax found the following application in complex analysis:

Theorem: If $f : \mathbb{C}^n \to \mathbb{C}^n$ is an injective polynomial function, that is there exist $f_1,...,f_n  \in \mathbb{C}[X_1,...,X_n]$ such that $f=(f_1,...,f_n)$, then $f$ is surjective.

You can show that the theorem holds for $f : k^n \to k^n$ where $k$ is a locally finite field, therefore it holds for the algebraic closure $\overline{\mathbb{F}_p}= \bigcup\limits_{n \geq 1} \mathbb{F}_{p^n}$ of $\mathbb{F}_p$. Then, it holds for the (non trivial) ultraproduct $K=\prod\limits_{p \in \mathbb{P}} \overline{\mathbb{F}_p} / \omega$ where $\omega$ is a non principal ultrafilter over the set of primes $\mathbb{P}$, because the theorem can be expressed as a set of sentences of the first order. But $K$ is an algebraic closed field of caracteristic $0$ and the theory of algebraic closed fields of caracteristic $0$ is complete, so $K$ and $\mathbb{C}$ are elementary equivalent. Finally, Ax theorem is proved.
Ax theorem was generalized by Grothendieck.
