here are some basic distributive properties in quantifiers, hope it might help someone.
∀x(P(x) ∧ Q(x)) ≡ (∀xP(x) ∧ ∀xQ(x))
∃x(P(x) ∧ Q(x)) → (∃xP(x) ∧ ∃xQ(x))
∀x(P(x) ∨ Q(x)) ← (∀xP(x) ∨ ∀xQ(x))
∃x(P(x) ∨ Q(x)) ≡ (∃xP(x) ∨ ∃xQ(x))
∀x(P(x) → Q(x)) ← (∃xP(x) → ∀xQ(x))
∃x(P(x) → Q(x)) ≡ (∀xP(x) → ∃xQ(x))
∀x¬P(x) ≡ ¬∃xP(x)
∃x¬P(x) ≡ ¬∀xP(x)
∀x∃yT(x,y) ← ∃y∀xT(x,y)
∀x∀yT(x,y) ≡ ∀y∀xT(x,y)
∃x∃yT(x,y) ≡ ∃y∃xT(x,y)
∀x(P(x) ∨ R) ≡ (∀xP(x) ∨ R)
∃x(P(x) ∧ R) ≡ (∃xP(x) ∧ R)
∀x(P(x) → R) ≡ (∃xP(x) → R)
∃x(P(x) → R) → (∀xP(x) → R)
∀x(R → Q(x)) ≡ (R → ∀xQ(x))
∃x(R → Q(x)) → (R → ∃xQ(x))
∀xR ← R
∃xR → R
The following formulas are not valid.
A B counterexample
∃x(P(x) ∧ Q(x)) ← (∃xP(x) ∧ ∃xQ(x)) D = {a, b}, M = {P(a), Q(b)}
∀x(P(x) ∨ Q(x)) → (∀xP(x) ∨ ∀xQ(x)) D = {a, b}, M = {P(a), Q(b)}
∀x(P(x) → Q(x)) → (∃xP(x) → ∀xQ(x)) D = {a, b}, M = {P(a), Q(a)}
∀x∃yT(x,y) → ∃y∀xT(x,y) D = {a, b}, M = {T(a,b), T(b,a)}
∃x(P(x) → R) ← (∀xP(x) → R) D = Ø, M = {R}
∃x(R → Q(x)) ← (R → ∃xQ(x)) D = Ø, M = Ø
∀xR → R D = Ø, M = Ø
∃xR ← R D = Ø, M = {R}
Note: if empty domains are not allowed, then the last four implications are in fact valid.
When you negate a quantifier, you 'bring the negation inside', e.g. $\neg \forall x P(x)$ is equivalent to $\exists x \: \neg P(x)$, where P(x) is some claim about $x$.
If you have two quantifiers, that still works the same way, e.g. $\neg \forall x \exists y P(x,y)$ is equivalent to $\exists x \neg \exists y P(x,y)$, which in turn is equivalent to $\exists x \forall y \neg P(x,y)$. And once you see that, you can understand that you can move a negation through a series of any number of quantifiers, as long as you change the quantifier: each $\forall$ becomes a $\exists$ and vice versa.
Also, since these are all equivalences, you can also bring negations outside, if that's what you ever wanted to, again as long as you change each quantifier that you move the negation through. For this reason, this is sometimes called the 'dagger rule': you can 'stab' a dagger (the negation) all the way through a quantifier, thereby changing the quantifier.
Best Answer
The logical form of your first statement is
$$\tag{1} \forall n \in \mathbb{Z} \, \exists k \in \mathbb{N} ((n \mid 12k+5 \wedge n \mid 18k+1) \implies n=17)$$
The contrapositive of such a formula (obtained by reversing the arrow and negating its antecedent and consequent) is
$$\tag{2}\forall n \in \mathbb{Z} \, \exists k \in \mathbb{N} (n \neq 17 \implies (n\not \mid 12k+5 \lor n \not\mid 18k+1))$$
which is logically equivalent to
$$\tag{3}\forall n \in \mathbb{Z} (n \neq 17 \implies \exists k \in \mathbb{N} (n\not \mid 12k+5 \lor n \not\mid 18k+1))$$
Note that both your proposals for the contrapositive are wrong, because they are not logically equivalent to $(2)$ or $(3)$. In your last formula you use $\land$ instead of $\lor$, and in your previous formula you use $\forall$ instead of $\exists$.
Another way to see this is considering the following formula, which is logically equivalent to $(1)$
$$\forall n \in \mathbb{Z} (\forall k \in \mathbb{N} (n \mid 12k+5 \wedge n \mid 18k+1) \implies n=17)$$
The contrapositive of such a formula (obtained by reversing the arrow and negating its antecedent and consequent) is exactly $(3)$.
The logical equivalences used above are: \begin{align} P \to Q &\equiv \lnot Q \to \lnot P &&\text{(contrapositive)} \\ \lnot (P \land Q) &\equiv \lnot P \lor \lnot Q &&\text{(De Morgan)} \\ \exists x (P \to Q) &\equiv (\forall x P) \to Q &&\text{(contravariance of the antecedent)} \\ \exists x (Q \to P) &\equiv Q \to (\exists x P) &&\text{(covariance of the consequent)} \end{align} where, in the last two equivalences, $x$ does not occur free in $Q$.