Description: Equivalent to saying that the real component of the square root of a complex number is a real number. Lemma for resqrtval and imsqrtval . (Contributed by RP, 11-May-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sqrtcvallem5 | |- ( 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 | readdcld | |- ( A e. CC -> ( ( abs ` A ) + ( Re ` A ) ) e. RR ) |
| 4 | 3 | rehalfcld | |- ( A e. CC -> ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) e. RR ) |
| 5 | sqrtcvallem4 | |- ( A e. CC -> 0 <_ ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) |
|
| 6 | 4 5 | resqrtcld | |- ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) e. RR ) |