# 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 ${⊢}{B}=\sqrt{\left|{A}\right|}\left(\frac{\left|{A}\right|+{A}}{\left|\left|{A}\right|+{A}\right|}\right)$
Assertion sqreulem ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|+{A}\ne 0\right)\to \left({{B}}^{2}={A}\wedge 0\le \Re \left({B}\right)\wedge \mathrm{i}{B}\notin {ℝ}^{+}\right)$

### Proof

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