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 ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) = ( ( √ ‘ ( ( ( abs ‘ 𝐴 ) + ( ℜ ‘ 𝐴 ) ) / 2 ) ) + ( i · ( if ( ( ℑ ‘ 𝐴 ) < 0 , - 1 , 1 ) · ( √ ‘ ( ( ( abs ‘ 𝐴 ) − ( ℜ ‘ 𝐴 ) ) / 2 ) ) ) ) ) )

Proof

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