Metamath Proof Explorer


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 A0A+A2

Proof

Step Hyp Ref Expression
1 abscl AA
2 recl AA
3 1 2 readdcld AA+A
4 2rp 2+
5 4 a1i A2+
6 negcl AA
7 6 releabsd AAA
8 6 abscld AA
9 6 recld AA
10 8 9 subge0d A0AAAA
11 7 10 mpbird A0AA
12 absneg AA=A
13 reneg AA=A
14 12 13 oveq12d AAA=AA
15 1 recnd AA
16 2 recnd AA
17 15 16 subnegd AAA=A+A
18 14 17 eqtrd AAA=A+A
19 11 18 breqtrd A0A+A
20 3 5 19 divge0d A0A+A2