Metamath Proof Explorer


Theorem imsqrtval

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

Ref Expression
Assertion imsqrtval ( 𝐴 ∈ ℂ → ( ℑ ‘ ( √ ‘ 𝐴 ) ) = ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 sqrtcval ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) = ( ( √ ‘ ( ( ( abs ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) / 2 ) ) + ( i · ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) ) ) )
2 1 fveq2d ( 𝐴 ∈ ℂ → ( ℑ ‘ ( √ ‘ 𝐴 ) ) = ( ℑ ‘ ( ( √ ‘ ( ( ( abs ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) / 2 ) ) + ( i · ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) ) ) ) )
3 sqrtcvallem5 ( 𝐴 ∈ ℂ → ( √ ‘ ( ( ( abs ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) / 2 ) ) ∈ ℝ )
4 neg1rr - 1 ∈ ℝ
5 1re 1 ∈ ℝ
6 4 5 ifcli if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) ∈ ℝ
7 6 a1i ( 𝐴 ∈ ℂ → if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) ∈ ℝ )
8 sqrtcvallem3 ( 𝐴 ∈ ℂ → ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ∈ ℝ )
9 7 8 remulcld ( 𝐴 ∈ ℂ → ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) ∈ ℝ )
10 3 9 crimd ( 𝐴 ∈ ℂ → ( ℑ ‘ ( ( √ ‘ ( ( ( abs ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) / 2 ) ) + ( i · ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) ) ) ) = ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) )
11 2 10 eqtrd ( 𝐴 ∈ ℂ → ( ℑ ‘ ( √ ‘ 𝐴 ) ) = ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) )