Quantifier Elimination

I want to prove the following: The structure $(\mathbb{Z},\equiv,0)$ has QE (with $\equiv$ a relation such that for all $m,n\in\mathbb{Z}$: $m\equiv n$ iff $m-n$ is even). I thought hereover in the following way: Suppose you have a formula $\phi$ in the language of the structure. Then bring this formula to the disjunctive normal form. The basis formulas in the language are: $$a=b,\neg(a=b),a=0,\neg(a=0),(a\equiv b),\neg(a\equiv b),(a\equiv 0),\neg(a\equiv 0)$$ and also combinations with $\wedge$. But than i have to find for all possible combinations a quantifier free formula. But how to do this?

Wat shall I do if i want to prove that a given structure has no QE?

Thank you ;)

-

1. First, notice that $a\equiv b$ is equivalent to $(a\equiv 0\wedge b\equiv 0)\vee (a\not\equiv 0\wedge b\not\equiv 0)$, and similarly for $a\not\equiv b$, so you can assume that there are none of those at the very beginning (before taking the normal form).
2. If you have a formula of the form $\varphi=\exists x \varphi'(x,\overline y)$ with $\varphi$ a conjunction of literals, one of which is $x=y_j$, then $\varphi$ is equivalent to $\varphi'(y_j,\overline y)$.
3. All other $\varphi$ are necessarily contradictory or tautological, which I will leave to you to prove.
Quantifier elimination is equivalent to substructural completeness, that is, a theory $T$ has q.e. iff for any model $M\models T$ and a nonempty subset $A$ of its universe, $T$ with the atomic diagram of $A$ is complete (or, equivalently, that any two models containing $A$ are elementarily equivalent), so you can show that a theory doesn't have q.e. by exhibiting a counterexample to substructural completeness (which may still be quite hard, as you need to find a suitable $A$ and show that some theory is not complete).
• For a complete (and model complete!) example, the theory of real closed fields (in the language $\{0,1,+,\cdot\}$) does not have q.e., because if we take some two algebraically independent real numbers $a,b$, then their atomic diagram will always be the same, but one is bigger than the other ($(\exists x) a+x^2=b$ or $(\exists x) b+x^2=a$), so we can't decide which.