Description: Equivalent to saying that the absolute value of the imaginary component of the square root of a complex number is a real number. Lemma for sqrtcval , sqrtcval2 , resqrtval , and imsqrtval . (Contributed by RP, 11-May-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | sqrtcvallem3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abscl | ||
2 | recl | ||
3 | 1 2 | resubcld | |
4 | 3 | rehalfcld | |
5 | sqrtcvallem2 | ||
6 | 4 5 | resqrtcld |