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

Metamath Proof Explorer

Theorem sqreu

Description: Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion sqreu ( 𝐴 ∈ ℂ → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )

Proof

Step Hyp Ref Expression
1 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
2 1 recnd ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℂ )
3 subneg ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) − - 𝐴 ) = ( ( abs ‘ 𝐴 ) + 𝐴 ) )
4 2 3 mpancom ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) − - 𝐴 ) = ( ( abs ‘ 𝐴 ) + 𝐴 ) )
5 4 eqeq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( abs ‘ 𝐴 ) − - 𝐴 ) = 0 ↔ ( ( abs ‘ 𝐴 ) + 𝐴 ) = 0 ) )
6 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
7 2 6 subeq0ad ⊢ ( 𝐴 ∈ ℂ → ( ( ( abs ‘ 𝐴 ) − - 𝐴 ) = 0 ↔ ( abs ‘ 𝐴 ) = - 𝐴 ) )
8 5 7 bitr3d ⊢ ( 𝐴 ∈ ℂ → ( ( ( abs ‘ 𝐴 ) + 𝐴 ) = 0 ↔ ( abs ‘ 𝐴 ) = - 𝐴 ) )
9 ax-icn ⊢ i ∈ ℂ
10 absge0 ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( abs ‘ 𝐴 ) )
11 1 10 jca ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) )
12 eleq1 ⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( ( abs ‘ 𝐴 ) ∈ ℝ ↔ - 𝐴 ∈ ℝ ) )
13 breq2 ⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( 0 ≤ ( abs ‘ 𝐴 ) ↔ 0 ≤ - 𝐴 ) )
14 12 13 anbi12d ⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) ↔ ( - 𝐴 ∈ ℝ ∧ 0 ≤ - 𝐴 ) ) )
15 11 14 imbitrid ⊢ ( ( abs ‘ 𝐴 ) = - 𝐴 → ( 𝐴 ∈ ℂ → ( - 𝐴 ∈ ℝ ∧ 0 ≤ - 𝐴 ) ) )
16 15 impcom ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( - 𝐴 ∈ ℝ ∧ 0 ≤ - 𝐴 ) )
17 resqrtcl ⊢ ( ( - 𝐴 ∈ ℝ ∧ 0 ≤ - 𝐴 ) → ( √ ‘ - 𝐴 ) ∈ ℝ )
18 16 17 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( √ ‘ - 𝐴 ) ∈ ℝ )
19 18 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( √ ‘ - 𝐴 ) ∈ ℂ )
20 mulcl ⊢ ( ( i ∈ ℂ ∧ ( √ ‘ - 𝐴 ) ∈ ℂ ) → ( i · ( √ ‘ - 𝐴 ) ) ∈ ℂ )
21 9 19 20 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( i · ( √ ‘ - 𝐴 ) ) ∈ ℂ )
22 sqrtneglem ⊢ ( ( - 𝐴 ∈ ℝ ∧ 0 ≤ - 𝐴 ) → ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = - - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) )
23 16 22 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = - - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) )
24 negneg ⊢ ( 𝐴 ∈ ℂ → - - 𝐴 = 𝐴 )
25 24 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → - - 𝐴 = 𝐴 )
26 25 eqeq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = - - 𝐴 ↔ ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = 𝐴 ) )
27 26 3anbi1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = - - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) ↔ ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) ) )
28 23 27 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) )
29 oveq1 ⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( 𝑥 ↑ 2 ) = ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) )
30 29 eqeq1d ⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( ( 𝑥 ↑ 2 ) = 𝐴 ↔ ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = 𝐴 ) )
31 fveq2 ⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) )
32 31 breq2d ⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ) )
33 oveq2 ⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( i · 𝑥 ) = ( i · ( i · ( √ ‘ - 𝐴 ) ) ) )
34 neleq1 ⊢ ( ( i · 𝑥 ) = ( i · ( i · ( √ ‘ - 𝐴 ) ) ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) )
35 33 34 syl ⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) )
36 30 32 35 3anbi123d ⊢ ( 𝑥 = ( i · ( √ ‘ - 𝐴 ) ) → ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) ) )
37 36 rspcev ⊢ ( ( ( i · ( √ ‘ - 𝐴 ) ) ∈ ℂ ∧ ( ( ( i · ( √ ‘ - 𝐴 ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ - 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ - 𝐴 ) ) ) ∉ ℝ+ ) ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
38 21 28 37 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = - 𝐴 ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
39 38 ex ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) = - 𝐴 → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
40 8 39 sylbid ⊢ ( 𝐴 ∈ ℂ → ( ( ( abs ‘ 𝐴 ) + 𝐴 ) = 0 → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
41 resqrtcl ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐴 ) ) → ( √ ‘ ( abs ‘ 𝐴 ) ) ∈ ℝ )
42 1 10 41 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( abs ‘ 𝐴 ) ) ∈ ℝ )
43 42 recnd ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( abs ‘ 𝐴 ) ) ∈ ℂ )
44 43 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( √ ‘ ( abs ‘ 𝐴 ) ) ∈ ℂ )
45 addcl ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ ℂ )
46 2 45 mpancom ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ ℂ )
47 46 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ ℂ )
48 abscl ⊢ ( ( ( abs ‘ 𝐴 ) + 𝐴 ) ∈ ℂ → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ∈ ℝ )
49 46 48 syl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ∈ ℝ )
50 49 recnd ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ∈ ℂ )
51 50 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ∈ ℂ )
52 46 abs00ad ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) = 0 ↔ ( ( abs ‘ 𝐴 ) + 𝐴 ) = 0 ) )
53 52 necon3bid ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ≠ 0 ↔ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) )
54 53 biimpar ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ≠ 0 )
55 47 51 54 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ∈ ℂ )
56 44 55 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ∈ ℂ )
57 eqid ⊢ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) )
58 57 sqreulem ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ( ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∧ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ) )
59 oveq1 ⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( 𝑥 ↑ 2 ) = ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) )
60 59 eqeq1d ⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( ( 𝑥 ↑ 2 ) = 𝐴 ↔ ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) = 𝐴 ) )
61 fveq2 ⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) )
62 61 breq2d ⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ) )
63 oveq2 ⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( i · 𝑥 ) = ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) )
64 neleq1 ⊢ ( ( i · 𝑥 ) = ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ) )
65 63 64 syl ⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ) )
66 60 62 65 3anbi123d ⊢ ( 𝑥 = ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) → ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∧ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ) ) )
67 66 rspcev ⊢ ( ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ∈ ℂ ∧ ( ( ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∧ ( i · ( ( √ ‘ ( abs ‘ 𝐴 ) ) · ( ( ( abs ‘ 𝐴 ) + 𝐴 ) / ( abs ‘ ( ( abs ‘ 𝐴 ) + 𝐴 ) ) ) ) ) ∉ ℝ+ ) ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
68 56 58 67 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
69 68 ex ⊢ ( 𝐴 ∈ ℂ → ( ( ( abs ‘ 𝐴 ) + 𝐴 ) ≠ 0 → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
70 40 69 pm2.61dne ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
71 sqrmo ⊢ ( 𝐴 ∈ ℂ → ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
72 reu5 ⊢ ( ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ∧ ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
73 70 71 72 sylanbrc ⊢ ( 𝐴 ∈ ℂ → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )