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	imbitrid	\|- ( ( 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	imbitrid	\|- ( 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	imbitrid	\|- ( ( 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+ ) )

Metamath Proof Explorer

Theorem sqreulem

Proof