complex analysis - Showing $iz+sqrt{1-z^2}$ has positive real part

Claim: for all $z\in\Bbb C$, $\Re[iz+\sqrt{1-z^2}]\ge0$.

Note that this square root function has its branch cut defined to take the square root with positive real part when one is available, or nonnegative imaginary part if both solutions are pure imaginary. The claim is false on the other branch, so this is important.

This problem comes up in the course of finding basic properties of the arcsin function via its definition in terms of $\log$, namely $\arcsin z=-i\log(iz+\sqrt{1-z^2})$, and it was verified "by inspection" in Mathematica by graphing it. The problem is of course reducible to $\Re[\sqrt{1-z^2}]\ge\Im[z]$ or $\Re[\sqrt{1-(x+iy)^2}]\ge y$ (switching $z\mapsto -z$ to get rid of the extra sign), but beyond this requires more detailed information on the behavior of the complex square root function.

If $1-z^2$ is a nonpositive real, then $z=x$ for some real $|x|\ge1$, in which case the expression reduces to $0\ge0$, because $\Im[z]=0$ and $\sqrt{1-x^2}$ is pure imaginary. Otherwise, we can use the following expansion for $\sqrt z$, which is valid when $|z|\ne-z$, i.e. $z$ is not a nonpositive real:

$$\sqrt z=\sqrt{|z|}\frac{|z|+z}{||z|+z|}.$$

Plugging in $z=1-(x+iy)^2$ to this expression, we get $$\Re[\sqrt{1-(x+iy)^2}]=\frac{\sqrt{\alpha}(\alpha+x)}{\sqrt{1+2\alpha x-x^2+x^4+3y^2+2x^2y^2+y^4}},$$

where $\alpha=\sqrt{(2xy)^2+(1-x^2+y^2)^2}$, and this expansion includes only square roots of positive real numbers. Then the claim is that this expression is greater than $-y$. I'll stop here, since the algebra only gets worse from here and I'm not certain I haven't made the original expression unnecessarily complicated. What is a nice way to derive the Claim?

---

More solution progress: We can assume that $x,y\ge0$, because the stronger equation $\Re[\sqrt{1-(x+iy)^2}]\ge|y|$ (with $|y|$ replacing $y$) is symmetric with respect to both $x\mapsto -x$ and $y\mapsto -y$, and reduces to the original equation when $y\ge0$. (To see the $x,y$ symmetries, note that $\Re[\sqrt{1-z^2}]=\Re[\sqrt{1-(-z)^2}]$, and we also have $\Re[\sqrt{1-\bar z^2}]=\Re[\overline{\sqrt{1-z^2}}]=\Re[\sqrt{1-z^2}]$ assuming $1-z^2$ is not a nonpositive real, which we have already dealt with above.)

Then since all the terms are manifestly nonnegative (except possibly the $-x^2$ term in the denominator, but this is not a problem since $1-x^2+x^4\ge0$) we can feel free to cross-multiply and square:

$$\frac{\sqrt{\alpha}(\alpha+x)}{\sqrt{1+2\alpha x-x^2+x^4+3y^2+2x^2y^2+y^4}}\ge y\iff$$
$$\sqrt{\alpha}(\alpha+x)\ge y\sqrt{1+2\alpha x-x^2+x^4+3y^2+2x^2y^2+y^4}\iff$$

$$\alpha^3+2\alpha^2 x+\alpha x^2\ge y^2(1+2\alpha x-x^2+x^4+3y^2+2x^2y^2+y^4)\iff$$
$$\overbrace{2x^5 - x^4y^2 + 4x^3 (y^2-1) + 2 x (y^2+1)^2 +
x^2 (y^2-2y^4) - y^2 (y^4+3y^2+1)}^u +
\alpha \overbrace{(x^4 - 2 x y^2 + (1 + y^2)^2 + x^2 (2 y^2-1))}^v\ge0$$

Now at this stage, I would like to rewrite the equation as $u\ge -\alpha v$ so I can square it, but unfortunately the terms are not nonnegative any longer. However, $v\ge0$ appears to hold for all $x,y\ge0$ (proof by graphing), so it suffices to prove $u^2\le\alpha^2v^2$ for all $u\le0$:

$$u^2\le((2xy)^2+(1-x^2+y^2)^2)v^2\iff$$
$$1 + x^{12} + 6 y^2 + 2 x^9 y^2 + 14 y^4 + 14 y^6 + 4 y^8 +
x^{10} (-9 + 6 y^2) +\\ 2 x (y + y^3)^2 (1 + 4 y^2 + y^4) +

x^7 (-4 y^2 + 8 y^4) + x^8 (27 - 30 y^2 + 14 y^4) +\\
4 x^3 y^2 (-1 - 2 y^2 + 5 y^4 + 2 y^6) + 4 x^5 (y^2 + y^4 + 3 y^6) +
2 x^6 (-19 + 12 y^2 - 14 y^4 + 8 y^6) +\\
x^4 (27 + 24 y^2 - 21 y^4 - 2 y^6 + 9 y^8) +
x^2 (-9 - 30 y^2 - 28 y^4 + 2 y^6 + 5 y^8 + 2 y^{10})\ge0$$
$$\mbox{when}\quad 2x^5 - x^4y^2 + 4x^3 (y^2-1) + 2 x (y^2+1)^2 +
x^2 (y^2-2y^4) - y^2 (y^4+3y^2+1)\le0.$$

Now it is finally a pure polynomial inequality. However, it is now a total mess, considering that the original problem doesn't seem like it should get this ugly, and this is some kind of polynomial optimization problem that I have no idea how to solve.

Answer

So there is no problem if $y$ is negative. For positive $y$, apply the binomial theorem to see
$$
\sqrt{1-z^2}+iz=\frac{(1-z^2)-(iz)^2}{\sqrt{1-z^2}-iz}=\frac1{\sqrt{1-z^2}+y-ix}
$$
and since inversion of numbers with positive real part gives again numbers with positive real part, also this case is done. The case $y=0$ is trivial.