Metamath Proof Explorer

Theorem sqrtval

Description: Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013)

Ref Expression
Assertion sqrtval 
|- ( A e. CC -> ( sqrt ` A ) = ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )

Proof

Step Hyp Ref Expression
1 eqeq2 
 |-  ( y = A -> ( ( x ^ 2 ) = y <-> ( x ^ 2 ) = A ) )
2 1 3anbi1d 
 |-  ( y = A -> ( ( ( x ^ 2 ) = y /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) <-> ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
3 2 riotabidv 
 |-  ( y = A -> ( iota_ x e. CC ( ( x ^ 2 ) = y /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) = ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
4 df-sqrt 
 |-  sqrt = ( y e. CC |-> ( iota_ x e. CC ( ( x ^ 2 ) = y /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
5 riotaex 
 |-  ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) e. _V
6 3 4 5 fvmpt 
 |-  ( A e. CC -> ( sqrt ` A ) = ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )