Metamath Proof Explorer

Theorem sqrtcval

Description: Explicit formula for the complex square root in terms of the square root of nonnegative reals. The right-hand side is decomposed into real and imaginary parts in the format expected by crrei and crimi . This formula can be found in section 3.7.27 of Handbook of Mathematical Functions, ed. M. Abramowitz and I. A. Stegun (1965, Dover Press). (Contributed by RP, 18-May-2024)

Ref Expression
Assertion 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sqrtcvallem5 
 |-  ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) e. RR )
2 1 recnd 
 |-  ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) e. CC )
3 ax-icn 
 |-  _i e. CC
4 3 a1i 
 |-  ( A e. CC -> _i e. CC )
5 neg1rr 
 |-  -u 1 e. RR
6 1re 
 |-  1 e. RR
7 5 6 ifcli 
 |-  if ( ( Im ` A ) < 0 , -u 1 , 1 ) e. RR
8 7 a1i 
 |-  ( A e. CC -> if ( ( Im ` A ) < 0 , -u 1 , 1 ) e. RR )
9 sqrtcvallem3 
 |-  ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) e. RR )
10 8 9 remulcld 
 |-  ( A e. CC -> ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) e. RR )
11 10 recnd 
 |-  ( A e. CC -> ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) e. CC )
12 4 11 mulcld 
 |-  ( A e. CC -> ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) e. CC )
13 2 12 addcld 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) e. CC )
14 id 
 |-  ( A e. CC -> A e. CC )
15 binom2 
 |-  ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) e. CC /\ ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) e. CC ) -> ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ^ 2 ) = ( ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ^ 2 ) + ( 2 x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( _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 ) ) ) ) ^ 2 ) ) )
16 2 12 15 syl2anc 
 |-  ( A e. CC -> ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ^ 2 ) = ( ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ^ 2 ) + ( 2 x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( _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 ) ) ) ) ^ 2 ) ) )
17 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
18 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
19 17 18 readdcld 
 |-  ( A e. CC -> ( ( abs ` A ) + ( Re ` A ) ) e. RR )
20 19 rehalfcld 
 |-  ( A e. CC -> ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) e. RR )
21 20 recnd 
 |-  ( A e. CC -> ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) e. CC )
22 21 sqsqrtd 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ^ 2 ) = ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) )
23 4 11 sqmuld 
 |-  ( A e. CC -> ( ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ^ 2 ) = ( ( _i ^ 2 ) x. ( ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ^ 2 ) ) )
24 i2 
 |-  ( _i ^ 2 ) = -u 1
25 24 a1i 
 |-  ( A e. CC -> ( _i ^ 2 ) = -u 1 )
26 8 recnd 
 |-  ( A e. CC -> if ( ( Im ` A ) < 0 , -u 1 , 1 ) e. CC )
27 9 recnd 
 |-  ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) e. CC )
28 26 27 sqmuld 
 |-  ( A e. CC -> ( ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ^ 2 ) = ( ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) ^ 2 ) x. ( ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ^ 2 ) ) )
29 ovif 
 |-  ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) ^ 2 ) = if ( ( Im ` A ) < 0 , ( -u 1 ^ 2 ) , ( 1 ^ 2 ) )
30 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
31 sq1 
 |-  ( 1 ^ 2 ) = 1
32 ifeq12 
 |-  ( ( ( -u 1 ^ 2 ) = 1 /\ ( 1 ^ 2 ) = 1 ) -> if ( ( Im ` A ) < 0 , ( -u 1 ^ 2 ) , ( 1 ^ 2 ) ) = if ( ( Im ` A ) < 0 , 1 , 1 ) )
33 30 31 32 mp2an 
 |-  if ( ( Im ` A ) < 0 , ( -u 1 ^ 2 ) , ( 1 ^ 2 ) ) = if ( ( Im ` A ) < 0 , 1 , 1 )
34 ifid 
 |-  if ( ( Im ` A ) < 0 , 1 , 1 ) = 1
35 29 33 34 3eqtri 
 |-  ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) ^ 2 ) = 1
36 35 a1i 
 |-  ( A e. CC -> ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) ^ 2 ) = 1 )
37 17 18 resubcld 
 |-  ( A e. CC -> ( ( abs ` A ) - ( Re ` A ) ) e. RR )
38 37 rehalfcld 
 |-  ( A e. CC -> ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) e. RR )
39 38 recnd 
 |-  ( A e. CC -> ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) e. CC )
40 39 sqsqrtd 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ^ 2 ) = ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) )
41 36 40 oveq12d 
 |-  ( A e. CC -> ( ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) ^ 2 ) x. ( ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ^ 2 ) ) = ( 1 x. ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) )
42 39 mulid2d 
 |-  ( A e. CC -> ( 1 x. ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) = ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) )
43 28 41 42 3eqtrd 
 |-  ( A e. CC -> ( ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ^ 2 ) = ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) )
44 25 43 oveq12d 
 |-  ( A e. CC -> ( ( _i ^ 2 ) x. ( ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ^ 2 ) ) = ( -u 1 x. ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) )
45 39 mulm1d 
 |-  ( A e. CC -> ( -u 1 x. ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) = -u ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) )
46 23 44 45 3eqtrd 
 |-  ( A e. CC -> ( ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ^ 2 ) = -u ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) )
47 22 46 oveq12d 
 |-  ( A e. CC -> ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ^ 2 ) + ( ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ^ 2 ) ) = ( ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) + -u ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) )
48 21 39 negsubd 
 |-  ( A e. CC -> ( ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) + -u ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) = ( ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) - ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) )
49 17 recnd 
 |-  ( A e. CC -> ( abs ` A ) e. CC )
50 18 recnd 
 |-  ( A e. CC -> ( Re ` A ) e. CC )
51 49 50 50 pnncand 
 |-  ( A e. CC -> ( ( ( abs ` A ) + ( Re ` A ) ) - ( ( abs ` A ) - ( Re ` A ) ) ) = ( ( Re ` A ) + ( Re ` A ) ) )
52 50 2timesd 
 |-  ( A e. CC -> ( 2 x. ( Re ` A ) ) = ( ( Re ` A ) + ( Re ` A ) ) )
53 51 52 eqtr4d 
 |-  ( A e. CC -> ( ( ( abs ` A ) + ( Re ` A ) ) - ( ( abs ` A ) - ( Re ` A ) ) ) = ( 2 x. ( Re ` A ) ) )
54 53 oveq1d 
 |-  ( A e. CC -> ( ( ( ( abs ` A ) + ( Re ` A ) ) - ( ( abs ` A ) - ( Re ` A ) ) ) / 2 ) = ( ( 2 x. ( Re ` A ) ) / 2 ) )
55 19 recnd 
 |-  ( A e. CC -> ( ( abs ` A ) + ( Re ` A ) ) e. CC )
56 37 recnd 
 |-  ( A e. CC -> ( ( abs ` A ) - ( Re ` A ) ) e. CC )
57 2cnd 
 |-  ( A e. CC -> 2 e. CC )
58 2ne0 
 |-  2 =/= 0
59 58 a1i 
 |-  ( A e. CC -> 2 =/= 0 )
60 55 56 57 59 divsubdird 
 |-  ( A e. CC -> ( ( ( ( abs ` A ) + ( Re ` A ) ) - ( ( abs ` A ) - ( Re ` A ) ) ) / 2 ) = ( ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) - ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) )
61 50 57 59 divcan3d 
 |-  ( A e. CC -> ( ( 2 x. ( Re ` A ) ) / 2 ) = ( Re ` A ) )
62 54 60 61 3eqtr3d 
 |-  ( A e. CC -> ( ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) - ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) = ( Re ` A ) )
63 47 48 62 3eqtrd 
 |-  ( A e. CC -> ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ^ 2 ) + ( ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ^ 2 ) ) = ( Re ` A ) )
64 57 2 mulcld 
 |-  ( A e. CC -> ( 2 x. ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ) e. CC )
65 64 4 11 mul12d 
 |-  ( A e. CC -> ( ( 2 x. ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ) x. ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) = ( _i x. ( ( 2 x. ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ) x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) )
66 57 2 12 mulassd 
 |-  ( A e. CC -> ( ( 2 x. ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ) x. ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) = ( 2 x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) )
67 57 2 11 mulassd 
 |-  ( A e. CC -> ( ( 2 x. ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ) x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) = ( 2 x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) )
68 2 26 27 mul12d 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) = ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) )
69 sqrtcvallem4 
 |-  ( A e. CC -> 0 <_ ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) )
70 halfnneg2 
 |-  ( ( ( abs ` A ) + ( Re ` A ) ) e. RR -> ( 0 <_ ( ( abs ` A ) + ( Re ` A ) ) <-> 0 <_ ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) )
71 19 70 syl 
 |-  ( A e. CC -> ( 0 <_ ( ( abs ` A ) + ( Re ` A ) ) <-> 0 <_ ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) )
72 69 71 mpbird 
 |-  ( A e. CC -> 0 <_ ( ( abs ` A ) + ( Re ` A ) ) )
73 2rp 
 |-  2 e. RR+
74 73 a1i 
 |-  ( A e. CC -> 2 e. RR+ )
75 19 72 74 sqrtdivd 
 |-  ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) = ( ( sqrt ` ( ( abs ` A ) + ( Re ` A ) ) ) / ( sqrt ` 2 ) ) )
76 sqrtcvallem2 
 |-  ( A e. CC -> 0 <_ ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) )
77 halfnneg2 
 |-  ( ( ( abs ` A ) - ( Re ` A ) ) e. RR -> ( 0 <_ ( ( abs ` A ) - ( Re ` A ) ) <-> 0 <_ ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) )
78 37 77 syl 
 |-  ( A e. CC -> ( 0 <_ ( ( abs ` A ) - ( Re ` A ) ) <-> 0 <_ ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) )
79 76 78 mpbird 
 |-  ( A e. CC -> 0 <_ ( ( abs ` A ) - ( Re ` A ) ) )
80 37 79 74 sqrtdivd 
 |-  ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) = ( ( sqrt ` ( ( abs ` A ) - ( Re ` A ) ) ) / ( sqrt ` 2 ) ) )
81 75 80 oveq12d 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) = ( ( ( sqrt ` ( ( abs ` A ) + ( Re ` A ) ) ) / ( sqrt ` 2 ) ) x. ( ( sqrt ` ( ( abs ` A ) - ( Re ` A ) ) ) / ( sqrt ` 2 ) ) ) )
82 19 72 resqrtcld 
 |-  ( A e. CC -> ( sqrt ` ( ( abs ` A ) + ( Re ` A ) ) ) e. RR )
83 82 recnd 
 |-  ( A e. CC -> ( sqrt ` ( ( abs ` A ) + ( Re ` A ) ) ) e. CC )
84 2re 
 |-  2 e. RR
85 84 a1i 
 |-  ( A e. CC -> 2 e. RR )
86 0le2 
 |-  0 <_ 2
87 86 a1i 
 |-  ( A e. CC -> 0 <_ 2 )
88 85 87 resqrtcld 
 |-  ( A e. CC -> ( sqrt ` 2 ) e. RR )
89 88 recnd 
 |-  ( A e. CC -> ( sqrt ` 2 ) e. CC )
90 37 79 resqrtcld 
 |-  ( A e. CC -> ( sqrt ` ( ( abs ` A ) - ( Re ` A ) ) ) e. RR )
91 90 recnd 
 |-  ( A e. CC -> ( sqrt ` ( ( abs ` A ) - ( Re ` A ) ) ) e. CC )
92 sqrt00 
 |-  ( ( 2 e. RR /\ 0 <_ 2 ) -> ( ( sqrt ` 2 ) = 0 <-> 2 = 0 ) )
93 84 86 92 mp2an 
 |-  ( ( sqrt ` 2 ) = 0 <-> 2 = 0 )
94 93 necon3bii 
 |-  ( ( sqrt ` 2 ) =/= 0 <-> 2 =/= 0 )
95 58 94 mpbir 
 |-  ( sqrt ` 2 ) =/= 0
96 95 a1i 
 |-  ( A e. CC -> ( sqrt ` 2 ) =/= 0 )
97 83 89 91 89 96 96 divmuldivd 
 |-  ( A e. CC -> ( ( ( sqrt ` ( ( abs ` A ) + ( Re ` A ) ) ) / ( sqrt ` 2 ) ) x. ( ( sqrt ` ( ( abs ` A ) - ( Re ` A ) ) ) / ( sqrt ` 2 ) ) ) = ( ( ( sqrt ` ( ( abs ` A ) + ( Re ` A ) ) ) x. ( sqrt ` ( ( abs ` A ) - ( Re ` A ) ) ) ) / ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) ) )
98 18 resqcld 
 |-  ( A e. CC -> ( ( Re ` A ) ^ 2 ) e. RR )
99 98 recnd 
 |-  ( A e. CC -> ( ( Re ` A ) ^ 2 ) e. CC )
100 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
101 100 resqcld 
 |-  ( A e. CC -> ( ( Im ` A ) ^ 2 ) e. RR )
102 101 recnd 
 |-  ( A e. CC -> ( ( Im ` A ) ^ 2 ) e. CC )
103 absvalsq2 
 |-  ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
104 99 102 103 mvrladdd 
 |-  ( A e. CC -> ( ( ( abs ` A ) ^ 2 ) - ( ( Re ` A ) ^ 2 ) ) = ( ( Im ` A ) ^ 2 ) )
105 subsq 
 |-  ( ( ( abs ` A ) e. CC /\ ( Re ` A ) e. CC ) -> ( ( ( abs ` A ) ^ 2 ) - ( ( Re ` A ) ^ 2 ) ) = ( ( ( abs ` A ) + ( Re ` A ) ) x. ( ( abs ` A ) - ( Re ` A ) ) ) )
106 49 50 105 syl2anc 
 |-  ( A e. CC -> ( ( ( abs ` A ) ^ 2 ) - ( ( Re ` A ) ^ 2 ) ) = ( ( ( abs ` A ) + ( Re ` A ) ) x. ( ( abs ` A ) - ( Re ` A ) ) ) )
107 104 106 eqtr3d 
 |-  ( A e. CC -> ( ( Im ` A ) ^ 2 ) = ( ( ( abs ` A ) + ( Re ` A ) ) x. ( ( abs ` A ) - ( Re ` A ) ) ) )
108 107 fveq2d 
 |-  ( A e. CC -> ( sqrt ` ( ( Im ` A ) ^ 2 ) ) = ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) x. ( ( abs ` A ) - ( Re ` A ) ) ) ) )
109 100 absred 
 |-  ( A e. CC -> ( abs ` ( Im ` A ) ) = ( sqrt ` ( ( Im ` A ) ^ 2 ) ) )
110 reabsifneg 
 |-  ( ( Im ` A ) e. RR -> ( abs ` ( Im ` A ) ) = if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) )
111 100 110 syl 
 |-  ( A e. CC -> ( abs ` ( Im ` A ) ) = if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) )
112 109 111 eqtr3d 
 |-  ( A e. CC -> ( sqrt ` ( ( Im ` A ) ^ 2 ) ) = if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) )
113 19 72 37 79 sqrtmuld 
 |-  ( A e. CC -> ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) x. ( ( abs ` A ) - ( Re ` A ) ) ) ) = ( ( sqrt ` ( ( abs ` A ) + ( Re ` A ) ) ) x. ( sqrt ` ( ( abs ` A ) - ( Re ` A ) ) ) ) )
114 108 112 113 3eqtr3rd 
 |-  ( A e. CC -> ( ( sqrt ` ( ( abs ` A ) + ( Re ` A ) ) ) x. ( sqrt ` ( ( abs ` A ) - ( Re ` A ) ) ) ) = if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) )
115 remsqsqrt 
 |-  ( ( 2 e. RR /\ 0 <_ 2 ) -> ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) = 2 )
116 84 86 115 mp2an 
 |-  ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) = 2
117 116 a1i 
 |-  ( A e. CC -> ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) = 2 )
118 114 117 oveq12d 
 |-  ( A e. CC -> ( ( ( sqrt ` ( ( abs ` A ) + ( Re ` A ) ) ) x. ( sqrt ` ( ( abs ` A ) - ( Re ` A ) ) ) ) / ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) ) = ( if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) / 2 ) )
119 81 97 118 3eqtrd 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) = ( if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) / 2 ) )
120 119 oveq2d 
 |-  ( A e. CC -> ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) = ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) / 2 ) ) )
121 68 120 eqtrd 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) = ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) / 2 ) ) )
122 121 oveq2d 
 |-  ( A e. CC -> ( 2 x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) = ( 2 x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) / 2 ) ) ) )
123 100 renegcld 
 |-  ( A e. CC -> -u ( Im ` A ) e. RR )
124 123 100 ifcld 
 |-  ( A e. CC -> if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) e. RR )
125 124 recnd 
 |-  ( A e. CC -> if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) e. CC )
126 26 125 57 59 divassd 
 |-  ( A e. CC -> ( ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) ) / 2 ) = ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) / 2 ) ) )
127 ovif12 
 |-  ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) ) = if ( ( Im ` A ) < 0 , ( -u 1 x. -u ( Im ` A ) ) , ( 1 x. ( Im ` A ) ) )
128 5 a1i 
 |-  ( A e. CC -> -u 1 e. RR )
129 128 recnd 
 |-  ( A e. CC -> -u 1 e. CC )
130 100 recnd 
 |-  ( A e. CC -> ( Im ` A ) e. CC )
131 129 129 130 mulassd 
 |-  ( A e. CC -> ( ( -u 1 x. -u 1 ) x. ( Im ` A ) ) = ( -u 1 x. ( -u 1 x. ( Im ` A ) ) ) )
132 neg1mulneg1e1 
 |-  ( -u 1 x. -u 1 ) = 1
133 132 a1i 
 |-  ( A e. CC -> ( -u 1 x. -u 1 ) = 1 )
134 133 oveq1d 
 |-  ( A e. CC -> ( ( -u 1 x. -u 1 ) x. ( Im ` A ) ) = ( 1 x. ( Im ` A ) ) )
135 130 mulid2d 
 |-  ( A e. CC -> ( 1 x. ( Im ` A ) ) = ( Im ` A ) )
136 134 135 eqtrd 
 |-  ( A e. CC -> ( ( -u 1 x. -u 1 ) x. ( Im ` A ) ) = ( Im ` A ) )
137 130 mulm1d 
 |-  ( A e. CC -> ( -u 1 x. ( Im ` A ) ) = -u ( Im ` A ) )
138 137 oveq2d 
 |-  ( A e. CC -> ( -u 1 x. ( -u 1 x. ( Im ` A ) ) ) = ( -u 1 x. -u ( Im ` A ) ) )
139 131 136 138 3eqtr3rd 
 |-  ( A e. CC -> ( -u 1 x. -u ( Im ` A ) ) = ( Im ` A ) )
140 139 adantr 
 |-  ( ( A e. CC /\ ( Im ` A ) < 0 ) -> ( -u 1 x. -u ( Im ` A ) ) = ( Im ` A ) )
141 135 adantr 
 |-  ( ( A e. CC /\ -. ( Im ` A ) < 0 ) -> ( 1 x. ( Im ` A ) ) = ( Im ` A ) )
142 140 141 ifeqda 
 |-  ( A e. CC -> if ( ( Im ` A ) < 0 , ( -u 1 x. -u ( Im ` A ) ) , ( 1 x. ( Im ` A ) ) ) = ( Im ` A ) )
143 127 142 syl5eq 
 |-  ( A e. CC -> ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) ) = ( Im ` A ) )
144 143 oveq1d 
 |-  ( A e. CC -> ( ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) ) / 2 ) = ( ( Im ` A ) / 2 ) )
145 126 144 eqtr3d 
 |-  ( A e. CC -> ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) / 2 ) ) = ( ( Im ` A ) / 2 ) )
146 145 oveq2d 
 |-  ( A e. CC -> ( 2 x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) / 2 ) ) ) = ( 2 x. ( ( Im ` A ) / 2 ) ) )
147 130 57 59 divcan2d 
 |-  ( A e. CC -> ( 2 x. ( ( Im ` A ) / 2 ) ) = ( Im ` A ) )
148 146 147 eqtrd 
 |-  ( A e. CC -> ( 2 x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( if ( ( Im ` A ) < 0 , -u ( Im ` A ) , ( Im ` A ) ) / 2 ) ) ) = ( Im ` A ) )
149 67 122 148 3eqtrd 
 |-  ( A e. CC -> ( ( 2 x. ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ) x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) = ( Im ` A ) )
150 149 oveq2d 
 |-  ( A e. CC -> ( _i x. ( ( 2 x. ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ) x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) = ( _i x. ( Im ` A ) ) )
151 65 66 150 3eqtr3d 
 |-  ( A e. CC -> ( 2 x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) = ( _i x. ( Im ` A ) ) )
152 63 151 oveq12d 
 |-  ( A e. CC -> ( ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ^ 2 ) + ( ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ^ 2 ) ) + ( 2 x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
153 1 resqcld 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ^ 2 ) e. RR )
154 153 recnd 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ^ 2 ) e. CC )
155 2 12 mulcld 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) e. CC )
156 57 155 mulcld 
 |-  ( A e. CC -> ( 2 x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) e. CC )
157 12 sqcld 
 |-  ( A e. CC -> ( ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ^ 2 ) e. CC )
158 154 156 157 add32d 
 |-  ( A e. CC -> ( ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ^ 2 ) + ( 2 x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( _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 ) ) ) ) ^ 2 ) ) = ( ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ^ 2 ) + ( ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ^ 2 ) ) + ( 2 x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) )
159 replim 
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
160 152 158 159 3eqtr4d 
 |-  ( A e. CC -> ( ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) ^ 2 ) + ( 2 x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) x. ( _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 ) ) ) ) ^ 2 ) ) = A )
161 16 160 eqtrd 
 |-  ( A e. CC -> ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ^ 2 ) = A )
162 20 69 sqrtge0d 
 |-  ( A e. CC -> 0 <_ ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) )
163 1 10 crred 
 |-  ( A e. CC -> ( Re ` ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) = ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) )
164 162 163 breqtrrd 
 |-  ( A e. CC -> 0 <_ ( Re ` ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) )
165 reim 
 |-  ( ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) e. CC -> ( Re ` ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) = ( Im ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) )
166 13 165 syl 
 |-  ( A e. CC -> ( Re ` ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) = ( Im ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) )
167 166 163 eqtr3d 
 |-  ( A e. CC -> ( Im ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) = ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) )
168 167 eqeq1d 
 |-  ( A e. CC -> ( ( Im ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) = 0 <-> ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) = 0 ) )
169 cnsqrt00 
 |-  ( ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) = 0 <-> ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) = 0 ) )
170 21 169 syl 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) = 0 <-> ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) = 0 ) )
171 half0 
 |-  ( ( ( abs ` A ) + ( Re ` A ) ) e. CC -> ( ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) = 0 <-> ( ( abs ` A ) + ( Re ` A ) ) = 0 ) )
172 55 171 syl 
 |-  ( A e. CC -> ( ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) = 0 <-> ( ( abs ` A ) + ( Re ` A ) ) = 0 ) )
173 49 50 addcomd 
 |-  ( A e. CC -> ( ( abs ` A ) + ( Re ` A ) ) = ( ( Re ` A ) + ( abs ` A ) ) )
174 173 eqeq1d 
 |-  ( A e. CC -> ( ( ( abs ` A ) + ( Re ` A ) ) = 0 <-> ( ( Re ` A ) + ( abs ` A ) ) = 0 ) )
175 addeq0 
 |-  ( ( ( Re ` A ) e. CC /\ ( abs ` A ) e. CC ) -> ( ( ( Re ` A ) + ( abs ` A ) ) = 0 <-> ( Re ` A ) = -u ( abs ` A ) ) )
176 50 49 175 syl2anc 
 |-  ( A e. CC -> ( ( ( Re ` A ) + ( abs ` A ) ) = 0 <-> ( Re ` A ) = -u ( abs ` A ) ) )
177 172 174 176 3bitrd 
 |-  ( A e. CC -> ( ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) = 0 <-> ( Re ` A ) = -u ( abs ` A ) ) )
178 168 170 177 3bitrd 
 |-  ( A e. CC -> ( ( Im ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) = 0 <-> ( Re ` A ) = -u ( abs ` A ) ) )
179 olc 
 |-  ( ( Re ` A ) = -u ( abs ` A ) -> ( ( Re ` A ) = ( abs ` A ) \/ ( Re ` A ) = -u ( abs ` A ) ) )
180 eqcom 
 |-  ( ( ( Re ` A ) ^ 2 ) = ( ( abs ` A ) ^ 2 ) <-> ( ( abs ` A ) ^ 2 ) = ( ( Re ` A ) ^ 2 ) )
181 180 a1i 
 |-  ( A e. CC -> ( ( ( Re ` A ) ^ 2 ) = ( ( abs ` A ) ^ 2 ) <-> ( ( abs ` A ) ^ 2 ) = ( ( Re ` A ) ^ 2 ) ) )
182 sqeqor 
 |-  ( ( ( Re ` A ) e. CC /\ ( abs ` A ) e. CC ) -> ( ( ( Re ` A ) ^ 2 ) = ( ( abs ` A ) ^ 2 ) <-> ( ( Re ` A ) = ( abs ` A ) \/ ( Re ` A ) = -u ( abs ` A ) ) ) )
183 50 49 182 syl2anc 
 |-  ( A e. CC -> ( ( ( Re ` A ) ^ 2 ) = ( ( abs ` A ) ^ 2 ) <-> ( ( Re ` A ) = ( abs ` A ) \/ ( Re ` A ) = -u ( abs ` A ) ) ) )
184 103 eqeq1d 
 |-  ( A e. CC -> ( ( ( abs ` A ) ^ 2 ) = ( ( Re ` A ) ^ 2 ) <-> ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) = ( ( Re ` A ) ^ 2 ) ) )
185 addid0 
 |-  ( ( ( ( Re ` A ) ^ 2 ) e. CC /\ ( ( Im ` A ) ^ 2 ) e. CC ) -> ( ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) = ( ( Re ` A ) ^ 2 ) <-> ( ( Im ` A ) ^ 2 ) = 0 ) )
186 99 102 185 syl2anc 
 |-  ( A e. CC -> ( ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) = ( ( Re ` A ) ^ 2 ) <-> ( ( Im ` A ) ^ 2 ) = 0 ) )
187 sqeq0 
 |-  ( ( Im ` A ) e. CC -> ( ( ( Im ` A ) ^ 2 ) = 0 <-> ( Im ` A ) = 0 ) )
188 130 187 syl 
 |-  ( A e. CC -> ( ( ( Im ` A ) ^ 2 ) = 0 <-> ( Im ` A ) = 0 ) )
189 184 186 188 3bitrd 
 |-  ( A e. CC -> ( ( ( abs ` A ) ^ 2 ) = ( ( Re ` A ) ^ 2 ) <-> ( Im ` A ) = 0 ) )
190 181 183 189 3bitr3d 
 |-  ( A e. CC -> ( ( ( Re ` A ) = ( abs ` A ) \/ ( Re ` A ) = -u ( abs ` A ) ) <-> ( Im ` A ) = 0 ) )
191 179 190 syl5ib 
 |-  ( A e. CC -> ( ( Re ` A ) = -u ( abs ` A ) -> ( Im ` A ) = 0 ) )
192 191 ancld 
 |-  ( A e. CC -> ( ( Re ` A ) = -u ( abs ` A ) -> ( ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) ) )
193 178 192 sylbid 
 |-  ( A e. CC -> ( ( Im ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) = 0 -> ( ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) ) )
194 simp2 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( Re ` A ) = -u ( abs ` A ) )
195 194 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( abs ` A ) + ( Re ` A ) ) = ( ( abs ` A ) + -u ( abs ` A ) ) )
196 simp1 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> A e. CC )
197 196 49 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( abs ` A ) e. CC )
198 197 negidd 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( abs ` A ) + -u ( abs ` A ) ) = 0 )
199 195 198 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( abs ` A ) + ( Re ` A ) ) = 0 )
200 199 oveq1d 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) = ( 0 / 2 ) )
201 2cn 
 |-  2 e. CC
202 201 58 div0i 
 |-  ( 0 / 2 ) = 0
203 200 202 eqtrdi 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) = 0 )
204 203 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) = ( sqrt ` 0 ) )
205 sqrt0 
 |-  ( sqrt ` 0 ) = 0
206 204 205 eqtrdi 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) = 0 )
207 simp3 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( Im ` A ) = 0 )
208 0red 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> 0 e. RR )
209 208 ltnrd 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> -. 0 < 0 )
210 207 209 eqnbrtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> -. ( Im ` A ) < 0 )
211 210 iffalsed 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> if ( ( Im ` A ) < 0 , -u 1 , 1 ) = 1 )
212 194 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( abs ` A ) - ( Re ` A ) ) = ( ( abs ` A ) - -u ( abs ` A ) ) )
213 49 49 subnegd 
 |-  ( A e. CC -> ( ( abs ` A ) - -u ( abs ` A ) ) = ( ( abs ` A ) + ( abs ` A ) ) )
214 49 2timesd 
 |-  ( A e. CC -> ( 2 x. ( abs ` A ) ) = ( ( abs ` A ) + ( abs ` A ) ) )
215 213 214 eqtr4d 
 |-  ( A e. CC -> ( ( abs ` A ) - -u ( abs ` A ) ) = ( 2 x. ( abs ` A ) ) )
216 196 215 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( abs ` A ) - -u ( abs ` A ) ) = ( 2 x. ( abs ` A ) ) )
217 212 216 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( abs ` A ) - ( Re ` A ) ) = ( 2 x. ( abs ` A ) ) )
218 217 oveq1d 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) = ( ( 2 x. ( abs ` A ) ) / 2 ) )
219 49 57 59 divcan3d 
 |-  ( A e. CC -> ( ( 2 x. ( abs ` A ) ) / 2 ) = ( abs ` A ) )
220 196 219 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( 2 x. ( abs ` A ) ) / 2 ) = ( abs ` A ) )
221 218 220 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) = ( abs ` A ) )
222 221 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) = ( sqrt ` ( abs ` A ) ) )
223 211 222 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) = ( 1 x. ( sqrt ` ( abs ` A ) ) ) )
224 absge0 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )
225 17 224 resqrtcld 
 |-  ( A e. CC -> ( sqrt ` ( abs ` A ) ) e. RR )
226 225 recnd 
 |-  ( A e. CC -> ( sqrt ` ( abs ` A ) ) e. CC )
227 226 mulid2d 
 |-  ( A e. CC -> ( 1 x. ( sqrt ` ( abs ` A ) ) ) = ( sqrt ` ( abs ` A ) ) )
228 196 227 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( 1 x. ( sqrt ` ( abs ` A ) ) ) = ( sqrt ` ( abs ` A ) ) )
229 223 228 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) = ( sqrt ` ( abs ` A ) ) )
230 229 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) = ( _i x. ( sqrt ` ( abs ` A ) ) ) )
231 206 230 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) = ( 0 + ( _i x. ( sqrt ` ( abs ` A ) ) ) ) )
232 4 226 mulcld 
 |-  ( A e. CC -> ( _i x. ( sqrt ` ( abs ` A ) ) ) e. CC )
233 196 232 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( _i x. ( sqrt ` ( abs ` A ) ) ) e. CC )
234 233 addid2d 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( 0 + ( _i x. ( sqrt ` ( abs ` A ) ) ) ) = ( _i x. ( sqrt ` ( abs ` A ) ) ) )
235 231 234 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) = ( _i x. ( sqrt ` ( abs ` A ) ) ) )
236 235 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) = ( _i x. ( _i x. ( sqrt ` ( abs ` A ) ) ) ) )
237 ixi 
 |-  ( _i x. _i ) = -u 1
238 237 a1i 
 |-  ( A e. CC -> ( _i x. _i ) = -u 1 )
239 238 oveq1d 
 |-  ( A e. CC -> ( ( _i x. _i ) x. ( sqrt ` ( abs ` A ) ) ) = ( -u 1 x. ( sqrt ` ( abs ` A ) ) ) )
240 4 4 226 mulassd 
 |-  ( A e. CC -> ( ( _i x. _i ) x. ( sqrt ` ( abs ` A ) ) ) = ( _i x. ( _i x. ( sqrt ` ( abs ` A ) ) ) ) )
241 226 mulm1d 
 |-  ( A e. CC -> ( -u 1 x. ( sqrt ` ( abs ` A ) ) ) = -u ( sqrt ` ( abs ` A ) ) )
242 239 240 241 3eqtr3d 
 |-  ( A e. CC -> ( _i x. ( _i x. ( sqrt ` ( abs ` A ) ) ) ) = -u ( sqrt ` ( abs ` A ) ) )
243 196 242 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( _i x. ( _i x. ( sqrt ` ( abs ` A ) ) ) ) = -u ( sqrt ` ( abs ` A ) ) )
244 236 243 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) = -u ( sqrt ` ( abs ` A ) ) )
245 244 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( Re ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) = ( Re ` -u ( sqrt ` ( abs ` A ) ) ) )
246 225 renegcld 
 |-  ( A e. CC -> -u ( sqrt ` ( abs ` A ) ) e. RR )
247 246 rered 
 |-  ( A e. CC -> ( Re ` -u ( sqrt ` ( abs ` A ) ) ) = -u ( sqrt ` ( abs ` A ) ) )
248 196 247 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( Re ` -u ( sqrt ` ( abs ` A ) ) ) = -u ( sqrt ` ( abs ` A ) ) )
249 245 248 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( Re ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) = -u ( sqrt ` ( abs ` A ) ) )
250 17 224 sqrtge0d 
 |-  ( A e. CC -> 0 <_ ( sqrt ` ( abs ` A ) ) )
251 225 le0neg2d 
 |-  ( A e. CC -> ( 0 <_ ( sqrt ` ( abs ` A ) ) <-> -u ( sqrt ` ( abs ` A ) ) <_ 0 ) )
252 250 251 mpbid 
 |-  ( A e. CC -> -u ( sqrt ` ( abs ` A ) ) <_ 0 )
253 196 252 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> -u ( sqrt ` ( abs ` A ) ) <_ 0 )
254 249 253 eqbrtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( Re ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) <_ 0 )
255 254 3expib 
 |-  ( A e. CC -> ( ( ( Re ` A ) = -u ( abs ` A ) /\ ( Im ` A ) = 0 ) -> ( Re ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) <_ 0 ) )
256 193 255 syld 
 |-  ( A e. CC -> ( ( Im ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) = 0 -> ( Re ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) <_ 0 ) )
257 4 13 mulcld 
 |-  ( A e. CC -> ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) e. CC )
258 257 sqrtcvallem1 
 |-  ( A e. CC -> ( ( ( Im ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) = 0 -> ( Re ` ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) ) <_ 0 ) <-> -. ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) e. RR+ ) )
259 256 258 mpbid 
 |-  ( A e. CC -> -. ( _i x. ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) ) e. RR+ )
260 13 14 161 164 259 eqsqrtd 
 |-  ( A e. CC -> ( ( sqrt ` ( ( ( abs ` A ) + ( Re ` A ) ) / 2 ) ) + ( _i x. ( if ( ( Im ` A ) < 0 , -u 1 , 1 ) x. ( sqrt ` ( ( ( abs ` A ) - ( Re ` A ) ) / 2 ) ) ) ) ) = ( sqrt ` A ) )
261 260 eqcomd 
 |-  ( 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 ) ) ) ) ) )