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 
|- ( A e. CC -> ( sqrt ` A ) = ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( if ( ( Im ` A ) < 0 , -u _i , _i ) 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 ovif2 
 |-  ( _i x. if ( ( Im ` A ) < 0 , -u 1 , 1 ) ) = if ( ( Im ` A ) < 0 , ( _i x. -u 1 ) , ( _i x. 1 ) )
3 neg1cn 
 |-  -u 1 e. CC
4 ax-icn 
 |-  _i e. CC
5 4 mulm1i 
 |-  ( -u 1 x. _i ) = -u _i
6 3 4 5 mulcomli 
 |-  ( _i x. -u 1 ) = -u _i
7 4 mulridi 
 |-  ( _i x. 1 ) = _i
8 ifeq12 
 |-  ( ( ( _i x. -u 1 ) = -u _i /\ ( _i x. 1 ) = _i ) -> if ( ( Im ` A ) < 0 , ( _i x. -u 1 ) , ( _i x. 1 ) ) = if ( ( Im ` A ) < 0 , -u _i , _i ) )
9 6 7 8 mp2an 
 |-  if ( ( Im ` A ) < 0 , ( _i x. -u 1 ) , ( _i x. 1 ) ) = if ( ( Im ` A ) < 0 , -u _i , _i )
10 2 9 eqtr2i 
 |-  if ( ( Im ` A ) < 0 , -u _i , _i ) = ( _i x. if ( ( Im ` A ) < 0 , -u 1 , 1 ) )
11 10 a1i 
 |-  ( A e. CC -> if ( ( Im ` A ) < 0 , -u _i , _i ) = ( _i x. if ( ( Im ` A ) < 0 , -u 1 , 1 ) ) )
12 11 oveq1d 
 |-  ( A e. CC -> ( if ( ( Im ` A ) < 0 , -u _i , _i ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) = ( ( _i x. if ( ( Im ` A ) < 0 , -u 1 , 1 ) ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) )
13 4 a1i 
 |-  ( A e. CC -> _i e. CC )
14 neg1rr 
 |-  -u 1 e. RR
15 1re 
 |-  1 e. RR
16 14 15 ifcli 
 |-  if ( ( Im ` A ) < 0 , -u 1 , 1 ) e. RR
17 16 a1i 
 |-  ( A e. CC -> if ( ( Im ` A ) < 0 , -u 1 , 1 ) e. RR )
18 17 recnd 
 |-  ( A e. CC -> if ( ( Im ` A ) < 0 , -u 1 , 1 ) e. CC )
19 sqrtcvallem3 
 |-  ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) e. RR )
20 19 recnd 
 |-  ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) e. CC )
21 13 18 20 mulassd 
 |-  ( A e. CC -> ( ( _i x. if ( ( Im ` A ) < 0 , -u 1 , 1 ) ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) = ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) )
22 12 21 eqtrd 
 |-  ( A e. CC -> ( if ( ( Im ` A ) < 0 , -u _i , _i ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) = ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) )
23 22 oveq2d 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( if ( ( Im ` A ) < 0 , -u _i , _i ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) = ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) )
24 1 23 eqtr4d 
 |-  ( A e. CC -> ( sqrt ` A ) = ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( if ( ( Im ` A ) < 0 , -u _i , _i ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) )