Metamath Proof Explorer


Theorem sqrtcvallem3

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

Proof

Step Hyp Ref Expression
1 abscl A A
2 recl A A
3 1 2 resubcld A A A
4 3 rehalfcld A A A 2
5 sqrtcvallem2 A 0 A A 2
6 4 5 resqrtcld A A A 2