Theorem sqrtcvallem5

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

	Ref	Expression
Assertion	sqrtcvallem5	$$⊢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	readdcld	$$⊢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		sqrtcvallem4	$$⊢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 ℝ$$