Metamath Proof Explorer

Theorem resqrtval

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

Ref Expression
Assertion resqrtval ( 𝐴 ∈ ℂ → ( ℜ ‘ ( √ ‘ 𝐴 ) ) = ( √ ‘ ( ( ( 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 crred ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( ( √ ‘ ( ( ( abs ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) / 2 ) ) + ( i · ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) ) ) ) = ( √ ‘ ( ( ( abs ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) / 2 ) ) )
11 2 10 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( √ ‘ 𝐴 ) ) = ( √ ‘ ( ( ( abs ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) / 2 ) ) )