Theorem sqrtcvallem4

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

	Ref	Expression
Assertion	sqrtcvallem4	$$⊢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	readdcld	$$⊢A\in ℂ\to \left|A\right|+\Re \left(A\right)\in ℝ$$
4		2rp	$$⊢2\in {ℝ}^{+}$$
5	4	a1i	$$⊢A\in ℂ\to 2\in {ℝ}^{+}$$
6		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
7	6	releabsd	$$⊢A\in ℂ\to \Re \left(-A\right)\le \left|-A\right|$$
8	6	abscld	$$⊢A\in ℂ\to \left|-A\right|\in ℝ$$
9	6	recld	$$⊢A\in ℂ\to \Re \left(-A\right)\in ℝ$$
10	8 9	subge0d	$$⊢A\in ℂ\to \left(0\le \left|-A\right|-\Re \left(-A\right)\leftrightarrow \Re \left(-A\right)\le \left|-A\right|\right)$$
11	7 10	mpbird	$$⊢A\in ℂ\to 0\le \left|-A\right|-\Re \left(-A\right)$$
12		absneg	$$⊢A\in ℂ\to \left|-A\right|=\left|A\right|$$
13		reneg	$$⊢A\in ℂ\to \Re \left(-A\right)=-\Re \left(A\right)$$
14	12 13	oveq12d	$$⊢A\in ℂ\to \left|-A\right|-\Re \left(-A\right)=\left|A\right|-\left(-\Re \left(A\right)\right)$$
15	1	recnd	$$⊢A\in ℂ\to \left|A\right|\in ℂ$$
16	2	recnd	$$⊢A\in ℂ\to \Re \left(A\right)\in ℂ$$
17	15 16	subnegd	$$⊢A\in ℂ\to \left|A\right|-\left(-\Re \left(A\right)\right)=\left|A\right|+\Re \left(A\right)$$
18	14 17	eqtrd	$$⊢A\in ℂ\to \left|-A\right|-\Re \left(-A\right)=\left|A\right|+\Re \left(A\right)$$
19	11 18	breqtrd	$$⊢A\in ℂ\to 0\le \left|A\right|+\Re \left(A\right)$$
20	3 5 19	divge0d	$$⊢A\in ℂ\to 0\le \frac{\left|A\right|+\Re \left(A\right)}{2}$$