Theorem sqrtcl

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

	Ref	Expression
Assertion	sqrtcl	|- ( A e. CC -> ( sqrt ` A ) e. CC )

Proof

Step	Hyp	Ref	Expression
1		sqrtval	|- ( A e. CC -> ( sqrt ` A ) = ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
2		sqreu	|- ( A e. CC -> E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
3		riotacl	|- ( E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) -> ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) e. CC )
4	2 3	syl	|- ( A e. CC -> ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) e. CC )
5	1 4	eqeltrd	|- ( A e. CC -> ( sqrt ` A ) e. CC )