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 ) ) ) ) ) )