Metamath Proof Explorer

Theorem sqrtcval2

Description: Explicit formula for the complex square root in terms of the square root of nonnegative reals. The right side is slightly more compact than sqrtcval . (Contributed by RP, 18-May-2024)

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

Proof

Step Hyp Ref Expression
1 sqrtcval ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) = ( ( √ ‘ ( ( ( abs ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) / 2 ) ) + ( i · ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) ) ) )
2 ovif2 ⊢ ( i · if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) ) = if ( ( ℑ ‘ 𝐴 ) < 0 , ( i · - 1 ) , ( i · 1 ) )
3 neg1cn ⊢ - 1 ∈ ℂ
4 ax-icn ⊢ i ∈ ℂ
5 4 mulm1i ⊢ ( - 1 · i ) = - i
6 3 4 5 mulcomli ⊢ ( i · - 1 ) = - i
7 4 mulridi ⊢ ( i · 1 ) = i
8 ifeq12 ⊢ ( ( ( i · - 1 ) = - i ∧ ( i · 1 ) = i ) → if ( ( ℑ ‘ 𝐴 ) < 0 , ( i · - 1 ) , ( i · 1 ) ) = if ( ( ℑ ‘ 𝐴 ) < 0 , - i , i ) )
9 6 7 8 mp2an ⊢ if ( ( ℑ ‘ 𝐴 ) < 0 , ( i · - 1 ) , ( i · 1 ) ) = if ( ( ℑ ‘ 𝐴 ) < 0 , - i , i )
10 2 9 eqtr2i ⊢ if ( ( ℑ ‘ 𝐴 ) < 0 , - i , i ) = ( i · if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) )
11 10 a1i ⊢ ( 𝐴 ∈ ℂ → if ( ( ℑ ‘ 𝐴 ) < 0 , - i , i ) = ( i · if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) ) )
12 11 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( if ( ( ℑ ‘ 𝐴 ) < 0 , - i , i ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) = ( ( i · if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) )
13 4 a1i ⊢ ( 𝐴 ∈ ℂ → i ∈ ℂ )
14 neg1rr ⊢ - 1 ∈ ℝ
15 1re ⊢ 1 ∈ ℝ
16 14 15 ifcli ⊢ if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) ∈ ℝ
17 16 a1i ⊢ ( 𝐴 ∈ ℂ → if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) ∈ ℝ )
18 17 recnd ⊢ ( 𝐴 ∈ ℂ → if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) ∈ ℂ )
19 sqrtcvallem3 ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ∈ ℝ )
20 19 recnd ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ∈ ℂ )
21 13 18 20 mulassd ⊢ ( 𝐴 ∈ ℂ → ( ( i · if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) = ( i · ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) ) )
22 12 21 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( if ( ( ℑ ‘ 𝐴 ) < 0 , - i , i ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) = ( i · ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) ) )
23 22 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ ( ( ( abs ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) / 2 ) ) + ( if ( ( ℑ ‘ 𝐴 ) < 0 , - i , i ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) ) = ( ( √ ‘ ( ( ( abs ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) / 2 ) ) + ( i · ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) ) ) )
24 1 23 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) = ( ( √ ‘ ( ( ( abs ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) / 2 ) ) + ( if ( ( ℑ ‘ 𝐴 ) < 0 , - i , i ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) ) )