Theorem sqrtcval 43603

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 15241 and crimi 15242. 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.)

Assertion

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

Proof of Theorem sqrtcval

Step	Hyp	Ref	Expression
1		sqrtcvallem5 43602	. . . . 5 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℝ)
2	1	recnd 11318	. . . 4 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℂ)
3		ax-icn 11243	. . . . . 6 ⊢ i ∈ ℂ
4	3	a1i 11	. . . . 5 ⊢ (𝐴 ∈ ℂ → i ∈ ℂ)
5		neg1rr 12408	. . . . . . . . 9 ⊢ -1 ∈ ℝ
6		1re 11290	. . . . . . . . 9 ⊢ 1 ∈ ℝ
7	5, 6	ifcli 4595	. . . . . . . 8 ⊢ if((ℑ‘𝐴) < 0, -1, 1) ∈ ℝ
8	7	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -1, 1) ∈ ℝ)
9		sqrtcvallem3 43600	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℝ)
10	8, 9	remulcld 11320	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℝ)
11	10	recnd 11318	. . . . 5 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℂ)
12	4, 11	mulcld 11310	. . . 4 ⊢ (𝐴 ∈ ℂ → (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) ∈ ℂ)
13	2, 12	addcld 11309	. . 3 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ)
14		id 22	. . 3 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
15		binom2 14266	. . . . 5 ⊢ (((√‘(((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 583	. . . 4 ⊢ (𝐴 ∈ ℂ → (((√‘(((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 15327	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
18		recl 15159	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
19	17, 18	readdcld 11319	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℝ)
20	19	rehalfcld 12540	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) ∈ ℝ)
21	20	recnd 11318	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) ∈ ℂ)
22	21	sqsqrtd 15488	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) + (ℜ‘𝐴)) / 2))
23	4, 11	sqmuld 14208	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) = ((i↑2) · ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2)))
24		i2 14251	. . . . . . . . . . 11 ⊢ (i↑2) = -1
25	24	a1i 11	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (i↑2) = -1)
26	8	recnd 11318	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -1, 1) ∈ ℂ)
27	9	recnd 11318	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℂ)
28	26, 27	sqmuld 14208	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2) = ((if((ℑ‘𝐴) < 0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2)))
29		ovif 7548	. . . . . . . . . . . . . 14 ⊢ (if((ℑ‘𝐴) < 0, -1, 1)↑2) = if((ℑ‘𝐴) < 0, (-1↑2), (1↑2))
30		neg1sqe1 14245	. . . . . . . . . . . . . . 15 ⊢ (-1↑2) = 1
31		sq1 14244	. . . . . . . . . . . . . . 15 ⊢ (1↑2) = 1
32		ifeq12 4566	. . . . . . . . . . . . . . 15 ⊢ (((-1↑2) = 1 ∧ (1↑2) = 1) → if((ℑ‘𝐴) < 0, (-1↑2), (1↑2)) = if((ℑ‘𝐴) < 0, 1, 1))
33	30, 31, 32	mp2an 691	. . . . . . . . . . . . . 14 ⊢ if((ℑ‘𝐴) < 0, (-1↑2), (1↑2)) = if((ℑ‘𝐴) < 0, 1, 1)
34		ifid 4588	. . . . . . . . . . . . . 14 ⊢ if((ℑ‘𝐴) < 0, 1, 1) = 1
35	29, 33, 34	3eqtri 2772	. . . . . . . . . . . . 13 ⊢ (if((ℑ‘𝐴) < 0, -1, 1)↑2) = 1
36	35	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1)↑2) = 1)
37	17, 18	resubcld 11718	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − (ℜ‘𝐴)) ∈ ℝ)
38	37	rehalfcld 12540	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) ∈ ℝ)
39	38	recnd 11318	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) ∈ ℂ)
40	39	sqsqrtd 15488	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
41	36, 40	oveq12d 7466	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2)) = (1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
42	39	mullidd 11308	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
43	28, 41, 42	3eqtrd 2784	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
44	25, 43	oveq12d 7466	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((i↑2) · ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2)) = (-1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
45	39	mulm1d 11742	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (-1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = -(((abs‘𝐴) − (ℜ‘𝐴)) / 2))
46	23, 44, 45	3eqtrd 2784	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) = -(((abs‘𝐴) − (ℜ‘𝐴)) / 2))
47	22, 46	oveq12d 7466	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) + -(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
48	21, 39	negsubd 11653	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) + -(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) − (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
49	17	recnd 11318	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℂ)
50	18	recnd 11318	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℂ)
51	49, 50, 50	pnncand 11686	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) = ((ℜ‘𝐴) + (ℜ‘𝐴)))
52	50	2timesd 12536	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (2 · (ℜ‘𝐴)) = ((ℜ‘𝐴) + (ℜ‘𝐴)))
53	51, 52	eqtr4d 2783	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) = (2 · (ℜ‘𝐴)))
54	53	oveq1d 7463	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) / 2) = ((2 · (ℜ‘𝐴)) / 2))
55	19	recnd 11318	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℂ)
56	37	recnd 11318	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − (ℜ‘𝐴)) ∈ ℂ)
57		2cnd 12371	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℂ)
58		2ne0 12397	. . . . . . . . . 10 ⊢ 2 ≠ 0
59	58	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 2 ≠ 0)
60	55, 56, 57, 59	divsubdird 12109	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) / 2) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) − (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
61	50, 57, 59	divcan3d 12075	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((2 · (ℜ‘𝐴)) / 2) = (ℜ‘𝐴))
62	54, 60, 61	3eqtr3d 2788	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) − (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (ℜ‘𝐴))
63	47, 48, 62	3eqtrd 2784	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = (ℜ‘𝐴))
64	57, 2	mulcld 11310	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) ∈ ℂ)
65	64, 4, 11	mul12d 11499	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((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 11313	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((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 11313	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))
68	2, 26, 27	mul12d 11499	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))
69		sqrtcvallem4 43601	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2))
70		halfnneg2 12524	. . . . . . . . . . . . . . . . 17 ⊢ (((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℝ → (0 ≤ ((abs‘𝐴) + (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
71	19, 70	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (0 ≤ ((abs‘𝐴) + (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
72	69, 71	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → 0 ≤ ((abs‘𝐴) + (ℜ‘𝐴)))
73		2rp 13062	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ+
74	73	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℝ+)
75	19, 72, 74	sqrtdivd 15472	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)))
76		sqrtcvallem2 43599	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
77		halfnneg2 12524	. . . . . . . . . . . . . . . . 17 ⊢ (((abs‘𝐴) − (ℜ‘𝐴)) ∈ ℝ → (0 ≤ ((abs‘𝐴) − (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
78	37, 77	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (0 ≤ ((abs‘𝐴) − (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
79	76, 78	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → 0 ≤ ((abs‘𝐴) − (ℜ‘𝐴)))
80	37, 79, 74	sqrtdivd 15472	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2)))
81	75, 80	oveq12d 7466	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) · ((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2))))
82	19, 72	resqrtcld 15466	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℝ)
83	82	recnd 11318	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℂ)
84		2re 12367	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
85	84	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℝ)
86		0le2 12395	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≤ 2
87	86	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → 0 ≤ 2)
88	85, 87	resqrtcld 15466	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘2) ∈ ℝ)
89	88	recnd 11318	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘2) ∈ ℂ)
90	37, 79	resqrtcld 15466	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℝ)
91	90	recnd 11318	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℂ)
92		sqrt00 15312	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) = 0 ↔ 2 = 0))
93	84, 86, 92	mp2an 691	. . . . . . . . . . . . . . . . 17 ⊢ ((√‘2) = 0 ↔ 2 = 0)
94	93	necon3bii 2999	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) ≠ 0 ↔ 2 ≠ 0)
95	58, 94	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ≠ 0
96	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘2) ≠ 0)
97	83, 89, 91, 89, 96, 96	divmuldivd 12111	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) · ((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2))) = (((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) · (√‘2))))
98	18	resqcld 14175	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴)↑2) ∈ ℝ)
99	98	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴)↑2) ∈ ℂ)
100		imcl 15160	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ)
101	100	resqcld 14175	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴)↑2) ∈ ℝ)
102	101	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴)↑2) ∈ ℂ)
103		absvalsq2 15330	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
104	99, 102, 103	mvrladdd 11703	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) − ((ℜ‘𝐴)↑2)) = ((ℑ‘𝐴)↑2))
105		subsq 14259	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs‘𝐴) ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) → (((abs‘𝐴)↑2) − ((ℜ‘𝐴)↑2)) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))
106	49, 50, 105	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) − ((ℜ‘𝐴)↑2)) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))
107	104, 106	eqtr3d 2782	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴)↑2) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))
108	107	fveq2d 6924	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘((ℑ‘𝐴)↑2)) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))))
109	100	absred 15465	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (abs‘(ℑ‘𝐴)) = (√‘((ℑ‘𝐴)↑2)))
110		reabsifneg 43594	. . . . . . . . . . . . . . . . 17 ⊢ ((ℑ‘𝐴) ∈ ℝ → (abs‘(ℑ‘𝐴)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
111	100, 110	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (abs‘(ℑ‘𝐴)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
112	109, 111	eqtr3d 2782	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘((ℑ‘𝐴)↑2)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
113	19, 72, 37, 79	sqrtmuld 15473	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))))
114	108, 112, 113	3eqtr3rd 2789	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
115		remsqsqrt 15305	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
116	84, 86, 115	mp2an 691	. . . . . . . . . . . . . . 15 ⊢ ((√‘2) · (√‘2)) = 2
117	116	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((√‘2) · (√‘2)) = 2)
118	114, 117	oveq12d 7466	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) · (√‘2))) = (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))
119	81, 97, 118	3eqtrd 2784	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))
120	119	oveq2d 7464	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))
121	68, 120	eqtrd 2780	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))
122	121	oveq2d 7464	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (2 · (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))))
123	100	renegcld 11717	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → -(ℑ‘𝐴) ∈ ℝ)
124	123, 100	ifcld 4594	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) ∈ ℝ)
125	124	recnd 11318	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) ∈ ℂ)
126	26, 125, 57, 59	divassd 12105	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) / 2) = (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))
127		ovif12 7550	. . . . . . . . . . . . . 14 ⊢ (if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) = if((ℑ‘𝐴) < 0, (-1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴)))
128	5	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → -1 ∈ ℝ)
129	128	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → -1 ∈ ℂ)
130	100	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℂ)
131	129, 129, 130	mulassd 11313	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → ((-1 · -1) · (ℑ‘𝐴)) = (-1 · (-1 · (ℑ‘𝐴))))
132		neg1mulneg1e1 12506	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-1 · -1) = 1
133	132	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → (-1 · -1) = 1)
134	133	oveq1d 7463	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((-1 · -1) · (ℑ‘𝐴)) = (1 · (ℑ‘𝐴)))
135	130	mullidd 11308	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (1 · (ℑ‘𝐴)) = (ℑ‘𝐴))
136	134, 135	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → ((-1 · -1) · (ℑ‘𝐴)) = (ℑ‘𝐴))
137	130	mulm1d 11742	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (-1 · (ℑ‘𝐴)) = -(ℑ‘𝐴))
138	137	oveq2d 7464	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (-1 · (-1 · (ℑ‘𝐴))) = (-1 · -(ℑ‘𝐴)))
139	131, 136, 138	3eqtr3rd 2789	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (-1 · -(ℑ‘𝐴)) = (ℑ‘𝐴))
140	139	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → (-1 · -(ℑ‘𝐴)) = (ℑ‘𝐴))
141	135	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ ¬ (ℑ‘𝐴) < 0) → (1 · (ℑ‘𝐴)) = (ℑ‘𝐴))
142	140, 141	ifeqda 4584	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, (-1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴))) = (ℑ‘𝐴))
143	127, 142	eqtrid 2792	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) = (ℑ‘𝐴))
144	143	oveq1d 7463	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) / 2) = ((ℑ‘𝐴) / 2))
145	126, 144	eqtr3d 2782	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)) = ((ℑ‘𝐴) / 2))
146	145	oveq2d 7464	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (2 · (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))) = (2 · ((ℑ‘𝐴) / 2)))
147	130, 57, 59	divcan2d 12072	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (2 · ((ℑ‘𝐴) / 2)) = (ℑ‘𝐴))
148	146, 147	eqtrd 2780	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (2 · (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))) = (ℑ‘𝐴))
149	67, 122, 148	3eqtrd 2784	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (ℑ‘𝐴))
150	149	oveq2d 7464	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (i · ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i · (ℑ‘𝐴)))
151	65, 66, 150	3eqtr3d 2788	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i · (ℑ‘𝐴)))
152	63, 151	oveq12d 7466	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((((√‘(((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 14175	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈ ℝ)
154	153	recnd 11318	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈ ℂ)
155	2, 12	mulcld 11310	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ)
156	57, 155	mulcld 11310	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈ ℂ)
157	12	sqcld 14194	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) ∈ ℂ)
158	154, 156, 157	add32d 11517	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((((√‘(((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 15165	. . . . 5 ⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))))
160	152, 158, 159	3eqtr4d 2790	. . . 4 ⊢ (𝐴 ∈ ℂ → ((((√‘(((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 2780	. . 3 ⊢ (𝐴 ∈ ℂ → (((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))↑2) = 𝐴)
162	20, 69	sqrtge0d 15469	. . . 4 ⊢ (𝐴 ∈ ℂ → 0 ≤ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
163	1, 10	crred 15280	. . . 4 ⊢ (𝐴 ∈ ℂ → (ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
164	162, 163	breqtrrd 5194	. . 3 ⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))))
165		reim 15158	. . . . . . . . . 10 ⊢ (((√‘(((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 17	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))))
167	166, 163	eqtr3d 2782	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
168	167	eqeq1d 2742	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 ↔ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0))
169		cnsqrt00 15441	. . . . . . . 8 ⊢ ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0))
170	21, 169	syl 17	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0))
171		half0 12520	. . . . . . . . 9 ⊢ (((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ ((abs‘𝐴) + (ℜ‘𝐴)) = 0))
172	55, 171	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ ((abs‘𝐴) + (ℜ‘𝐴)) = 0))
173	49, 50	addcomd 11492	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + (ℜ‘𝐴)) = ((ℜ‘𝐴) + (abs‘𝐴)))
174	173	eqeq1d 2742	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) = 0 ↔ ((ℜ‘𝐴) + (abs‘𝐴)) = 0))
175		addeq0 11713	. . . . . . . . 9 ⊢ (((ℜ‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (((ℜ‘𝐴) + (abs‘𝐴)) = 0 ↔ (ℜ‘𝐴) = -(abs‘𝐴)))
176	50, 49, 175	syl2anc 583	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴) + (abs‘𝐴)) = 0 ↔ (ℜ‘𝐴) = -(abs‘𝐴)))
177	172, 174, 176	3bitrd 305	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ (ℜ‘𝐴) = -(abs‘𝐴)))
178	168, 170, 177	3bitrd 305	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 ↔ (ℜ‘𝐴) = -(abs‘𝐴)))
179		olc 867	. . . . . . . 8 ⊢ ((ℜ‘𝐴) = -(abs‘𝐴) → ((ℜ‘𝐴) = (abs‘𝐴) ∨ (ℜ‘𝐴) = -(abs‘𝐴)))
180		eqcom 2747	. . . . . . . . . 10 ⊢ (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2))
181	180	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2)))
182		sqeqor 14265	. . . . . . . . . 10 ⊢ (((ℜ‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((ℜ‘𝐴) = (abs‘𝐴) ∨ (ℜ‘𝐴) = -(abs‘𝐴))))
183	50, 49, 182	syl2anc 583	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((ℜ‘𝐴) = (abs‘𝐴) ∨ (ℜ‘𝐴) = -(abs‘𝐴))))
184	103	eqeq1d 2742	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2) ↔ (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2)))
185		addid0 11709	. . . . . . . . . . 11 ⊢ ((((ℜ‘𝐴)↑2) ∈ ℂ ∧ ((ℑ‘𝐴)↑2) ∈ ℂ) → ((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2) ↔ ((ℑ‘𝐴)↑2) = 0))
186	99, 102, 185	syl2anc 583	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2) ↔ ((ℑ‘𝐴)↑2) = 0))
187		sqeq0 14170	. . . . . . . . . . 11 ⊢ ((ℑ‘𝐴) ∈ ℂ → (((ℑ‘𝐴)↑2) = 0 ↔ (ℑ‘𝐴) = 0))
188	130, 187	syl 17	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((ℑ‘𝐴)↑2) = 0 ↔ (ℑ‘𝐴) = 0))
189	184, 186, 188	3bitrd 305	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2) ↔ (ℑ‘𝐴) = 0))
190	181, 183, 189	3bitr3d 309	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴) = (abs‘𝐴) ∨ (ℜ‘𝐴) = -(abs‘𝐴)) ↔ (ℑ‘𝐴) = 0))
191	179, 190	imbitrid 244	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴) = -(abs‘𝐴) → (ℑ‘𝐴) = 0))
192	191	ancld 550	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴) = -(abs‘𝐴) → ((ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0)))
193	178, 192	sylbid 240	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 → ((ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0)))
194		simp2 1137	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘𝐴) = -(abs‘𝐴))
195	194	oveq2d 7464	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) + (ℜ‘𝐴)) = ((abs‘𝐴) + -(abs‘𝐴)))
196	49	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (abs‘𝐴) ∈ ℂ)
197	196	negidd 11637	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) + -(abs‘𝐴)) = 0)
198	195, 197	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) + (ℜ‘𝐴)) = 0)
199	198	oveq1d 7463	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = (0 / 2))
200		2cn 12368	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℂ
201	200, 58	div0i 12028	. . . . . . . . . . . . . . . 16 ⊢ (0 / 2) = 0
202	199, 201	eqtrdi 2796	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0)
203	202	fveq2d 6924	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = (√‘0))
204		sqrt0 15290	. . . . . . . . . . . . . 14 ⊢ (√‘0) = 0
205	203, 204	eqtrdi 2796	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0)
206		simp3 1138	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℑ‘𝐴) = 0)
207		0red 11293	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → 0 ∈ ℝ)
208	207	ltnrd 11424	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ¬ 0 < 0)
209	206, 208	eqnbrtrd 5184	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ¬ (ℑ‘𝐴) < 0)
210	209	iffalsed 4559	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → if((ℑ‘𝐴) < 0, -1, 1) = 1)
211	194	oveq2d 7464	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) − (ℜ‘𝐴)) = ((abs‘𝐴) − -(abs‘𝐴)))
212	49, 49	subnegd 11654	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − -(abs‘𝐴)) = ((abs‘𝐴) + (abs‘𝐴)))
213	49	2timesd 12536	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ ℂ → (2 · (abs‘𝐴)) = ((abs‘𝐴) + (abs‘𝐴)))
214	212, 213	eqtr4d 2783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − -(abs‘𝐴)) = (2 · (abs‘𝐴)))
215	214	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) − -(abs‘𝐴)) = (2 · (abs‘𝐴)))
216	211, 215	eqtrd 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) − (ℜ‘𝐴)) = (2 · (abs‘𝐴)))
217	216	oveq1d 7463	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) = ((2 · (abs‘𝐴)) / 2))
218	49, 57, 59	divcan3d 12075	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) / 2) = (abs‘𝐴))
219	218	3ad2ant1 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((2 · (abs‘𝐴)) / 2) = (abs‘𝐴))
220	217, 219	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) = (abs‘𝐴))
221	220	fveq2d 6924	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (√‘(abs‘𝐴)))
222	210, 221	oveq12d 7466	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (1 · (√‘(abs‘𝐴))))
223		absge0 15336	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
224	17, 223	resqrtcld 15466	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℝ)
225	224	recnd 11318	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℂ)
226	225	mullidd 11308	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (1 · (√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
227	226	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (1 · (√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
228	222, 227	eqtrd 2780	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (√‘(abs‘𝐴)))
229	228	oveq2d 7464	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (i · (√‘(abs‘𝐴))))
230	205, 229	oveq12d 7466	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (0 + (i · (√‘(abs‘𝐴)))))
231	4, 225	mulcld 11310	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (i · (√‘(abs‘𝐴))) ∈ ℂ)
232	231	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · (√‘(abs‘𝐴))) ∈ ℂ)
233	232	addlidd 11491	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (0 + (i · (√‘(abs‘𝐴)))) = (i · (√‘(abs‘𝐴))))
234	230, 233	eqtrd 2780	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i · (√‘(abs‘𝐴))))
235	234	oveq2d 7464	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i · (i · (√‘(abs‘𝐴)))))
236		ixi 11919	. . . . . . . . . . . . . 14 ⊢ (i · i) = -1
237	236	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (i · i) = -1)
238	237	oveq1d 7463	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((i · i) · (√‘(abs‘𝐴))) = (-1 · (√‘(abs‘𝐴))))
239	4, 4, 225	mulassd 11313	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((i · i) · (√‘(abs‘𝐴))) = (i · (i · (√‘(abs‘𝐴)))))
240	225	mulm1d 11742	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (-1 · (√‘(abs‘𝐴))) = -(√‘(abs‘𝐴)))
241	238, 239, 240	3eqtr3d 2788	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (i · (i · (√‘(abs‘𝐴)))) = -(√‘(abs‘𝐴)))
242	241	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · (i · (√‘(abs‘𝐴)))) = -(√‘(abs‘𝐴)))
243	235, 242	eqtrd 2780	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = -(√‘(abs‘𝐴)))
244	243	fveq2d 6924	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = (ℜ‘-(√‘(abs‘𝐴))))
245	224	renegcld 11717	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → -(√‘(abs‘𝐴)) ∈ ℝ)
246	245	rered 15273	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (ℜ‘-(√‘(abs‘𝐴))) = -(√‘(abs‘𝐴)))
247	246	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘-(√‘(abs‘𝐴))) = -(√‘(abs‘𝐴)))
248	244, 247	eqtrd 2780	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = -(√‘(abs‘𝐴)))
249	17, 223	sqrtge0d 15469	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 0 ≤ (√‘(abs‘𝐴)))
250	224	le0neg2d 11862	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (0 ≤ (√‘(abs‘𝐴)) ↔ -(√‘(abs‘𝐴)) ≤ 0))
251	249, 250	mpbid 232	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → -(√‘(abs‘𝐴)) ≤ 0)
252	251	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → -(√‘(abs‘𝐴)) ≤ 0)
253	248, 252	eqbrtrd 5188	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) ≤ 0)
254	253	3expib 1122	. . . . 5 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) ≤ 0))
255	193, 254	syld 47	. . . 4 ⊢ (𝐴 ∈ ℂ → ((ℑ‘(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 11310	. . . . 5 ⊢ (𝐴 ∈ ℂ → (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈ ℂ)
257	256	sqrtcvallem1 43593	. . . 4 ⊢ (𝐴 ∈ ℂ → (((ℑ‘(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 232	. . 3 ⊢ (𝐴 ∈ ℂ → ¬ (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈ ℝ+)
259	13, 14, 161, 164, 258	eqsqrtd 15416	. 2 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (√‘𝐴))
260	259	eqcomd 2746	1 ⊢ (𝐴 ∈ ℂ → (√‘𝐴) = ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ifcif 4548   class class class wbr 5166  ‘cfv 6573  (class class class)co 7448  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185  ici 11186   + caddc 11187   · cmul 11189   < clt 11324   ≤ cle 11325   − cmin 11520  -cneg 11521   / cdiv 11947  2c2 12348  ℝ⁺crp 13057  ↑cexp 14112  ℜcre 15146  ℑcim 15147  √csqrt 15282  abscabs 15283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-sup 9511  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-n0 12554  df-z 12640  df-uz 12904  df-rp 13058  df-seq 14053  df-exp 14113  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285

This theorem is referenced by:  sqrtcval2  43604  resqrtval  43605  imsqrtval  43606