Metamath Proof Explorer

Theorem imsqrtval

Description: Imaginary part of the complex square root. (Contributed by RP, 18-May-2024)

Ref Expression
Assertion imsqrtval 
|- ( A e. CC -> ( Im ` ( sqrt ` A ) ) = ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 sqrtcval 
 |-  ( A e. CC -> ( sqrt ` A ) = ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) )
2 1 fveq2d 
 |-  ( A e. CC -> ( Im ` ( sqrt ` A ) ) = ( Im ` ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) )
3 sqrtcvallem5 
 |-  ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) e. RR )
4 neg1rr 
 |-  -u 1 e. RR
5 1re 
 |-  1 e. RR
6 4 5 ifcli 
 |-  if ( ( Im ` A ) < 0 , -u 1 , 1 ) e. RR
7 6 a1i 
 |-  ( A e. CC -> if ( ( Im ` A ) < 0 , -u 1 , 1 ) e. RR )
8 sqrtcvallem3 
 |-  ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) e. RR )
9 7 8 remulcld 
 |-  ( A e. CC -> ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) e. RR )
10 3 9 crimd 
 |-  ( A e. CC -> ( Im ` ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) = ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) )
11 2 10 eqtrd 
 |-  ( A e. CC -> ( Im ` ( sqrt ` A ) ) = ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) )