Proving that two structures are elementarily equivalent using the Tarski-Vaught Test I wish to show that $(\mathbb{N},<)\equiv(\mathbb{N}+\mathbb{Z},<)$.
I tried to approach the problem using the Tarski-Vaught Test, where $\mathbb{N}+\mathbb{Z}$ is an ordered set that is order-isomorphic to the ordered set $\mathbb{N}$ followed by the ordered set $\mathbb{Z}$, and $\equiv$ is elementary equivalence. In other words, what needs to be shown is that for every first-order formula $\phi(x, y_1, \dots, y_k)$ ($k\in \{0, 1, \dots\}$), and for every $n_1, \dots, n_k \in \mathbb{N}$, if $\exists x, \phi(x, n_1, \dots, n_k)$ holds in $(\mathbb{N}+\mathbb{Z},<)$ then it holds in $(\mathbb{N}, <)$.
Attempted proof We shall proceed by structural induction on $\phi$.


*

*Basis: If $\phi(x,y_1) = (x < y_1)$, we can choose some $x^*\in \mathbb{N}+\mathbb{Z}$ such that $x^* < n_1$, in which case $x^* \in \mathbb{N}$, and we're done. If $\phi(x,y_1) = (y_1 < x)$, setting $x^* := n_1 +1$ we have $x^* \in \mathbb{N}$ and $\phi(x^*, n_1)$.

*Induction step.


*

*Suppose $\phi(x,y_1,\dots,y_k)=\psi(x,y_1,\dots,y_k)\vee\xi(x,y_1,\dots,y_k)$. Then we may choose some $x^* \in \mathbb{N}+\mathbb{Z}$ such that $\psi(x^*,n_1,\dots,n_k)\vee\xi(x^*,n_1,\dots,n_k)$. If $\psi(x^*,n_1,\dots,n_k)$, then by the induction hypothesis we can choose some $x^{**}\in\mathbb{N}$ such that $\psi(x^{**},n_1,\dots,n_k)$; otherwise, we can choose some $x^{**}\in\mathbb{N}$ such that $\xi(x^{**},n_1,\dots,n_k)$. Either way, $\phi(x^{**},n_1,\dots,n_k)$.

*Suppose $\phi(x,y_1, \dots, y_k) = \neg\psi(x,y_1,\dots,y_k)$. I don't know how to proceed.

*Suppose $\phi(x,y_1, \dots, y_k) = \forall z, \psi(x,y_1,\dots,y_k,z)$.  I don't know how to proceed.
 A: This should really be a comment, since it doesn't use Tarski-Vaught, but it's vastly too long:
I actually think T-V is the wrong approach here; even though it does work, EF-games, as mentioned in the comments, do the job more cleanly IMO. 
Interestingly, there's also a lengthy but elementary proof via an elementary chain construction (see the bottom of page $16$ here if you're not familiar with these). In particular, this proof is semantic: it builds a model which is elementarily equivalent to both structures simultaneously. To me, this gives a good explanation for why the two structures are elementary equivalent, rather than just proving that they are; I find this explanation much better than the one provided by induction on formula complexity, and better even that the proof via EF-games.
Really, all this proof is doing is showing that the theories of the two structures have the same countable saturated model, but you may not be familiar with these, so I'm giving a ground-up proof.
First, note that - up to isomorphism - there is only one linear order $L$ with the following properties:


*

*$L$ is countable.

*$L$ is of the form "$\mathbb{N}+\mathbb{K}$" for some linear order $\mathbb{K}$.

*$\mathbb{K}$ is of the form "$\mathbb{I}\cdot\mathbb{Z}$," where $\mathbb{I}$ is a dense linear order without endpoints. (Remember how multiplication of linear orders works: "$A\cdot B$" means "replace each point in $A$ with a copy of $B$".)
This is a consequence of Cantor's theorem that there is only one countable dense linear order without endpoints, up to isomorphism; if you haven't seen it before, this is proved via a back-and-forth argument, and it's a good exercise.
So why do I care about this? Well, I'm going to argue that $L$ satisfies both $T_0=Th(\mathbb{N}, <)$ and $T_1=Th(\mathbb{N}+\mathbb{Z}, <)$; if so, we'll clearly have $T_0=T_1$, that is, $(\mathbb{N}, <)\equiv(\mathbb{N}+\mathbb{Z}, <)$.

I'll show why $L\models T_0$; the proof that $L\models T_1$ is basically the same.
We'll construct a sequence of models $M_i$ for $i\in\mathbb{N}$. Each $M_i$ will be a countable model of $T_0$, and we'll have $M_i\preccurlyeq M_{i+1}$, so their union $M_\infty=\bigcup_{i\in\mathbb{N}} M_i$ - being [the union of an elementary chain] - will satisfy $T_0$ as well; by construction, we'll have $M_\infty\cong L$. (In particular, countability will be guaranteed since $M_\infty$ is a countable union of countable sets.
So how will we do this?
For $M\models T_0$, let $\sim$ be the "finite distance" equivalence relation on $M$: $a\sim b$ if for some $n$ there are $c_1, . . ., c_n\in M$ such that $c_1=a, c_n=b$, and $c_{i+1}$ is the immediate successor of $c_i$. Say that a transversal of $M$ is a set $S\subseteq M$ such that $S$ contains exactly one element from each $\sim$-class. Basically, $\sim$ partitions $M$ into the initial "$\mathbb{N}$-piece" and a bunch of "$\mathbb{Z}$-pieces," and a transversal "names" each of these pieces with specific elements.
Now we'll build our sequence of models.


*

*Let $M_0=(\mathbb{N}, <)\models T_0$, and fix some $S_0$ a transversal for $M_0$. Okay, this transversal will consist of a single natural number, so that's boring; but bear with me.

*Let's say we've built $M_i$; pick a transversal $S_i$ of $M_i$. Let $\hat{M_i}$ be the expansion of $M_i$ by new constants $c_j$ naming the elements of $S_i$. Now consider the even larger language gotten by adding lots of new constant symbols $d_{s, t}$ for $s, t\in S$ with $s<t$, and a new constant $e$; and look at the theory $T_{0, i}$ in this language consisting of:


*

*$Th(\hat{M_i})$,

*$c_s<d_{s, t}<c_t$,

*$\{$"$c_r$ and $d_{s, t}$ are at least distance $n$ apart": $r, s, t\in S$, $s<t$, $n\in\mathbb{N}\}$, and

*$\{(c_r<e)\wedge$"$c_r$ and $e$ are at least distance $n$ apart":$ r\in S\}$.


*Basically, the $d_{s, t}$s name new $\sim$-classes between each pair of existing ones; and $e$ names a new $\sim$-class bigger than all the existing ones.

*The theory $T_{0, i}$ is finitely consistent (exercise), so by Compactness and Lowenheim-Skolem we get a countable model $M_{i+1}\models T_0$ which is the reduct of a model of $T_{0,i}$ to the language of order, with $M_i$ as an elementary substructure of $M_{i+1}$.
Now you can show without too much work that taking the union of the chain $M_0\preccurlyeq M_1\preccurlyeq M_2\preccurlyeq ...$ gives (a linear order isomorphic to) $L$.

Incidentally, it's a good exercise to show that $A\preccurlyeq C$ and $B\preccurlyeq C$, and $A\subseteq B$ implies $A\preccurlyeq B$. The argument above shows in fact that $(\mathbb{N}, <)\preccurlyeq L$ and $(\mathbb{N}+\mathbb{Z}, <)\preccurlyeq L$, so in fact we get $(\mathbb{N}, <)\preccurlyeq(\mathbb{N}+\mathbb{Z}, <)$, which is the strong conclusion of T-V (stronger than mere elementary equivalence, that is).
