Theorem sqrtcvallem2

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

	Ref	Expression
Assertion	sqrtcvallem2	$$⊢A\in ℂ\to 0\le \frac{\left|A\right|-\Re \left(A\right)}{2}$$

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		2rp	$$⊢2\in {ℝ}^{+}$$
5	4	a1i	$$⊢A\in ℂ\to 2\in {ℝ}^{+}$$
6		releabs	$$⊢A\in ℂ\to \Re \left(A\right)\le \left|A\right|$$
7	1 2	subge0d	$$⊢A\in ℂ\to \left(0\le \left|A\right|-\Re \left(A\right)\leftrightarrow \Re \left(A\right)\le \left|A\right|\right)$$
8	6 7	mpbird	$$⊢A\in ℂ\to 0\le \left|A\right|-\Re \left(A\right)$$
9	3 5 8	divge0d	$$⊢A\in ℂ\to 0\le \frac{\left|A\right|-\Re \left(A\right)}{2}$$