I am reading about the Gödel-Rosser Theorem, i.e. the Rosser's refinement of first Gödel's incompleteness Theorem, which states that if $\mathbf{PA}$ is consistent then it is incomplete.
I am posting this question to understand a point in its proof as written in van Dalen "Logic and Structure" 4th Edition.
Just the Foreground (Please, feel free to skip it).
Rosser's trick amounts to consider the wff $\mathscr{R}(x)$ defined by $\forall y[\overline{\mathrm{Neg}}(x,y)\to\forall z(\overline{\mathrm{Prov}}(z,y)\to\exists w< z\overline{\mathrm{Prov}}(w,x)],$ where
the formula $\overline{\mathrm{Neg}}(x,y)$ represents the numeric function $f$ defined by $f(m)=n$ iff there exists a wff $\phi$ such that $m$ and $n$ are the Gödel numers of $\phi$ and $\neg\phi$ respectively; and
the formula $\overline{\mathrm{Prov}}(z,y)$ represents the numeric relation $R$ such that $(m,n)\in R$ iff there exists a wff $\phi,$ whose Gödel number is $n,$ while $m$ is the Gödel number of a deduction of $\phi.$
Applying the Fixed Point Theorem, we find a sentence $\psi$ such that $\vdash\psi\leftrightarrow\neg\mathscr R(\overline{g(\psi)}),$ where we are denoting the Godel numbering with $g,$ and the $n$-th ordinal as $\overline{n}.$
Gödel-Rosser Theorem: If $\mathbf{PA}$ is consistent then $\psi$ is indecidible, therefore $\mathbf{PA}$ is incomplete.
My Question about the Proof
In the step "if $\vdash\psi$ then $\mathbf{PA}$ is inconsistent" (see snapshot below), after having written the assumption as $\vdash\overline{Prov}(\overline{n},\overline{g(\psi)}),$ for some natural number $n,$ I think that we should distinguish between the following two cases: $\vdash\neg\overline{Prov}(\overline{n},\overline{g(\psi)}),\tag{a}$ $\not\vdash\neg\overline{Prov}(\overline{n},\overline{g(\psi)}).\tag{b}$
My thoughts about
In the case $(a),$ we would get immediately the inconsistency of $\mathbf{PA},$ precisely $\overline{Prov}(\overline{n},\overline{g(\psi)})$ is indecidible.
In the case $(b),$ $\not\vdash\neg\overline{Prov}(\overline{n},\overline{g(\psi)})$ implies $\not\vdash\exists z>\overline{n}(\overline{Prov}(z,\overline{g(\neg\psi)})\wedge\forall w
Now by $(*)$, $\vdash\psi$ and $\vdash\psi\leftrightarrow\neg\mathscr R(\overline{g(\psi)}),$ we infer $\vdash\exists z\leq\overline{n}(\overline{Prov}(z,\overline{g(\neg\psi)})\wedge\forall w