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 ` ( abs ` A ) ) x. ( ( ( abs ` A ) + A ) / ( abs ` ( ( abs ` A ) + A ) ) ) )
Assertion	sqreulem	|- ( ( A e. CC /\ ( ( abs ` A ) + A ) =/= 0 ) -> ( ( B ^ 2 ) = A /\ 0 <_ ( Re ` B ) /\ ( _i x. B ) e/ RR+ ) )

Proof

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