This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 · 𝐵 ) ∉ ℝ+ ) )