Theorem imsqrtval

Description: Imaginary part of the complex square root. (Contributed by RP, 18-May-2024)

	Ref	Expression
Assertion	imsqrtval	$$⊢A\in ℂ\to \Im \left(\sqrt{A}\right)=if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}$$

Proof

Step	Hyp	Ref	Expression
1		sqrtcval	$$⊢A\in ℂ\to \sqrt{A}=\sqrt{\frac{\left|A\right|+\Re \left(A\right)}{2}}+\mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}$$
2	1	fveq2d	$$⊢A\in ℂ\to \Im \left(\sqrt{A}\right)=\Im \left(\sqrt{\frac{\left|A\right|+\Re \left(A\right)}{2}}+\mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}\right)$$
3		sqrtcvallem5	$$⊢A\in ℂ\to \sqrt{\frac{\left|A\right|+\Re \left(A\right)}{2}}\in ℝ$$
4		neg1rr	$$⊢-1\in ℝ$$
5		1re	$$⊢1\in ℝ$$
6	4 5	ifcli	$$⊢if\left(\Im \left(A\right)<0,-1,1\right)\in ℝ$$
7	6	a1i	$$⊢A\in ℂ\to if\left(\Im \left(A\right)<0,-1,1\right)\in ℝ$$
8		sqrtcvallem3	$$⊢A\in ℂ\to \sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}\in ℝ$$
9	7 8	remulcld	$$⊢A\in ℂ\to if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}\in ℝ$$
10	3 9	crimd	$$⊢A\in ℂ\to \Im \left(\sqrt{\frac{\left|A\right|+\Re \left(A\right)}{2}}+\mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}\right)=if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}$$
11	2 10	eqtrd	$$⊢A\in ℂ\to \Im \left(\sqrt{A}\right)=if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}$$