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 A 0 A + A 2

Proof

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