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 e. CC -> 0 <_ ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		abscl	|- ( A e. CC -> ( abs ` A ) e. RR )
2		recl	|- ( A e. CC -> ( Re ` A ) e. RR )
3	1 2	readdcld	|- ( A e. CC -> ( ( abs ` A ) + ( Re ` A ) ) e. RR )
4		2rp	|- 2 e. RR+
5	4	a1i	|- ( A e. CC -> 2 e. RR+ )
6		negcl	|- ( A e. CC -> -u A e. CC )
7	6	releabsd	|- ( A e. CC -> ( Re ` -u A ) <_ ( abs ` -u A ) )
8	6	abscld	|- ( A e. CC -> ( abs ` -u A ) e. RR )
9	6	recld	|- ( A e. CC -> ( Re ` -u A ) e. RR )
10	8 9	subge0d	|- ( A e. CC -> ( 0 <_ ( ( abs ` -u A ) - ( Re ` -u A ) ) <-> ( Re ` -u A ) <_ ( abs ` -u A ) ) )
11	7 10	mpbird	|- ( A e. CC -> 0 <_ ( ( abs ` -u A ) - ( Re ` -u A ) ) )
12		absneg	|- ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )
13		reneg	|- ( A e. CC -> ( Re ` -u A ) = -u ( Re ` A ) )
14	12 13	oveq12d	|- ( A e. CC -> ( ( abs ` -u A ) - ( Re ` -u A ) ) = ( ( abs ` A ) - -u ( Re ` A ) ) )
15	1	recnd	|- ( A e. CC -> ( abs ` A ) e. CC )
16	2	recnd	|- ( A e. CC -> ( Re ` A ) e. CC )
17	15 16	subnegd	|- ( A e. CC -> ( ( abs ` A ) - -u ( Re ` A ) ) = ( ( abs ` A ) + ( Re ` A ) ) )
18	14 17	eqtrd	|- ( A e. CC -> ( ( abs ` -u A ) - ( Re ` -u A ) ) = ( ( abs ` A ) + ( Re ` A ) ) )
19	11 18	breqtrd	|- ( A e. CC -> 0 <_ ( ( abs ` A ) + ( Re ` A ) ) )
20	3 5 19	divge0d	|- ( A e. CC -> 0 <_ ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) )