Metamath Proof Explorer


Theorem sqrtcl

Description: Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 10-Jul-2013)

Ref Expression
Assertion sqrtcl AA

Proof

Step Hyp Ref Expression
1 sqrtval AA=ιx|x2=A0xix+
2 sqreu A∃!xx2=A0xix+
3 riotacl ∃!xx2=A0xix+ιx|x2=A0xix+
4 2 3 syl Aιx|x2=A0xix+
5 1 4 eqeltrd AA