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 | |- ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) e. RR ) |
| 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 | resubcld | |- ( A e. CC -> ( ( abs ` A ) - ( Re ` A ) ) e. RR ) |
| 4 | 3 | rehalfcld | |- ( A e. CC -> ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) e. RR ) |
| 5 | sqrtcvallem2 | |- ( A e. CC -> 0 <_ ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) |
|
| 6 | 4 5 | resqrtcld | |- ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) e. RR ) |