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 ) ) ) )