Theorem sqrtcval

Description: Explicit formula for the complex square root in terms of the square root of non-negative reals. The right-hand side is decomposed into real and imaginary parts in the format expected by crrei and crimi . This formula can be found in section 3.7.27 of Handbook of Mathematical Functions, ed. M. Abramowitz and I. A. Stegun (1965, Dover Press). (Contributed by RP, 18-May-2024)

	Ref	Expression
Assertion	sqrtcval	$$⊢A\in ℂ\to \sqrt{A}=\sqrt{\frac{\left|A\right|+\Re \left(A\right)}{2}}+\mathrm{i}if\left(\Im \left(A\right)<0,-1,1\right)\sqrt{\frac{\left|A\right|-\Re \left(A\right)}{2}}$$

Proof

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