Metamath Proof Explorer


Theorem sqrtcvallem2

Description: Equivalent to saying that the square of the imaginary component of the square root of a complex number is a nonnegative real number. Lemma for sqrtcval . See imsqrtval . (Contributed by RP, 11-May-2024)

Ref Expression
Assertion sqrtcvallem2 A 0 A A 2

Proof

Step Hyp Ref Expression
1 abscl A A
2 recl A A
3 1 2 resubcld A A A
4 2rp 2 +
5 4 a1i A 2 +
6 releabs A A A
7 1 2 subge0d A 0 A A A A
8 6 7 mpbird A 0 A A
9 3 5 8 divge0d A 0 A A 2