# [PVS-Help] real square roots and complex numbers

``` Dear all, I'm trying to re-prove the algebraic formula for square roots
of complex numbers given, e.g., here
http://en.wikipedia.org/wiki/Square_root#Square_roots_of_negative_and_complex_numbers

I'm getting stuck with silly things for example PVS not accepting a
trivial identity such as

[-1]  w!1`2 > 0
|-------
[1]   (w!1`1 + r!1) / 2 - (r!1 - w!1`1) / 2 = w!1`1

unless I do (name-replace "x!1" "w!1`1").

Normally, I would have thought that a proof of the "lemma" below should
be automatic once the right hints are installed which is why I'm asking
you for help :-)

Looking forward, Martin

sqrt: THEORY
BEGIN
sqrt : [nnreal -> nnreal]
sqrt_ax : AXIOM FORALL(x:nnreal):sqrt(x)*sqrt(x) = x
% more axioms needed ???

CC : TYPE = [real,real]
CCtimes(w,z:CC) : CC = (w`1*z`1 - w`2*z`2, w`1*z`2+w`2*z`1)
CCsqrt(w:CC) : CC = LET r=sqrt(w`1*w`1+w`2*w`2) IN
LET  sign = IF w`2 > 0 THEN 1 ELSE -1 ENDIF
IN
(sqrt((r+w`1)/2),sign*sqrt((r-w`1)/2))
lemma : LEMMA FORALL(w:CC):CCtimes(CCsqrt(w),CCsqrt(w))=w
END sqrt

```