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	⊢ 𝐵 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) )
Assertion	sqreulem	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( ( 𝐵 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ∧ ( i · 𝐵 ) ∉ ℝ+ ) )

Proof

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