| 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
|
syl5ib |
⊢ ( ( 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 · 𝑥 ) ∉ ℝ+ ) ) |