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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abscl | |
|
2 | recl | |
|
3 | 1 2 | readdcld | |
4 | 2rp | |
|
5 | 4 | a1i | |
6 | negcl | |
|
7 | 6 | releabsd | |
8 | 6 | abscld | |
9 | 6 | recld | |
10 | 8 9 | subge0d | |
11 | 7 10 | mpbird | |
12 | absneg | |
|
13 | reneg | |
|
14 | 12 13 | oveq12d | |
15 | 1 | recnd | |
16 | 2 | recnd | |
17 | 15 16 | subnegd | |
18 | 14 17 | eqtrd | |
19 | 11 18 | breqtrd | |
20 | 3 5 19 | divge0d | |