Showing that formulae which are provably $Σ_n$ and $Π_n$ ($n > 0$) in the arithmetical hierarchy are closed under $∃$ and $∀$ respectively As the title explains, I'm trying to solve the following problem:

Show that for $n > 0$, formulae provably $Σ_n$ with respect to PA are closed under existential
quantification, and formulae provably $Π_n$ with respect to PA are closed under universal
quantification

(where $Π_n$ and $Σ_n$ are in the arithmetical hierarchy).
I assume this is done using induction, and I've done the base cases using the fact that $$PA ⊢ (∃v_j ∃v_i F(v_i , v_j) ↔ ∃v_k (∃v_j ≤ v_k)(∃v_i ≤ v_k)F(v_i
, v_j )).$$
to show that if $\phi$ is provably $Σ_1$ then it's equivalent to some $\phi' = \exists v_1\psi$ where $\psi$ is $\Pi_0$, and since $(∃v_j ≤ v_k)$, $(∃v_i ≤ v_k)$ are bounded it follows that $(∃v_j ≤ v_k)(∃v_i ≤ v_k)\psi$ is $\Pi_0$ making $$∃v_3 (∃v_2 ≤ v_3)(∃v_1 ≤ v_3)\psi$$ be $Σ_1$ and the result following by equivalence of $\exists v_2\phi$ with $∃v_3 (∃v_2 ≤ v_3)(∃v_1 ≤ v_3)\psi$ (and doing similar for the case where $\phi$ is $\Pi_1$).
I'm stuck when I get to the inductive step though - if we take $\phi$ to be $Σ_{n+1}$ the same trick doesn't work because there's no guarantee (I don't think) that $(∃v_2 ≤ v_3)(∃v_1 ≤ v_3)\psi$ will be $Π_n$ since what made $(∃v_2 ≤ v_3)(∃v_1 ≤ v_3)\psi$ be $Π_0$ in the previous case was that $Π_0$ formulae are defined as those with only bounded quantifiers, so the same trick doesn't work.
I though about maybe proving both results together as a single induction, so that I could apply the inductive hypothesis to some manipulation of $\psi$ (call it $\psi'$) which is in $\Pi_n$ to obtain $\forall v_2 \phi'$ in $\Pi_n$ and try to manipulate that somehow to obtain $\exists v_2\exists v_1\psi$ as being $Σ_{n+1}$, but I don't know how I'd make that work.
Any advice would be greatly appreciated.
 A: You need to be a bit more subtle in using bounded quantifiers. Get greedy! Make your new variable do more work!

It's often easier to first work things out for a more expressive theory, and then "pull down" to the actual theory in question. This is such a case. Consider the following equivalence in the expanded language of arithmetic gotten by adding the "factor-counting function" $count(a,b)=\max\{n: a^n\vert b\}$ (we'll address the change-of-language later): $$\exists a\exists b\varphi(a,b)\quad\equiv\quad \exists u\varphi(count(2,u), count(3,u)).$$
Here $\varphi$ is any formula whatsoever - complexity considerations haven't entered the picture yet.
The idea here is that $u$ codes the pair $(a,b)$ and the "count" function decodes it appropriately: we'll want $u=2^a3^b$ (admittedly, $2^a3^bk$ for some $k$ not divisible by $2$ or $3$ would also do the job). For longer blocks of existential quantifiers we just use more primes, e.g. $$\exists a\exists b\exists c\psi(a,b,c)\quad\equiv\quad \exists u\psi(count(2,u), count(3,u), count(5,u)).$$
And of course universal quantifiers will play out the same way, e.g. $$\forall a\forall b\forall c\forall d\theta(a,b,c,d)\quad\equiv\quad\forall u\theta(count(2,u), count(3,u), count(5,u), count(7,u)).$$

Now let's go back to the complexity issue. Note that all the above worked regardless of the complexity of the formula after the displayed quantifiers ($\varphi,\psi,\theta$ respectively). We can see the real power of this approach when we look at mixed quantifiers: the sentence $$\color{green}{\exists a\exists b}\color{red}{\forall c\forall d\forall k}\color{blue}{\exists l\exists m}\chi(\color{green}{a,b},\color{red}{c,d,k},\color{blue}{l,m})$$ is provably equivalent to $$\color{green}{\exists u}\color{red}{\forall v}\color{blue}{\exists w}\chi(\color{green}{count(2,u), count(3,u)}, \color{red}{count(2,v), count(3,v), count(5,v),}\color{blue}{count(2, w), count(3,w)}).$$
(Colors! Muahahaha! I've gone mad with power!)
Via coding finite tuples as individual numbers - which is a trick we use constantly - we've condensed all the homogeneous quantifier blocks at once.

OK, now there's just one issue left: change of language. The above establishes (once some appropriate verification has been performed) the desired result for an extension of Peano arithmetic. But what about $\mathsf{PA}$ itself?
Here we need a "low-complexity definability" result:

There is a $\Pi_0$ formula $\zeta(x,y,z)$ defining the graph of $code$ in $\mathbb{N}$; that is, such that $$\zeta^\mathbb{N}=\{(x,y,z): code(x,y)=z\}.$$

We then use this formula to "simulate" the function symbol $code$ by appropriate introduction of new variables, e.g. $$\exists a\exists b\varphi(a,b)\quad\equiv\quad\exists u\forall a<u\forall b<u(\zeta(2,u,a)\wedge\zeta(3,u,b)\rightarrow \varphi(a,b))$$ (note that those $\forall$s could be $\exists$ if that would be preferred).
