Theorem sqrtcvallem3

Description: Equivalent to saying that the absolute value of the imaginary component of the square root of a complex number is a real number. Lemma for sqrtcval , sqrtcval2 , resqrtval , and imsqrtval . (Contributed by RP, 11-May-2024)

	Ref	Expression
Assertion	sqrtcvallem3	$$⊢A\in ℂ\to \sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
2		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
3	1 2	resubcld	$$⊢A\in ℂ\to \left|A\right|-\Re \left(A\right)\in ℝ$$
4	3	rehalfcld	$$⊢A\in ℂ\to \frac{\left|A\right|-\Re \left(A\right)}{2}\in ℝ$$
5		sqrtcvallem2	$$⊢A\in ℂ\to 0\le \frac{\left|A\right|-\Re \left(A\right)}{2}$$
6	4 5	resqrtcld	$$⊢A\in ℂ\to \sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}\in ℝ$$