Theorem sqrtcval 42392

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 15139 and crimi 15140. 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 42391	. . . . 5 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℝ)
2	1	recnd 11242	. . . 4 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℂ)
3		ax-icn 11169	. . . . . 6 ⊢ i ∈ ℂ
4	3	a1i 11	. . . . 5 ⊢ (𝐴 ∈ ℂ → i ∈ ℂ)
5		neg1rr 12327	. . . . . . . . 9 ⊢ -1 ∈ ℝ
6		1re 11214	. . . . . . . . 9 ⊢ 1 ∈ ℝ
7	5, 6	ifcli 4576	. . . . . . . 8 ⊢ if((ℑ‘𝐴) < 0, -1, 1) ∈ ℝ
8	7	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -1, 1) ∈ ℝ)
9		sqrtcvallem3 42389	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℝ)
10	8, 9	remulcld 11244	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℝ)
11	10	recnd 11242	. . . . 5 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℂ)
12	4, 11	mulcld 11234	. . . 4 ⊢ (𝐴 ∈ ℂ → (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) ∈ ℂ)
13	2, 12	addcld 11233	. . 3 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ)
14		id 22	. . 3 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
15		binom2 14181	. . . . 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 585	. . . 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 15225	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
18		recl 15057	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
19	17, 18	readdcld 11243	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℝ)
20	19	rehalfcld 12459	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) ∈ ℝ)
21	20	recnd 11242	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) ∈ ℂ)
22	21	sqsqrtd 15386	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) + (ℜ‘𝐴)) / 2))
23	4, 11	sqmuld 14123	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) = ((i↑2) · ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2)))
24		i2 14166	. . . . . . . . . . 11 ⊢ (i↑2) = -1
25	24	a1i 11	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (i↑2) = -1)
26	8	recnd 11242	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -1, 1) ∈ ℂ)
27	9	recnd 11242	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℂ)
28	26, 27	sqmuld 14123	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2) = ((if((ℑ‘𝐴) < 0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2)))
29		ovif 7506	. . . . . . . . . . . . . 14 ⊢ (if((ℑ‘𝐴) < 0, -1, 1)↑2) = if((ℑ‘𝐴) < 0, (-1↑2), (1↑2))
30		neg1sqe1 14160	. . . . . . . . . . . . . . 15 ⊢ (-1↑2) = 1
31		sq1 14159	. . . . . . . . . . . . . . 15 ⊢ (1↑2) = 1
32		ifeq12 4547	. . . . . . . . . . . . . . 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 4569	. . . . . . . . . . . . . 14 ⊢ if((ℑ‘𝐴) < 0, 1, 1) = 1
35	29, 33, 34	3eqtri 2765	. . . . . . . . . . . . 13 ⊢ (if((ℑ‘𝐴) < 0, -1, 1)↑2) = 1
36	35	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1)↑2) = 1)
37	17, 18	resubcld 11642	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − (ℜ‘𝐴)) ∈ ℝ)
38	37	rehalfcld 12459	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) ∈ ℝ)
39	38	recnd 11242	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) ∈ ℂ)
40	39	sqsqrtd 15386	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
41	36, 40	oveq12d 7427	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2)) = (1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
42	39	mullidd 11232	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
43	28, 41, 42	3eqtrd 2777	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
44	25, 43	oveq12d 7427	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((i↑2) · ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2)) = (-1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
45	39	mulm1d 11666	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (-1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = -(((abs‘𝐴) − (ℜ‘𝐴)) / 2))
46	23, 44, 45	3eqtrd 2777	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) = -(((abs‘𝐴) − (ℜ‘𝐴)) / 2))
47	22, 46	oveq12d 7427	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) + -(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
48	21, 39	negsubd 11577	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) + -(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) − (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
49	17	recnd 11242	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℂ)
50	18	recnd 11242	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℂ)
51	49, 50, 50	pnncand 11610	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) = ((ℜ‘𝐴) + (ℜ‘𝐴)))
52	50	2timesd 12455	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (2 · (ℜ‘𝐴)) = ((ℜ‘𝐴) + (ℜ‘𝐴)))
53	51, 52	eqtr4d 2776	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) = (2 · (ℜ‘𝐴)))
54	53	oveq1d 7424	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) / 2) = ((2 · (ℜ‘𝐴)) / 2))
55	19	recnd 11242	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℂ)
56	37	recnd 11242	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − (ℜ‘𝐴)) ∈ ℂ)
57		2cnd 12290	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℂ)
58		2ne0 12316	. . . . . . . . . 10 ⊢ 2 ≠ 0
59	58	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 2 ≠ 0)
60	55, 56, 57, 59	divsubdird 12029	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) / 2) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) − (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
61	50, 57, 59	divcan3d 11995	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((2 · (ℜ‘𝐴)) / 2) = (ℜ‘𝐴))
62	54, 60, 61	3eqtr3d 2781	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) − (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (ℜ‘𝐴))
63	47, 48, 62	3eqtrd 2777	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = (ℜ‘𝐴))
64	57, 2	mulcld 11234	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) ∈ ℂ)
65	64, 4, 11	mul12d 11423	. . . . . . 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 11237	. . . . . . 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 11237	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))
68	2, 26, 27	mul12d 11423	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))
69		sqrtcvallem4 42390	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2))
70		halfnneg2 12443	. . . . . . . . . . . . . . . . 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 12979	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ+
74	73	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℝ+)
75	19, 72, 74	sqrtdivd 15370	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)))
76		sqrtcvallem2 42388	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
77		halfnneg2 12443	. . . . . . . . . . . . . . . . 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 15370	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2)))
81	75, 80	oveq12d 7427	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) · ((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2))))
82	19, 72	resqrtcld 15364	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℝ)
83	82	recnd 11242	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℂ)
84		2re 12286	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
85	84	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℝ)
86		0le2 12314	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≤ 2
87	86	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → 0 ≤ 2)
88	85, 87	resqrtcld 15364	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘2) ∈ ℝ)
89	88	recnd 11242	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘2) ∈ ℂ)
90	37, 79	resqrtcld 15364	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℝ)
91	90	recnd 11242	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℂ)
92		sqrt00 15210	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) = 0 ↔ 2 = 0))
93	84, 86, 92	mp2an 691	. . . . . . . . . . . . . . . . 17 ⊢ ((√‘2) = 0 ↔ 2 = 0)
94	93	necon3bii 2994	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) ≠ 0 ↔ 2 ≠ 0)
95	58, 94	mpbir 230	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ≠ 0
96	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘2) ≠ 0)
97	83, 89, 91, 89, 96, 96	divmuldivd 12031	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) · ((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2))) = (((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) · (√‘2))))
98	18	resqcld 14090	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴)↑2) ∈ ℝ)
99	98	recnd 11242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴)↑2) ∈ ℂ)
100		imcl 15058	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ)
101	100	resqcld 14090	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴)↑2) ∈ ℝ)
102	101	recnd 11242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴)↑2) ∈ ℂ)
103		absvalsq2 15228	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
104	99, 102, 103	mvrladdd 11627	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) − ((ℜ‘𝐴)↑2)) = ((ℑ‘𝐴)↑2))
105		subsq 14174	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs‘𝐴) ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) → (((abs‘𝐴)↑2) − ((ℜ‘𝐴)↑2)) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))
106	49, 50, 105	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) − ((ℜ‘𝐴)↑2)) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))
107	104, 106	eqtr3d 2775	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴)↑2) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))
108	107	fveq2d 6896	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘((ℑ‘𝐴)↑2)) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))))
109	100	absred 15363	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (abs‘(ℑ‘𝐴)) = (√‘((ℑ‘𝐴)↑2)))
110		reabsifneg 42383	. . . . . . . . . . . . . . . . 17 ⊢ ((ℑ‘𝐴) ∈ ℝ → (abs‘(ℑ‘𝐴)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
111	100, 110	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (abs‘(ℑ‘𝐴)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
112	109, 111	eqtr3d 2775	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘((ℑ‘𝐴)↑2)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
113	19, 72, 37, 79	sqrtmuld 15371	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))))
114	108, 112, 113	3eqtr3rd 2782	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
115		remsqsqrt 15203	. . . . . . . . . . . . . . . 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 7427	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) · (√‘2))) = (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))
119	81, 97, 118	3eqtrd 2777	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))
120	119	oveq2d 7425	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))
121	68, 120	eqtrd 2773	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))
122	121	oveq2d 7425	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (2 · (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))))
123	100	renegcld 11641	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → -(ℑ‘𝐴) ∈ ℝ)
124	123, 100	ifcld 4575	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) ∈ ℝ)
125	124	recnd 11242	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) ∈ ℂ)
126	26, 125, 57, 59	divassd 12025	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) / 2) = (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))
127		ovif12 7508	. . . . . . . . . . . . . 14 ⊢ (if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) = if((ℑ‘𝐴) < 0, (-1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴)))
128	5	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → -1 ∈ ℝ)
129	128	recnd 11242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → -1 ∈ ℂ)
130	100	recnd 11242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℂ)
131	129, 129, 130	mulassd 11237	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → ((-1 · -1) · (ℑ‘𝐴)) = (-1 · (-1 · (ℑ‘𝐴))))
132		neg1mulneg1e1 12425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-1 · -1) = 1
133	132	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → (-1 · -1) = 1)
134	133	oveq1d 7424	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((-1 · -1) · (ℑ‘𝐴)) = (1 · (ℑ‘𝐴)))
135	130	mullidd 11232	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (1 · (ℑ‘𝐴)) = (ℑ‘𝐴))
136	134, 135	eqtrd 2773	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → ((-1 · -1) · (ℑ‘𝐴)) = (ℑ‘𝐴))
137	130	mulm1d 11666	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (-1 · (ℑ‘𝐴)) = -(ℑ‘𝐴))
138	137	oveq2d 7425	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (-1 · (-1 · (ℑ‘𝐴))) = (-1 · -(ℑ‘𝐴)))
139	131, 136, 138	3eqtr3rd 2782	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (-1 · -(ℑ‘𝐴)) = (ℑ‘𝐴))
140	139	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → (-1 · -(ℑ‘𝐴)) = (ℑ‘𝐴))
141	135	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ ¬ (ℑ‘𝐴) < 0) → (1 · (ℑ‘𝐴)) = (ℑ‘𝐴))
142	140, 141	ifeqda 4565	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, (-1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴))) = (ℑ‘𝐴))
143	127, 142	eqtrid 2785	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) = (ℑ‘𝐴))
144	143	oveq1d 7424	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) / 2) = ((ℑ‘𝐴) / 2))
145	126, 144	eqtr3d 2775	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)) = ((ℑ‘𝐴) / 2))
146	145	oveq2d 7425	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (2 · (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))) = (2 · ((ℑ‘𝐴) / 2)))
147	130, 57, 59	divcan2d 11992	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (2 · ((ℑ‘𝐴) / 2)) = (ℑ‘𝐴))
148	146, 147	eqtrd 2773	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (2 · (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))) = (ℑ‘𝐴))
149	67, 122, 148	3eqtrd 2777	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (ℑ‘𝐴))
150	149	oveq2d 7425	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (i · ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i · (ℑ‘𝐴)))
151	65, 66, 150	3eqtr3d 2781	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i · (ℑ‘𝐴)))
152	63, 151	oveq12d 7427	. . . . 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 14090	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈ ℝ)
154	153	recnd 11242	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈ ℂ)
155	2, 12	mulcld 11234	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ)
156	57, 155	mulcld 11234	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈ ℂ)
157	12	sqcld 14109	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) ∈ ℂ)
158	154, 156, 157	add32d 11441	. . . . 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 15063	. . . . 5 ⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))))
160	152, 158, 159	3eqtr4d 2783	. . . 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 2773	. . 3 ⊢ (𝐴 ∈ ℂ → (((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))↑2) = 𝐴)
162	20, 69	sqrtge0d 15367	. . . 4 ⊢ (𝐴 ∈ ℂ → 0 ≤ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
163	1, 10	crred 15178	. . . 4 ⊢ (𝐴 ∈ ℂ → (ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
164	162, 163	breqtrrd 5177	. . 3 ⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))))
165		reim 15056	. . . . . . . . . 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 2775	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
168	167	eqeq1d 2735	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 ↔ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0))
169		cnsqrt00 15339	. . . . . . . 8 ⊢ ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0))
170	21, 169	syl 17	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0))
171		half0 12439	. . . . . . . . 9 ⊢ (((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ ((abs‘𝐴) + (ℜ‘𝐴)) = 0))
172	55, 171	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ ((abs‘𝐴) + (ℜ‘𝐴)) = 0))
173	49, 50	addcomd 11416	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + (ℜ‘𝐴)) = ((ℜ‘𝐴) + (abs‘𝐴)))
174	173	eqeq1d 2735	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) = 0 ↔ ((ℜ‘𝐴) + (abs‘𝐴)) = 0))
175		addeq0 11637	. . . . . . . . 9 ⊢ (((ℜ‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (((ℜ‘𝐴) + (abs‘𝐴)) = 0 ↔ (ℜ‘𝐴) = -(abs‘𝐴)))
176	50, 49, 175	syl2anc 585	. . . . . . . 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 2740	. . . . . . . . . 10 ⊢ (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2))
181	180	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2)))
182		sqeqor 14180	. . . . . . . . . 10 ⊢ (((ℜ‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((ℜ‘𝐴) = (abs‘𝐴) ∨ (ℜ‘𝐴) = -(abs‘𝐴))))
183	50, 49, 182	syl2anc 585	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((ℜ‘𝐴) = (abs‘𝐴) ∨ (ℜ‘𝐴) = -(abs‘𝐴))))
184	103	eqeq1d 2735	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2) ↔ (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2)))
185		addid0 11633	. . . . . . . . . . 11 ⊢ ((((ℜ‘𝐴)↑2) ∈ ℂ ∧ ((ℑ‘𝐴)↑2) ∈ ℂ) → ((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2) ↔ ((ℑ‘𝐴)↑2) = 0))
186	99, 102, 185	syl2anc 585	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2) ↔ ((ℑ‘𝐴)↑2) = 0))
187		sqeq0 14085	. . . . . . . . . . 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 243	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴) = -(abs‘𝐴) → (ℑ‘𝐴) = 0))
192	191	ancld 552	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴) = -(abs‘𝐴) → ((ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0)))
193	178, 192	sylbid 239	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 → ((ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0)))
194		simp2 1138	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘𝐴) = -(abs‘𝐴))
195	194	oveq2d 7425	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) + (ℜ‘𝐴)) = ((abs‘𝐴) + -(abs‘𝐴)))
196	49	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (abs‘𝐴) ∈ ℂ)
197	196	negidd 11561	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) + -(abs‘𝐴)) = 0)
198	195, 197	eqtrd 2773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) + (ℜ‘𝐴)) = 0)
199	198	oveq1d 7424	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = (0 / 2))
200		2cn 12287	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℂ
201	200, 58	div0i 11948	. . . . . . . . . . . . . . . 16 ⊢ (0 / 2) = 0
202	199, 201	eqtrdi 2789	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0)
203	202	fveq2d 6896	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = (√‘0))
204		sqrt0 15188	. . . . . . . . . . . . . 14 ⊢ (√‘0) = 0
205	203, 204	eqtrdi 2789	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0)
206		simp3 1139	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℑ‘𝐴) = 0)
207		0red 11217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → 0 ∈ ℝ)
208	207	ltnrd 11348	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ¬ 0 < 0)
209	206, 208	eqnbrtrd 5167	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ¬ (ℑ‘𝐴) < 0)
210	209	iffalsed 4540	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → if((ℑ‘𝐴) < 0, -1, 1) = 1)
211	194	oveq2d 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) − (ℜ‘𝐴)) = ((abs‘𝐴) − -(abs‘𝐴)))
212	49, 49	subnegd 11578	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − -(abs‘𝐴)) = ((abs‘𝐴) + (abs‘𝐴)))
213	49	2timesd 12455	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ ℂ → (2 · (abs‘𝐴)) = ((abs‘𝐴) + (abs‘𝐴)))
214	212, 213	eqtr4d 2776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − -(abs‘𝐴)) = (2 · (abs‘𝐴)))
215	214	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) − -(abs‘𝐴)) = (2 · (abs‘𝐴)))
216	211, 215	eqtrd 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) − (ℜ‘𝐴)) = (2 · (abs‘𝐴)))
217	216	oveq1d 7424	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) = ((2 · (abs‘𝐴)) / 2))
218	49, 57, 59	divcan3d 11995	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) / 2) = (abs‘𝐴))
219	218	3ad2ant1 1134	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((2 · (abs‘𝐴)) / 2) = (abs‘𝐴))
220	217, 219	eqtrd 2773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) = (abs‘𝐴))
221	220	fveq2d 6896	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (√‘(abs‘𝐴)))
222	210, 221	oveq12d 7427	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (1 · (√‘(abs‘𝐴))))
223		absge0 15234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
224	17, 223	resqrtcld 15364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℝ)
225	224	recnd 11242	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℂ)
226	225	mullidd 11232	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (1 · (√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
227	226	3ad2ant1 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (1 · (√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
228	222, 227	eqtrd 2773	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (√‘(abs‘𝐴)))
229	228	oveq2d 7425	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (i · (√‘(abs‘𝐴))))
230	205, 229	oveq12d 7427	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (0 + (i · (√‘(abs‘𝐴)))))
231	4, 225	mulcld 11234	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (i · (√‘(abs‘𝐴))) ∈ ℂ)
232	231	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · (√‘(abs‘𝐴))) ∈ ℂ)
233	232	addlidd 11415	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (0 + (i · (√‘(abs‘𝐴)))) = (i · (√‘(abs‘𝐴))))
234	230, 233	eqtrd 2773	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i · (√‘(abs‘𝐴))))
235	234	oveq2d 7425	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i · (i · (√‘(abs‘𝐴)))))
236		ixi 11843	. . . . . . . . . . . . . 14 ⊢ (i · i) = -1
237	236	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (i · i) = -1)
238	237	oveq1d 7424	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((i · i) · (√‘(abs‘𝐴))) = (-1 · (√‘(abs‘𝐴))))
239	4, 4, 225	mulassd 11237	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((i · i) · (√‘(abs‘𝐴))) = (i · (i · (√‘(abs‘𝐴)))))
240	225	mulm1d 11666	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (-1 · (√‘(abs‘𝐴))) = -(√‘(abs‘𝐴)))
241	238, 239, 240	3eqtr3d 2781	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (i · (i · (√‘(abs‘𝐴)))) = -(√‘(abs‘𝐴)))
242	241	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · (i · (√‘(abs‘𝐴)))) = -(√‘(abs‘𝐴)))
243	235, 242	eqtrd 2773	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = -(√‘(abs‘𝐴)))
244	243	fveq2d 6896	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = (ℜ‘-(√‘(abs‘𝐴))))
245	224	renegcld 11641	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → -(√‘(abs‘𝐴)) ∈ ℝ)
246	245	rered 15171	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (ℜ‘-(√‘(abs‘𝐴))) = -(√‘(abs‘𝐴)))
247	246	3ad2ant1 1134	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘-(√‘(abs‘𝐴))) = -(√‘(abs‘𝐴)))
248	244, 247	eqtrd 2773	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = -(√‘(abs‘𝐴)))
249	17, 223	sqrtge0d 15367	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 0 ≤ (√‘(abs‘𝐴)))
250	224	le0neg2d 11786	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (0 ≤ (√‘(abs‘𝐴)) ↔ -(√‘(abs‘𝐴)) ≤ 0))
251	249, 250	mpbid 231	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → -(√‘(abs‘𝐴)) ≤ 0)
252	251	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → -(√‘(abs‘𝐴)) ≤ 0)
253	248, 252	eqbrtrd 5171	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) ≤ 0)
254	253	3expib 1123	. . . . 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 11234	. . . . 5 ⊢ (𝐴 ∈ ℂ → (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈ ℂ)
257	256	sqrtcvallem1 42382	. . . 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 231	. . 3 ⊢ (𝐴 ∈ ℂ → ¬ (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈ ℝ+)
259	13, 14, 161, 164, 258	eqsqrtd 15314	. 2 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (√‘𝐴))
260	259	eqcomd 2739	1 ⊢ (𝐴 ∈ ℂ → (√‘𝐴) = ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ifcif 4529   class class class wbr 5149  ‘cfv 6544  (class class class)co 7409  ℂcc 11108  ℝcr 11109  0cc0 11110  1c1 11111  ici 11112   + caddc 11113   · cmul 11115   < clt 11248   ≤ cle 11249   − cmin 11444  -cneg 11445   / cdiv 11871  2c2 12267  ℝ⁺crp 12974  ↑cexp 14027  ℜcre 15044  ℑcim 15045  √csqrt 15180  abscabs 15181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-sup 9437  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-seq 13967  df-exp 14028  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183

This theorem is referenced by:  sqrtcval2  42393  resqrtval  42394  imsqrtval  42395