Theorem sqreulem

Description: Lemma for sqreu : write a general complex square root in terms of the square root function over nonnegative reals. (Contributed by Mario Carneiro, 9-Jul-2013)

	Ref	Expression
Hypothesis	sqrteulem.1	$$⊢B=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)$$
Assertion	sqreulem	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left(B^2=A\wedge 0\le \Re \left(B\right)\wedge \mathrm{i}B\notin {ℝ}^{+}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sqrteulem.1	$$⊢B=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)$$
2	1	oveq1i	$$⊢B^2={\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}^2$$
3		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
4		absge0	$$⊢A\in ℂ\to 0\le \left|A\right|$$
5		resqrtcl	$$⊢\left(\left|A\right|\in ℝ\wedge 0\le \left|A\right|\right)\to \sqrt{\left|A\right|}\in ℝ$$
6	3 4 5	syl2anc	$$⊢A\in ℂ\to \sqrt{\left|A\right|}\in ℝ$$
7	6	recnd	$$⊢A\in ℂ\to \sqrt{\left|A\right|}\in ℂ$$
8	7	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \sqrt{\left|A\right|}\in ℂ$$
9	3	recnd	$$⊢A\in ℂ\to \left|A\right|\in ℂ$$
10		addcl	$$⊢\left(\left|A\right|\in ℂ\wedge A\in ℂ\right)\to \left|A\right|+A\in ℂ$$
11	9 10	mpancom	$$⊢A\in ℂ\to \left|A\right|+A\in ℂ$$
12	11	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|A\right|+A\in ℂ$$
13		abscl	$$⊢\left|A\right|+A\in ℂ\to \left|\left|A\right|+A\right|\in ℝ$$
14	11 13	syl	$$⊢A\in ℂ\to \left|\left|A\right|+A\right|\in ℝ$$
15	14	recnd	$$⊢A\in ℂ\to \left|\left|A\right|+A\right|\in ℂ$$
16	15	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|\left|A\right|+A\right|\in ℂ$$
17	11	abs00ad	$$⊢A\in ℂ\to \left(\left|\left|A\right|+A\right|=0\leftrightarrow \left|A\right|+A=0\right)$$
18	17	necon3bid	$$⊢A\in ℂ\to \left(\left|\left|A\right|+A\right|\ne 0\leftrightarrow \left|A\right|+A\ne 0\right)$$
19	18	biimpar	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|\left|A\right|+A\right|\ne 0$$
20	12 16 19	divcld	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\in ℂ$$
21	8 20	sqmuld	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to {\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}^2={\sqrt{\left|A\right|}}^2{\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}^2$$
22	2 21	eqtrid	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to B^2={\sqrt{\left|A\right|}}^2{\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}^2$$
23	3	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|A\right|\in ℝ$$
24	4	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to 0\le \left|A\right|$$
25		resqrtth	$$⊢\left(\left|A\right|\in ℝ\wedge 0\le \left|A\right|\right)\to {\sqrt{\left|A\right|}}^2=\left|A\right|$$
26	23 24 25	syl2anc	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to {\sqrt{\left|A\right|}}^2=\left|A\right|$$
27	12 16 19	sqdivd	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to {\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}^2=\frac{{\left(\left|A\right|+A\right)}^2}{{\left|\left|A\right|+A\right|}^2}$$
28		absvalsq	$$⊢A\in ℂ\to {\left|A\right|}^2=A\bar{A}$$
29		2cn	$$⊢2\in ℂ$$
30		mulass	$$⊢\left(2\in ℂ\wedge \left|A\right|\in ℂ\wedge A\in ℂ\right)\to 2\left|A\right|A=2\left|A\right|A$$
31	29 30	mp3an1	$$⊢\left(\left|A\right|\in ℂ\wedge A\in ℂ\right)\to 2\left|A\right|A=2\left|A\right|A$$
32	9 31	mpancom	$$⊢A\in ℂ\to 2\left|A\right|A=2\left|A\right|A$$
33		mulcl	$$⊢\left(2\in ℂ\wedge \left|A\right|\in ℂ\right)\to 2\left|A\right|\in ℂ$$
34	29 9 33	sylancr	$$⊢A\in ℂ\to 2\left|A\right|\in ℂ$$
35		mulcom	$$⊢\left(2\left|A\right|\in ℂ\wedge A\in ℂ\right)\to 2\left|A\right|A=A2\left|A\right|$$
36	34 35	mpancom	$$⊢A\in ℂ\to 2\left|A\right|A=A2\left|A\right|$$
37	32 36	eqtr3d	$$⊢A\in ℂ\to 2\left|A\right|A=A2\left|A\right|$$
38	28 37	oveq12d	$$⊢A\in ℂ\to {\left|A\right|}^2+2\left|A\right|A=A\bar{A}+A2\left|A\right|$$
39		cjcl	$$⊢A\in ℂ\to \bar{A}\in ℂ$$
40		adddi	$$⊢\left(A\in ℂ\wedge \bar{A}\in ℂ\wedge 2\left|A\right|\in ℂ\right)\to A\left(\bar{A}+2\left|A\right|\right)=A\bar{A}+A2\left|A\right|$$
41	39 34 40	mpd3an23	$$⊢A\in ℂ\to A\left(\bar{A}+2\left|A\right|\right)=A\bar{A}+A2\left|A\right|$$
42	38 41	eqtr4d	$$⊢A\in ℂ\to {\left|A\right|}^2+2\left|A\right|A=A\left(\bar{A}+2\left|A\right|\right)$$
43		sqval	$$⊢A\in ℂ\to A^2=AA$$
44	42 43	oveq12d	$$⊢A\in ℂ\to {\left|A\right|}^2+2\left|A\right|A+A^2=A\left(\bar{A}+2\left|A\right|\right)+AA$$
45		binom2	$$⊢\left(\left|A\right|\in ℂ\wedge A\in ℂ\right)\to {\left(\left|A\right|+A\right)}^2={\left|A\right|}^2+2\left|A\right|A+A^2$$
46	9 45	mpancom	$$⊢A\in ℂ\to {\left(\left|A\right|+A\right)}^2={\left|A\right|}^2+2\left|A\right|A+A^2$$
47		id	$$⊢A\in ℂ\to A\in ℂ$$
48	39 34	addcld	$$⊢A\in ℂ\to \bar{A}+2\left|A\right|\in ℂ$$
49	47 48 47	adddid	$$⊢A\in ℂ\to A\left(\bar{A}+2\left|A\right|+A\right)=A\left(\bar{A}+2\left|A\right|\right)+AA$$
50	44 46 49	3eqtr4d	$$⊢A\in ℂ\to {\left(\left|A\right|+A\right)}^2=A\left(\bar{A}+2\left|A\right|+A\right)$$
51	9 34	mulcld	$$⊢A\in ℂ\to \left|A\right|2\left|A\right|\in ℂ$$
52	9 39	mulcld	$$⊢A\in ℂ\to \left|A\right|\bar{A}\in ℂ$$
53	51 52	addcomd	$$⊢A\in ℂ\to \left|A\right|2\left|A\right|+\left|A\right|\bar{A}=\left|A\right|\bar{A}+\left|A\right|2\left|A\right|$$
54	9 9	mulcld	$$⊢A\in ℂ\to \left|A\right|\left|A\right|\in ℂ$$
55	54	2timesd	$$⊢A\in ℂ\to 2\left|A\right|\left|A\right|=\left|A\right|\left|A\right|+\left|A\right|\left|A\right|$$
56		mul12	$$⊢\left(2\in ℂ\wedge \left|A\right|\in ℂ\wedge \left|A\right|\in ℂ\right)\to 2\left|A\right|\left|A\right|=\left|A\right|2\left|A\right|$$
57	29 9 9 56	mp3an2i	$$⊢A\in ℂ\to 2\left|A\right|\left|A\right|=\left|A\right|2\left|A\right|$$
58	9	sqvald	$$⊢A\in ℂ\to {\left|A\right|}^2=\left|A\right|\left|A\right|$$
59		mulcom	$$⊢\left(A\in ℂ\wedge \bar{A}\in ℂ\right)\to A\bar{A}=\bar{A}A$$
60	39 59	mpdan	$$⊢A\in ℂ\to A\bar{A}=\bar{A}A$$
61	28 58 60	3eqtr3d	$$⊢A\in ℂ\to \left|A\right|\left|A\right|=\bar{A}A$$
62	61	oveq2d	$$⊢A\in ℂ\to \left|A\right|\left|A\right|+\left|A\right|\left|A\right|=\left|A\right|\left|A\right|+\bar{A}A$$
63	55 57 62	3eqtr3rd	$$⊢A\in ℂ\to \left|A\right|\left|A\right|+\bar{A}A=\left|A\right|2\left|A\right|$$
64	63	oveq1d	$$⊢A\in ℂ\to \left|A\right|\left|A\right|+\bar{A}A+\left|A\right|\bar{A}=\left|A\right|2\left|A\right|+\left|A\right|\bar{A}$$
65	9 39 34	adddid	$$⊢A\in ℂ\to \left|A\right|\left(\bar{A}+2\left|A\right|\right)=\left|A\right|\bar{A}+\left|A\right|2\left|A\right|$$
66	53 64 65	3eqtr4d	$$⊢A\in ℂ\to \left|A\right|\left|A\right|+\bar{A}A+\left|A\right|\bar{A}=\left|A\right|\left(\bar{A}+2\left|A\right|\right)$$
67	66	oveq1d	$$⊢A\in ℂ\to \left(\left|A\right|\left|A\right|+\bar{A}A\right)+\left|A\right|\bar{A}+\left|A\right|A=\left|A\right|\left(\bar{A}+2\left|A\right|\right)+\left|A\right|A$$
68		cjadd	$$⊢\left(\left|A\right|\in ℂ\wedge A\in ℂ\right)\to \overline{\left|A\right|+A}=\overline{\left|A\right|}+\bar{A}$$
69	9 68	mpancom	$$⊢A\in ℂ\to \overline{\left|A\right|+A}=\overline{\left|A\right|}+\bar{A}$$
70	3	cjred	$$⊢A\in ℂ\to \overline{\left|A\right|}=\left|A\right|$$
71	70	oveq1d	$$⊢A\in ℂ\to \overline{\left|A\right|}+\bar{A}=\left|A\right|+\bar{A}$$
72	69 71	eqtrd	$$⊢A\in ℂ\to \overline{\left|A\right|+A}=\left|A\right|+\bar{A}$$
73	72	oveq2d	$$⊢A\in ℂ\to \left(\left|A\right|+A\right)\overline{\left|A\right|+A}=\left(\left|A\right|+A\right)\left(\left|A\right|+\bar{A}\right)$$
74	9 47 9 39	muladdd	$$⊢A\in ℂ\to \left(\left|A\right|+A\right)\left(\left|A\right|+\bar{A}\right)=\left|A\right|\left|A\right|+\bar{A}A+\left|A\right|\bar{A}+\left|A\right|A$$
75	73 74	eqtrd	$$⊢A\in ℂ\to \left(\left|A\right|+A\right)\overline{\left|A\right|+A}=\left|A\right|\left|A\right|+\bar{A}A+\left|A\right|\bar{A}+\left|A\right|A$$
76		absvalsq	$$⊢\left|A\right|+A\in ℂ\to {\left|\left|A\right|+A\right|}^2=\left(\left|A\right|+A\right)\overline{\left|A\right|+A}$$
77	11 76	syl	$$⊢A\in ℂ\to {\left|\left|A\right|+A\right|}^2=\left(\left|A\right|+A\right)\overline{\left|A\right|+A}$$
78		mulcl	$$⊢\left(\bar{A}\in ℂ\wedge A\in ℂ\right)\to \bar{A}A\in ℂ$$
79	39 78	mpancom	$$⊢A\in ℂ\to \bar{A}A\in ℂ$$
80	54 79	addcld	$$⊢A\in ℂ\to \left|A\right|\left|A\right|+\bar{A}A\in ℂ$$
81		mulcl	$$⊢\left(\left|A\right|\in ℂ\wedge A\in ℂ\right)\to \left|A\right|A\in ℂ$$
82	9 81	mpancom	$$⊢A\in ℂ\to \left|A\right|A\in ℂ$$
83	80 52 82	addassd	$$⊢A\in ℂ\to \left(\left|A\right|\left|A\right|+\bar{A}A\right)+\left|A\right|\bar{A}+\left|A\right|A=\left|A\right|\left|A\right|+\bar{A}A+\left|A\right|\bar{A}+\left|A\right|A$$
84	75 77 83	3eqtr4d	$$⊢A\in ℂ\to {\left|\left|A\right|+A\right|}^2=\left(\left|A\right|\left|A\right|+\bar{A}A\right)+\left|A\right|\bar{A}+\left|A\right|A$$
85	9 48 47	adddid	$$⊢A\in ℂ\to \left|A\right|\left(\bar{A}+2\left|A\right|+A\right)=\left|A\right|\left(\bar{A}+2\left|A\right|\right)+\left|A\right|A$$
86	67 84 85	3eqtr4d	$$⊢A\in ℂ\to {\left|\left|A\right|+A\right|}^2=\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)$$
87	50 86	oveq12d	$$⊢A\in ℂ\to \frac{{\left(\left|A\right|+A\right)}^2}{{\left|\left|A\right|+A\right|}^2}=\frac{A\left(\bar{A}+2\left|A\right|+A\right)}{\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}$$
88	87	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \frac{{\left(\left|A\right|+A\right)}^2}{{\left|\left|A\right|+A\right|}^2}=\frac{A\left(\bar{A}+2\left|A\right|+A\right)}{\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}$$
89	27 88	eqtrd	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to {\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}^2=\frac{A\left(\bar{A}+2\left|A\right|+A\right)}{\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}$$
90	26 89	oveq12d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to {\sqrt{\left|A\right|}}^2{\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}^2=\left|A\right|\left(\frac{A\left(\bar{A}+2\left|A\right|+A\right)}{\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}\right)$$
91		addcl	$$⊢\left(\bar{A}+2\left|A\right|\in ℂ\wedge A\in ℂ\right)\to \bar{A}+2\left|A\right|+A\in ℂ$$
92	48 91	mpancom	$$⊢A\in ℂ\to \bar{A}+2\left|A\right|+A\in ℂ$$
93	9 47 92	mul12d	$$⊢A\in ℂ\to \left|A\right|A\left(\bar{A}+2\left|A\right|+A\right)=A\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)$$
94	93	oveq1d	$$⊢A\in ℂ\to \frac{\left|A\right|A\left(\bar{A}+2\left|A\right|+A\right)}{\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}=\frac{A\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}{\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}$$
95	94	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \frac{\left|A\right|A\left(\bar{A}+2\left|A\right|+A\right)}{\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}=\frac{A\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}{\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}$$
96	9	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|A\right|\in ℂ$$
97		mulcl	$$⊢\left(A\in ℂ\wedge \bar{A}+2\left|A\right|+A\in ℂ\right)\to A\left(\bar{A}+2\left|A\right|+A\right)\in ℂ$$
98	92 97	mpdan	$$⊢A\in ℂ\to A\left(\bar{A}+2\left|A\right|+A\right)\in ℂ$$
99	98	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to A\left(\bar{A}+2\left|A\right|+A\right)\in ℂ$$
100	9 92	mulcld	$$⊢A\in ℂ\to \left|A\right|\left(\bar{A}+2\left|A\right|+A\right)\in ℂ$$
101	100	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|A\right|\left(\bar{A}+2\left|A\right|+A\right)\in ℂ$$
102		sqeq0	$$⊢\left|\left|A\right|+A\right|\in ℂ\to \left({\left|\left|A\right|+A\right|}^2=0\leftrightarrow \left|\left|A\right|+A\right|=0\right)$$
103	15 102	syl	$$⊢A\in ℂ\to \left({\left|\left|A\right|+A\right|}^2=0\leftrightarrow \left|\left|A\right|+A\right|=0\right)$$
104	86	eqeq1d	$$⊢A\in ℂ\to \left({\left|\left|A\right|+A\right|}^2=0\leftrightarrow \left|A\right|\left(\bar{A}+2\left|A\right|+A\right)=0\right)$$
105	103 104 17	3bitr3rd	$$⊢A\in ℂ\to \left(\left|A\right|+A=0\leftrightarrow \left|A\right|\left(\bar{A}+2\left|A\right|+A\right)=0\right)$$
106	105	necon3bid	$$⊢A\in ℂ\to \left(\left|A\right|+A\ne 0\leftrightarrow \left|A\right|\left(\bar{A}+2\left|A\right|+A\right)\ne 0\right)$$
107	106	biimpa	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|A\right|\left(\bar{A}+2\left|A\right|+A\right)\ne 0$$
108	96 99 101 107	divassd	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \frac{\left|A\right|A\left(\bar{A}+2\left|A\right|+A\right)}{\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}=\left|A\right|\left(\frac{A\left(\bar{A}+2\left|A\right|+A\right)}{\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}\right)$$
109		simpl	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to A\in ℂ$$
110	109 101 107	divcan4d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \frac{A\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}{\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}=A$$
111	95 108 110	3eqtr3d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|A\right|\left(\frac{A\left(\bar{A}+2\left|A\right|+A\right)}{\left|A\right|\left(\bar{A}+2\left|A\right|+A\right)}\right)=A$$
112	22 90 111	3eqtrd	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to B^2=A$$
113	6	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \sqrt{\left|A\right|}\in ℝ$$
114	11	addcjd	$$⊢A\in ℂ\to \left|A\right|+A+\overline{\left|A\right|+A}=2\Re \left(\left|A\right|+A\right)$$
115		2re	$$⊢2\in ℝ$$
116	11	recld	$$⊢A\in ℂ\to \Re \left(\left|A\right|+A\right)\in ℝ$$
117		remulcl	$$⊢\left(2\in ℝ\wedge \Re \left(\left|A\right|+A\right)\in ℝ\right)\to 2\Re \left(\left|A\right|+A\right)\in ℝ$$
118	115 116 117	sylancr	$$⊢A\in ℂ\to 2\Re \left(\left|A\right|+A\right)\in ℝ$$
119	114 118	eqeltrd	$$⊢A\in ℂ\to \left|A\right|+A+\overline{\left|A\right|+A}\in ℝ$$
120	119	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|A\right|+A+\overline{\left|A\right|+A}\in ℝ$$
121	14	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|\left|A\right|+A\right|\in ℝ$$
122	120 121 19	redivcld	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\in ℝ$$
123	113 122	remulcld	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)\in ℝ$$
124		sqrtge0	$$⊢\left(\left|A\right|\in ℝ\wedge 0\le \left|A\right|\right)\to 0\le \sqrt{\left|A\right|}$$
125	3 4 124	syl2anc	$$⊢A\in ℂ\to 0\le \sqrt{\left|A\right|}$$
126	125	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to 0\le \sqrt{\left|A\right|}$$
127		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
128		releabs	$$⊢-A\in ℂ\to \Re \left(-A\right)\le \left|-A\right|$$
129	127 128	syl	$$⊢A\in ℂ\to \Re \left(-A\right)\le \left|-A\right|$$
130		abscl	$$⊢-A\in ℂ\to \left|-A\right|\in ℝ$$
131	127 130	syl	$$⊢A\in ℂ\to \left|-A\right|\in ℝ$$
132	127	recld	$$⊢A\in ℂ\to \Re \left(-A\right)\in ℝ$$
133	131 132	subge0d	$$⊢A\in ℂ\to \left(0\le \left|-A\right|-\Re \left(-A\right)\leftrightarrow \Re \left(-A\right)\le \left|-A\right|\right)$$
134	129 133	mpbird	$$⊢A\in ℂ\to 0\le \left|-A\right|-\Re \left(-A\right)$$
135		readd	$$⊢\left(\left|A\right|\in ℂ\wedge A\in ℂ\right)\to \Re \left(\left|A\right|+A\right)=\Re \left(\left|A\right|\right)+\Re \left(A\right)$$
136	9 135	mpancom	$$⊢A\in ℂ\to \Re \left(\left|A\right|+A\right)=\Re \left(\left|A\right|\right)+\Re \left(A\right)$$
137	3	rered	$$⊢A\in ℂ\to \Re \left(\left|A\right|\right)=\left|A\right|$$
138		absneg	$$⊢A\in ℂ\to \left|-A\right|=\left|A\right|$$
139	137 138	eqtr4d	$$⊢A\in ℂ\to \Re \left(\left|A\right|\right)=\left|-A\right|$$
140		negneg	$$⊢A\in ℂ\to -\left(-A\right)=A$$
141	140	fveq2d	$$⊢A\in ℂ\to \Re \left(-\left(-A\right)\right)=\Re \left(A\right)$$
142	127	renegd	$$⊢A\in ℂ\to \Re \left(-\left(-A\right)\right)=-\Re \left(-A\right)$$
143	141 142	eqtr3d	$$⊢A\in ℂ\to \Re \left(A\right)=-\Re \left(-A\right)$$
144	139 143	oveq12d	$$⊢A\in ℂ\to \Re \left(\left|A\right|\right)+\Re \left(A\right)=\left|-A\right|+\left(-\Re \left(-A\right)\right)$$
145	131	recnd	$$⊢A\in ℂ\to \left|-A\right|\in ℂ$$
146	132	recnd	$$⊢A\in ℂ\to \Re \left(-A\right)\in ℂ$$
147	145 146	negsubd	$$⊢A\in ℂ\to \left|-A\right|+\left(-\Re \left(-A\right)\right)=\left|-A\right|-\Re \left(-A\right)$$
148	136 144 147	3eqtrd	$$⊢A\in ℂ\to \Re \left(\left|A\right|+A\right)=\left|-A\right|-\Re \left(-A\right)$$
149	134 148	breqtrrd	$$⊢A\in ℂ\to 0\le \Re \left(\left|A\right|+A\right)$$
150		0le2	$$⊢0\le 2$$
151		mulge0	$$⊢\left(\left(2\in ℝ\wedge 0\le 2\right)\wedge \left(\Re \left(\left|A\right|+A\right)\in ℝ\wedge 0\le \Re \left(\left|A\right|+A\right)\right)\right)\to 0\le 2\Re \left(\left|A\right|+A\right)$$
152	115 150 151	mpanl12	$$⊢\left(\Re \left(\left|A\right|+A\right)\in ℝ\wedge 0\le \Re \left(\left|A\right|+A\right)\right)\to 0\le 2\Re \left(\left|A\right|+A\right)$$
153	116 149 152	syl2anc	$$⊢A\in ℂ\to 0\le 2\Re \left(\left|A\right|+A\right)$$
154	153 114	breqtrrd	$$⊢A\in ℂ\to 0\le \left|A\right|+A+\overline{\left|A\right|+A}$$
155	154	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to 0\le \left|A\right|+A+\overline{\left|A\right|+A}$$
156		absge0	$$⊢\left|A\right|+A\in ℂ\to 0\le \left|\left|A\right|+A\right|$$
157	12 156	syl	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to 0\le \left|\left|A\right|+A\right|$$
158	121 157 19	ne0gt0d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to 0<\left|\left|A\right|+A\right|$$
159		divge0	$$⊢\left(\left(\left|A\right|+A+\overline{\left|A\right|+A}\in ℝ\wedge 0\le \left|A\right|+A+\overline{\left|A\right|+A}\right)\wedge \left(\left|\left|A\right|+A\right|\in ℝ\wedge 0<\left|\left|A\right|+A\right|\right)\right)\to 0\le \frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}$$
160	120 155 121 158 159	syl22anc	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to 0\le \frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}$$
161	113 122 126 160	mulge0d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to 0\le \sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)$$
162		2pos	$$⊢0<2$$
163		divge0	$$⊢\left(\left(\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)\in ℝ\wedge 0\le \sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)\right)\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to 0\le \frac{\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)}{2}$$
164	115 162 163	mpanr12	$$⊢\left(\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)\in ℝ\wedge 0\le \sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)\right)\to 0\le \frac{\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)}{2}$$
165	123 161 164	syl2anc	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to 0\le \frac{\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)}{2}$$
166	8 20	mulcld	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)\in ℂ$$
167	1 166	eqeltrid	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to B\in ℂ$$
168		reval	$$⊢B\in ℂ\to \Re \left(B\right)=\frac{B+\bar{B}}{2}$$
169	167 168	syl	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \Re \left(B\right)=\frac{B+\bar{B}}{2}$$
170	1	oveq1i	$$⊢B+\sqrt{\left|A\right|}\left(\frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)+\sqrt{\left|A\right|}\left(\frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)$$
171	1	fveq2i	$$⊢\bar{B}=\overline{\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}$$
172	8 20	cjmuld	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \overline{\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)}=\overline{\sqrt{\left|A\right|}}\overline{\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}}$$
173	171 172	eqtrid	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \bar{B}=\overline{\sqrt{\left|A\right|}}\overline{\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}}$$
174	6	cjred	$$⊢A\in ℂ\to \overline{\sqrt{\left|A\right|}}=\sqrt{\left|A\right|}$$
175	174	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \overline{\sqrt{\left|A\right|}}=\sqrt{\left|A\right|}$$
176	12 16 19	cjdivd	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \overline{\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}}=\frac{\overline{\left|A\right|+A}}{\overline{\left|\left|A\right|+A\right|}}$$
177	121	cjred	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \overline{\left|\left|A\right|+A\right|}=\left|\left|A\right|+A\right|$$
178	177	oveq2d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \frac{\overline{\left|A\right|+A}}{\overline{\left|\left|A\right|+A\right|}}=\frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}$$
179	176 178	eqtrd	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \overline{\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}}=\frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}$$
180	175 179	oveq12d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \overline{\sqrt{\left|A\right|}}\overline{\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}}=\sqrt{\left|A\right|}\left(\frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)$$
181	173 180	eqtrd	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \bar{B}=\sqrt{\left|A\right|}\left(\frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)$$
182	181	oveq2d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to B+\bar{B}=B+\sqrt{\left|A\right|}\left(\frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)$$
183	12	cjcld	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \overline{\left|A\right|+A}\in ℂ$$
184	183 16 19	divcld	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\in ℂ$$
185	8 20 184	adddid	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \sqrt{\left|A\right|}\left(\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)+\left(\frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)\right)=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)+\sqrt{\left|A\right|}\left(\frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)$$
186	170 182 185	3eqtr4a	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to B+\bar{B}=\sqrt{\left|A\right|}\left(\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)+\left(\frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)\right)$$
187	12 183 16 19	divdird	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}=\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)+\left(\frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)$$
188	187	oveq2d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)=\sqrt{\left|A\right|}\left(\left(\frac{\left|A\right|+A}{\left|\left|A\right|+A\right|}\right)+\left(\frac{\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)\right)$$
189	186 188	eqtr4d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to B+\bar{B}=\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)$$
190	189	oveq1d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \frac{B+\bar{B}}{2}=\frac{\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)}{2}$$
191	169 190	eqtrd	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \Re \left(B\right)=\frac{\sqrt{\left|A\right|}\left(\frac{\left|A\right|+A+\overline{\left|A\right|+A}}{\left|\left|A\right|+A\right|}\right)}{2}$$
192	165 191	breqtrrd	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to 0\le \Re \left(B\right)$$
193		subneg	$$⊢\left(\left|A\right|\in ℂ\wedge A\in ℂ\right)\to \left|A\right|-\left(-A\right)=\left|A\right|+A$$
194	9 193	mpancom	$$⊢A\in ℂ\to \left|A\right|-\left(-A\right)=\left|A\right|+A$$
195	194	eqeq1d	$$⊢A\in ℂ\to \left(\left|A\right|-\left(-A\right)=0\leftrightarrow \left|A\right|+A=0\right)$$
196	9 127	subeq0ad	$$⊢A\in ℂ\to \left(\left|A\right|-\left(-A\right)=0\leftrightarrow \left|A\right|=-A\right)$$
197	195 196	bitr3d	$$⊢A\in ℂ\to \left(\left|A\right|+A=0\leftrightarrow \left|A\right|=-A\right)$$
198	197	necon3bid	$$⊢A\in ℂ\to \left(\left|A\right|+A\ne 0\leftrightarrow \left|A\right|\ne -A\right)$$
199	198	biimpa	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left|A\right|\ne -A$$
200		resqcl	$$⊢\mathrm{i}B\in ℝ\to {\mathrm{i}B}^2\in ℝ$$
201		ax-icn	$$⊢\mathrm{i}\in ℂ$$
202		sqmul	$$⊢\left(\mathrm{i}\in ℂ\wedge B\in ℂ\right)\to {\mathrm{i}B}^2={\mathrm{i}}^2{B}^2$$
203	201 167 202	sylancr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to {\mathrm{i}B}^2={\mathrm{i}}^2{B}^2$$
204		i2	$$⊢{\mathrm{i}}^2=-1$$
205	204	a1i	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to {\mathrm{i}}^2=-1$$
206	205 112	oveq12d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to {\mathrm{i}}^2{B}^2=-1A$$
207		mulm1	$$⊢A\in ℂ\to -1A=-A$$
208	207	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to -1A=-A$$
209	203 206 208	3eqtrd	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to {\mathrm{i}B}^2=-A$$
210	209	eleq1d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left({\mathrm{i}B}^2\in ℝ\leftrightarrow -A\in ℝ\right)$$
211	200 210	imbitrid	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left(\mathrm{i}B\in ℝ\to -A\in ℝ\right)$$
212		renegcl	$$⊢-A\in ℝ\to -\left(-A\right)\in ℝ$$
213	140	eleq1d	$$⊢A\in ℂ\to \left(-\left(-A\right)\in ℝ\leftrightarrow A\in ℝ\right)$$
214	212 213	imbitrid	$$⊢A\in ℂ\to \left(-A\in ℝ\to A\in ℝ\right)$$
215	109 211 214	sylsyld	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left(\mathrm{i}B\in ℝ\to A\in ℝ\right)$$
216		sqge0	$$⊢\mathrm{i}B\in ℝ\to 0\le {\mathrm{i}B}^2$$
217	209	breq2d	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left(0\le {\mathrm{i}B}^2\leftrightarrow 0\le -A\right)$$
218	216 217	imbitrid	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left(\mathrm{i}B\in ℝ\to 0\le -A\right)$$
219		le0neg1	$$⊢A\in ℝ\to \left(A\le 0\leftrightarrow 0\le -A\right)$$
220	219	biimprcd	$$⊢0\le -A\to \left(A\in ℝ\to A\le 0\right)$$
221	218 215 220	syl6c	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left(\mathrm{i}B\in ℝ\to A\le 0\right)$$
222	215 221	jcad	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left(\mathrm{i}B\in ℝ\to \left(A\in ℝ\wedge A\le 0\right)\right)$$
223		absnid	$$⊢\left(A\in ℝ\wedge A\le 0\right)\to \left|A\right|=-A$$
224	222 223	syl6	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left(\mathrm{i}B\in ℝ\to \left|A\right|=-A\right)$$
225	224	necon3ad	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left(\left|A\right|\ne -A\to \neg \mathrm{i}B\in ℝ\right)$$
226	199 225	mpd	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \neg \mathrm{i}B\in ℝ$$
227		rpre	$$⊢\mathrm{i}B\in {ℝ}^{+}\to \mathrm{i}B\in ℝ$$
228	226 227	nsyl	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \neg \mathrm{i}B\in {ℝ}^{+}$$
229		df-nel	$$⊢\mathrm{i}B\notin {ℝ}^{+}\leftrightarrow \neg \mathrm{i}B\in {ℝ}^{+}$$
230	228 229	sylibr	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \mathrm{i}B\notin {ℝ}^{+}$$
231	112 192 230	3jca	$$⊢\left(A\in ℂ\wedge \left|A\right|+A\ne 0\right)\to \left(B^2=A\wedge 0\le \Re \left(B\right)\wedge \mathrm{i}B\notin {ℝ}^{+}\right)$$