Theorem sqrtcval 44833

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 15388 and crimi 15389. 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 44832	. . . . 5 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℝ)
2	1	recnd 11364	. . . 4 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℂ)
3		ax-icn 11286	. . . . . 6 ⊢ i ∈ ℂ
4	3	a1i 11	. . . . 5 ⊢ (𝐴 ∈ ℂ → i ∈ ℂ)
5		neg1rr 12333	. . . . . . . . 9 ⊢ -1 ∈ ℝ
6		1re 11335	. . . . . . . . 9 ⊢ 1 ∈ ℝ
7	5, 6	ifcli 4533	. . . . . . . 8 ⊢ if((ℑ‘𝐴) < 0, -1, 1) ∈ ℝ
8	7	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -1, 1) ∈ ℝ)
9		sqrtcvallem3 44830	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℝ)
10	8, 9	remulcld 11366	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℝ)
11	10	recnd 11364	. . . . 5 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) ∈ ℂ)
12	4, 11	mulcld 11356	. . . 4 ⊢ (𝐴 ∈ ℂ → (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) ∈ ℂ)
13	2, 12	addcld 11355	. . 3 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ)
14		id 23	. . 3 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
15		binom2 14388	. . . . 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 596	. . . 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 15474	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)
18		recl 15306	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
19	17, 18	readdcld 11365	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℝ)
20	19	rehalfcld 12620	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) ∈ ℝ)
21	20	recnd 11364	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) ∈ ℂ)
22	21	sqsqrtd 15638	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) + (ℜ‘𝐴)) / 2))
23	4, 11	sqmuld 14328	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) = ((i↑2) · ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2)))
24		i2 14373	. . . . . . . . . . 11 ⊢ (i↑2) = -1
25	24	a1i 11	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (i↑2) = -1)
26	8	recnd 11364	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -1, 1) ∈ ℂ)
27	9	recnd 11364	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℂ)
28	26, 27	sqmuld 14328	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2) = ((if((ℑ‘𝐴) < 0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2)))
29		ovif 7541	. . . . . . . . . . . . . 14 ⊢ (if((ℑ‘𝐴) < 0, -1, 1)↑2) = if((ℑ‘𝐴) < 0, ( -1↑2), (1↑2))
30		neg1sqe1 14366	. . . . . . . . . . . . . . 15 ⊢ ( -1↑2) = 1
31		sq1 14365	. . . . . . . . . . . . . . 15 ⊢ (1↑2) = 1
32		ifeq12 4504	. . . . . . . . . . . . . . 15 ⊢ ((( -1↑2) = 1 ∧ (1↑2) = 1) → if((ℑ‘𝐴) < 0, ( -1↑2), (1↑2)) = if((ℑ‘𝐴) < 0, 1, 1))
33	30, 31, 32	mp2an 705	. . . . . . . . . . . . . 14 ⊢ if((ℑ‘𝐴) < 0, ( -1↑2), (1↑2)) = if((ℑ‘𝐴) < 0, 1, 1)
34		ifid 4526	. . . . . . . . . . . . . 14 ⊢ if((ℑ‘𝐴) < 0, 1, 1) = 1
35	29, 33, 34	3eqtri 2790	. . . . . . . . . . . . 13 ⊢ (if((ℑ‘𝐴) < 0, -1, 1)↑2) = 1
36	35	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1)↑2) = 1)
37	17, 18	resubcld 11771	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − (ℜ‘𝐴)) ∈ ℝ)
38	37	rehalfcld 12620	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) ∈ ℝ)
39	38	recnd 11364	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) ∈ ℂ)
40	39	sqsqrtd 15638	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
41	36, 40	oveq12d 7461	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1)↑2) · ((√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))↑2)) = (1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
42	39	mullidd 11354	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
43	28, 41, 42	3eqtrd 2802	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2) = (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
44	25, 43	oveq12d 7461	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((i↑2) · ((if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))↑2)) = ( -1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
45	39	mulm1d 11795	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ( -1 · (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = -(((abs‘𝐴) − (ℜ‘𝐴)) / 2))
46	23, 44, 45	3eqtrd 2802	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) = -(((abs‘𝐴) − (ℜ‘𝐴)) / 2))
47	22, 46	oveq12d 7461	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) + -(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
48	21, 39	negsubd 11702	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) + -(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) − (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
49	17	recnd 11364	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℂ)
50	18	recnd 11364	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℂ)
51	49, 50, 50	pnncand 11735	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) = ((ℜ‘𝐴) + (ℜ‘𝐴)))
52	50	2timesd 12616	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (2 · (ℜ‘𝐴)) = ((ℜ‘𝐴) + (ℜ‘𝐴)))
53	51, 52	eqtr4d 2801	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) = (2 · (ℜ‘𝐴)))
54	53	oveq1d 7458	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) / 2) = ((2 · (ℜ‘𝐴)) / 2))
55	19	recnd 11364	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℂ)
56	37	recnd 11364	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − (ℜ‘𝐴)) ∈ ℂ)
57		2cnd 12448	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℂ)
58		2ne0 12476	. . . . . . . . . 10 ⊢ 2 ≠ 0
59	58	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 2 ≠ 0)
60	55, 56, 57, 59	divsubdird 12159	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) − ((abs‘𝐴) − (ℜ‘𝐴))) / 2) = ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) − (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
61	50, 57, 59	divcan3d 12125	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((2 · (ℜ‘𝐴)) / 2) = (ℜ‘𝐴))
62	54, 60, 61	3eqtr3d 2806	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) − (((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (ℜ‘𝐴))
63	47, 48, 62	3eqtrd 2802	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) + ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2)) = (ℜ‘𝐴))
64	57, 2	mulcld 11356	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) ∈ ℂ)
65	64, 4, 11	mul12d 11546	. . . . . . 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 11359	. . . . . . 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 11359	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))
68	2, 26, 27	mul12d 11546	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))
69		sqrtcvallem4 44831	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2))
70		halfnneg2 12604	. . . . . . . . . . . . . . . . 17 ⊢ (((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℝ → (0 ≤ ((abs‘𝐴) + (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
71	19, 70	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (0 ≤ ((abs‘𝐴) + (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
72	69, 71	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → 0 ≤ ((abs‘𝐴) + (ℜ‘𝐴)))
73		2rp 13152	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ+
74	73	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℝ+)
75	19, 72, 74	sqrtdivd 15620	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)))
76		sqrtcvallem2 44829	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
77		halfnneg2 12604	. . . . . . . . . . . . . . . . 17 ⊢ (((abs‘𝐴) − (ℜ‘𝐴)) ∈ ℝ → (0 ≤ ((abs‘𝐴) − (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
78	37, 77	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (0 ≤ ((abs‘𝐴) − (ℜ‘𝐴)) ↔ 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2)))
79	76, 78	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → 0 ≤ ((abs‘𝐴) − (ℜ‘𝐴)))
80	37, 79, 74	sqrtdivd 15620	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = ((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2)))
81	75, 80	oveq12d 7461	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) · ((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2))))
82	19, 72	resqrtcld 15614	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℝ)
83	82	recnd 11364	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘((abs‘𝐴) + (ℜ‘𝐴))) ∈ ℂ)
84		2re 12444	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
85	84	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℝ)
86		0le2 12472	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≤ 2
87	86	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → 0 ≤ 2)
88	85, 87	resqrtcld 15614	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘2) ∈ ℝ)
89	88	recnd 11364	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘2) ∈ ℂ)
90	37, 79	resqrtcld 15614	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℝ)
91	90	recnd 11364	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘((abs‘𝐴) − (ℜ‘𝐴))) ∈ ℂ)
92		sqrt00 15459	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) = 0 ↔ 2 = 0))
93	84, 86, 92	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((√‘2) = 0 ↔ 2 = 0)
94	93	necon3bii 3011	. . . . . . . . . . . . . . . 16 ⊢ ((√‘2) ≠ 0 ↔ 2 ≠ 0)
95	58, 94	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ (√‘2) ≠ 0
96	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (√‘2) ≠ 0)
97	83, 89, 91, 89, 96, 96	divmuldivd 12161	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (((√‘((abs‘𝐴) + (ℜ‘𝐴))) / (√‘2)) · ((√‘((abs‘𝐴) − (ℜ‘𝐴))) / (√‘2))) = (((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) · (√‘2))))
98	18	resqcld 14295	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴)↑2) ∈ ℝ)
99	98	recnd 11364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴)↑2) ∈ ℂ)
100		imcl 15307	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ)
101	100	resqcld 14295	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴)↑2) ∈ ℝ)
102	101	recnd 11364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴)↑2) ∈ ℂ)
103		absvalsq2 15477	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))
104	99, 102, 103	mvrladdd 11755	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) − ((ℜ‘𝐴)↑2)) = ((ℑ‘𝐴)↑2))
105		subsq 14381	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs‘𝐴) ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℂ) → (((abs‘𝐴)↑2) − ((ℜ‘𝐴)↑2)) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))
106	49, 50, 105	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) − ((ℜ‘𝐴)↑2)) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))
107	104, 106	eqtr3d 2800	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴)↑2) = (((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴))))
108	107	fveq2d 6912	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘((ℑ‘𝐴)↑2)) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))))
109	100	absred 15613	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (abs‘(ℑ‘𝐴)) = (√‘((ℑ‘𝐴)↑2)))
110		reabsifneg 44824	. . . . . . . . . . . . . . . . 17 ⊢ ((ℑ‘𝐴) ∈ ℝ → (abs‘(ℑ‘𝐴)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
111	100, 110	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (abs‘(ℑ‘𝐴)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
112	109, 111	eqtr3d 2800	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘((ℑ‘𝐴)↑2)) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
113	19, 72, 37, 79	sqrtmuld 15621	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) · ((abs‘𝐴) − (ℜ‘𝐴)))) = ((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))))
114	108, 112, 113	3eqtr3rd 2807	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))) = if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)))
115		remsqsqrt 15452	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → ((√‘2) · (√‘2)) = 2)
116	84, 86, 115	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ ((√‘2) · (√‘2)) = 2
117	116	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((√‘2) · (√‘2)) = 2)
118	114, 117	oveq12d 7461	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (((√‘((abs‘𝐴) + (ℜ‘𝐴))) · (√‘((abs‘𝐴) − (ℜ‘𝐴)))) / ((√‘2) · (√‘2))) = (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))
119	81, 97, 118	3eqtrd 2802	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))
120	119	oveq2d 7459	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))
121	68, 120	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))
122	121	oveq2d 7459	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (2 · (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))))
123	100	renegcld 11770	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → -(ℑ‘𝐴) ∈ ℝ)
124	123, 100	ifcld 4532	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) ∈ ℝ)
125	124	recnd 11364	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) ∈ ℂ)
126	26, 125, 57, 59	divassd 12155	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) / 2) = (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)))
127		ovif12 7543	. . . . . . . . . . . . . 14 ⊢ (if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) = if((ℑ‘𝐴) < 0, ( -1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴)))
128	5	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → -1 ∈ ℝ)
129	128	recnd 11364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → -1 ∈ ℂ)
130	100	recnd 11364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℂ)
131	129, 129, 130	mulassd 11359	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (( -1 · -1) · (ℑ‘𝐴)) = ( -1 · ( -1 · (ℑ‘𝐴))))
132		neg1mulneg1e1 12585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( -1 · -1) = 1
133	132	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → ( -1 · -1) = 1)
134	133	oveq1d 7458	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (( -1 · -1) · (ℑ‘𝐴)) = (1 · (ℑ‘𝐴)))
135	130	mullidd 11354	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (1 · (ℑ‘𝐴)) = (ℑ‘𝐴))
136	134, 135	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (( -1 · -1) · (ℑ‘𝐴)) = (ℑ‘𝐴))
137	130	mulm1d 11795	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → ( -1 · (ℑ‘𝐴)) = -(ℑ‘𝐴))
138	137	oveq2d 7459	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → ( -1 · ( -1 · (ℑ‘𝐴))) = ( -1 · -(ℑ‘𝐴)))
139	131, 136, 138	3eqtr3rd 2807	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → ( -1 · -(ℑ‘𝐴)) = (ℑ‘𝐴))
140	139	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) < 0) → ( -1 · -(ℑ‘𝐴)) = (ℑ‘𝐴))
141	135	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ ¬ (ℑ‘𝐴) < 0) → (1 · (ℑ‘𝐴)) = (ℑ‘𝐴))
142	140, 141	ifeqda 4522	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → if((ℑ‘𝐴) < 0, ( -1 · -(ℑ‘𝐴)), (1 · (ℑ‘𝐴))) = (ℑ‘𝐴))
143	127, 142	eqtrid 2810	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) = (ℑ‘𝐴))
144	143	oveq1d 7458	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((if((ℑ‘𝐴) < 0, -1, 1) · if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴))) / 2) = ((ℑ‘𝐴) / 2))
145	126, 144	eqtr3d 2800	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2)) = ((ℑ‘𝐴) / 2))
146	145	oveq2d 7459	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (2 · (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))) = (2 · ((ℑ‘𝐴) / 2)))
147	130, 57, 59	divcan2d 12122	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (2 · ((ℑ‘𝐴) / 2)) = (ℑ‘𝐴))
148	146, 147	eqtrd 2798	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (2 · (if((ℑ‘𝐴) < 0, -1, 1) · (if((ℑ‘𝐴) < 0, -(ℑ‘𝐴), (ℑ‘𝐴)) / 2))) = (ℑ‘𝐴))
149	67, 122, 148	3eqtrd 2802	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (ℑ‘𝐴))
150	149	oveq2d 7459	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (i · ((2 · (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))) · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i · (ℑ‘𝐴)))
151	65, 66, 150	3eqtr3d 2806	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i · (ℑ‘𝐴)))
152	63, 151	oveq12d 7461	. . . . 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 14295	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈ ℝ)
154	153	recnd 11364	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2))↑2) ∈ ℂ)
155	2, 12	mulcld 11356	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) ∈ ℂ)
156	57, 155	mulcld 11356	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (2 · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) · (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈ ℂ)
157	12	sqcld 14314	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))↑2) ∈ ℂ)
158	154, 156, 157	add32d 11565	. . . . 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 15312	. . . . 5 ⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))))
160	152, 158, 159	3eqtr4d 2808	. . . 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 2798	. . 3 ⊢ (𝐴 ∈ ℂ → (((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))↑2) = 𝐴)
162	20, 69	sqrtge0d 15617	. . . 4 ⊢ (𝐴 ∈ ℂ → 0 ≤ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
163	1, 10	crred 15427	. . . 4 ⊢ (𝐴 ∈ ℂ → (ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
164	162, 163	breqtrrd 5136	. . 3 ⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))))
165		reim 15305	. . . . . . . . . 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 18	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (ℜ‘((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))))
167	166, 163	eqtr3d 2800	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
168	167	eqeq1d 2765	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 ↔ (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0))
169		cnsqrt00 15589	. . . . . . . 8 ⊢ ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0))
170	21, 169	syl 18	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0 ↔ (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0))
171		half0 12601	. . . . . . . . 9 ⊢ (((abs‘𝐴) + (ℜ‘𝐴)) ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ ((abs‘𝐴) + (ℜ‘𝐴)) = 0))
172	55, 171	syl 18	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ ((abs‘𝐴) + (ℜ‘𝐴)) = 0))
173	49, 50	addcomd 11539	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) + (ℜ‘𝐴)) = ((ℜ‘𝐴) + (abs‘𝐴)))
174	173	eqeq1d 2765	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴) + (ℜ‘𝐴)) = 0 ↔ ((ℜ‘𝐴) + (abs‘𝐴)) = 0))
175		addeq0 11766	. . . . . . . . 9 ⊢ (((ℜ‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (((ℜ‘𝐴) + (abs‘𝐴)) = 0 ↔ (ℜ‘𝐴) = -(abs‘𝐴)))
176	50, 49, 175	syl2anc 596	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴) + (abs‘𝐴)) = 0 ↔ (ℜ‘𝐴) = -(abs‘𝐴)))
177	172, 174, 176	3bitrd 308	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0 ↔ (ℜ‘𝐴) = -(abs‘𝐴)))
178	168, 170, 177	3bitrd 308	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 ↔ (ℜ‘𝐴) = -(abs‘𝐴)))
179		olc 882	. . . . . . . 8 ⊢ ((ℜ‘𝐴) = -(abs‘𝐴) → ((ℜ‘𝐴) = (abs‘𝐴) ∨ (ℜ‘𝐴) = -(abs‘𝐴)))
180		eqcom 2770	. . . . . . . . . 10 ⊢ (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2))
181	180	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2)))
182		sqeqor 14387	. . . . . . . . . 10 ⊢ (((ℜ‘𝐴) ∈ ℂ ∧ (abs‘𝐴) ∈ ℂ) → (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((ℜ‘𝐴) = (abs‘𝐴) ∨ (ℜ‘𝐴) = -(abs‘𝐴))))
183	50, 49, 182	syl2anc 596	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴)↑2) = ((abs‘𝐴)↑2) ↔ ((ℜ‘𝐴) = (abs‘𝐴) ∨ (ℜ‘𝐴) = -(abs‘𝐴))))
184	103	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2) ↔ (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2)))
185		addid0 11762	. . . . . . . . . . 11 ⊢ ((((ℜ‘𝐴)↑2) ∈ ℂ ∧ ((ℑ‘𝐴)↑2) ∈ ℂ) → ((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2) ↔ ((ℑ‘𝐴)↑2) = 0))
186	99, 102, 185	syl2anc 596	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)) = ((ℜ‘𝐴)↑2) ↔ ((ℑ‘𝐴)↑2) = 0))
187		sqeq0 14290	. . . . . . . . . . 11 ⊢ ((ℑ‘𝐴) ∈ ℂ → (((ℑ‘𝐴)↑2) = 0 ↔ (ℑ‘𝐴) = 0))
188	130, 187	syl 18	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((ℑ‘𝐴)↑2) = 0 ↔ (ℑ‘𝐴) = 0))
189	184, 186, 188	3bitrd 308	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((abs‘𝐴)↑2) = ((ℜ‘𝐴)↑2) ↔ (ℑ‘𝐴) = 0))
190	181, 183, 189	3bitr3d 312	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴) = (abs‘𝐴) ∨ (ℜ‘𝐴) = -(abs‘𝐴)) ↔ (ℑ‘𝐴) = 0))
191	179, 190	imbitrid 247	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴) = -(abs‘𝐴) → (ℑ‘𝐴) = 0))
192	191	ancld 560	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴) = -(abs‘𝐴) → ((ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0)))
193	178, 192	sylbid 243	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((ℑ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = 0 → ((ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0)))
194		simp2 1155	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘𝐴) = -(abs‘𝐴))
195	194	oveq2d 7459	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) + (ℜ‘𝐴)) = ((abs‘𝐴) + -(abs‘𝐴)))
196	49	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (abs‘𝐴) ∈ ℂ)
197	196	negidd 11686	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) + -(abs‘𝐴)) = 0)
198	195, 197	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) + (ℜ‘𝐴)) = 0)
199	198	oveq1d 7458	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = (0 / 2))
200		2cn 12445	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℂ
201	200, 58	div0i 12078	. . . . . . . . . . . . . . . 16 ⊢ (0 / 2) = 0
202	199, 201	eqtrdi 2814	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) + (ℜ‘𝐴)) / 2) = 0)
203	202	fveq2d 6912	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = (√‘0))
204		sqrt0 15437	. . . . . . . . . . . . . 14 ⊢ (√‘0) = 0
205	203, 204	eqtrdi 2814	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) = 0)
206		simp3 1156	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℑ‘𝐴) = 0)
207		0red 11338	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → 0 ∈ ℝ)
208	207	ltnrd 11471	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ¬ 0 < 0)
209	206, 208	eqnbrtrd 5126	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ¬ (ℑ‘𝐴) < 0)
210	209	iffalsed 4496	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → if((ℑ‘𝐴) < 0, -1, 1) = 1)
211	194	oveq2d 7459	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) − (ℜ‘𝐴)) = ((abs‘𝐴) − -(abs‘𝐴)))
212	49, 49	subnegd 11703	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − -(abs‘𝐴)) = ((abs‘𝐴) + (abs‘𝐴)))
213	49	2timesd 12616	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ ℂ → (2 · (abs‘𝐴)) = ((abs‘𝐴) + (abs‘𝐴)))
214	212, 213	eqtr4d 2801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴) − -(abs‘𝐴)) = (2 · (abs‘𝐴)))
215	214	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) − -(abs‘𝐴)) = (2 · (abs‘𝐴)))
216	211, 215	eqtrd 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((abs‘𝐴) − (ℜ‘𝐴)) = (2 · (abs‘𝐴)))
217	216	oveq1d 7458	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) = ((2 · (abs‘𝐴)) / 2))
218	49, 57, 59	divcan3d 12125	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → ((2 · (abs‘𝐴)) / 2) = (abs‘𝐴))
219	218	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((2 · (abs‘𝐴)) / 2) = (abs‘𝐴))
220	217, 219	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (((abs‘𝐴) − (ℜ‘𝐴)) / 2) = (abs‘𝐴))
221	220	fveq2d 6912	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) = (√‘(abs‘𝐴)))
222	210, 221	oveq12d 7461	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (1 · (√‘(abs‘𝐴))))
223		absge0 15483	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))
224	17, 223	resqrtcld 15614	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℝ)
225	224	recnd 11364	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (√‘(abs‘𝐴)) ∈ ℂ)
226	225	mullidd 11354	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (1 · (√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
227	226	3ad2ant1 1151	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (1 · (√‘(abs‘𝐴))) = (√‘(abs‘𝐴)))
228	222, 227	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))) = (√‘(abs‘𝐴)))
229	228	oveq2d 7459	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))) = (i · (√‘(abs‘𝐴))))
230	205, 229	oveq12d 7461	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (0 + (i · (√‘(abs‘𝐴)))))
231	4, 225	mulcld 11356	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (i · (√‘(abs‘𝐴))) ∈ ℂ)
232	231	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · (√‘(abs‘𝐴))) ∈ ℂ)
233	232	addlidd 11538	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (0 + (i · (√‘(abs‘𝐴)))) = (i · (√‘(abs‘𝐴))))
234	230, 233	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (i · (√‘(abs‘𝐴))))
235	234	oveq2d 7459	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = (i · (i · (√‘(abs‘𝐴)))))
236		ixi 11972	. . . . . . . . . . . . . 14 ⊢ (i · i) = -1
237	236	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (i · i) = -1)
238	237	oveq1d 7458	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((i · i) · (√‘(abs‘𝐴))) = ( -1 · (√‘(abs‘𝐴))))
239	4, 4, 225	mulassd 11359	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((i · i) · (√‘(abs‘𝐴))) = (i · (i · (√‘(abs‘𝐴)))))
240	225	mulm1d 11795	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ( -1 · (√‘(abs‘𝐴))) = -(√‘(abs‘𝐴)))
241	238, 239, 240	3eqtr3d 2806	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (i · (i · (√‘(abs‘𝐴)))) = -(√‘(abs‘𝐴)))
242	241	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · (i · (√‘(abs‘𝐴)))) = -(√‘(abs‘𝐴)))
243	235, 242	eqtrd 2798	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) = -(√‘(abs‘𝐴)))
244	243	fveq2d 6912	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = (ℜ‘ -(√‘(abs‘𝐴))))
245	224	renegcld 11770	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → -(√‘(abs‘𝐴)) ∈ ℝ)
246	245	rered 15420	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (ℜ‘ -(√‘(abs‘𝐴))) = -(√‘(abs‘𝐴)))
247	246	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘ -(√‘(abs‘𝐴))) = -(√‘(abs‘𝐴)))
248	244, 247	eqtrd 2798	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) = -(√‘(abs‘𝐴)))
249	17, 223	sqrtge0d 15617	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → 0 ≤ (√‘(abs‘𝐴)))
250	224	le0neg2d 11915	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (0 ≤ (√‘(abs‘𝐴)) ↔ -(√‘(abs‘𝐴)) ≤ 0))
251	249, 250	mpbid 235	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → -(√‘(abs‘𝐴)) ≤ 0)
252	251	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → -(√‘(abs‘𝐴)) ≤ 0)
253	248, 252	eqbrtrd 5130	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) ≤ 0)
254	253	3expib 1140	. . . . 5 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴) = -(abs‘𝐴) ∧ (ℑ‘𝐴) = 0) → (ℜ‘(i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))) ≤ 0))
255	193, 254	syld 48	. . . 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 11356	. . . . 5 ⊢ (𝐴 ∈ ℂ → (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈ ℂ)
257	256	sqrtcvallem1 44823	. . . 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 235	. . 3 ⊢ (𝐴 ∈ ℂ → ¬ (i · ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))) ∈ ℝ+)
259	13, 14, 161, 164, 258	eqsqrtd 15564	. 2 ⊢ (𝐴 ∈ ℂ → ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))) = (√‘𝐴))
260	259	eqcomd 2769	1 ⊢ (𝐴 ∈ ℂ → (√‘𝐴) = ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ifcif 4485   class class class wbr 5106  ‘cfv 6558  (class class class)co 7443  ℂcc 11225  ℝcr 11226  0cc0 11227  1c1 11228  ici 11229   + caddc 11230   · cmul 11232   < clt 11370   ≤ cle 11371   − cmin 11568   -cneg 11569   / cdiv 12000  2c2 12424  ℝ⁺crp 13147  ↑cexp 14231  ℜcre 15293  ℑcim 15294  √csqrt 15429  abscabs 15430

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304  ax-pre-sup 11305

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-sup 9461  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-div 12001  df-nn 12363  df-2 12432  df-3 12433  df-n0 12634  df-z 12721  df-uz 12993  df-rp 13148  df-seq 14172  df-exp 14232  df-cj 15295  df-re 15296  df-im 15297  df-sqrt 15431  df-abs 15432

This theorem is used by:  sqrtcval2  44834  resqrtval  44835  imsqrtval  44836