| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ax-icn |
⊢ i ∈ ℂ |
| 2 |
|
sqrtcl |
⊢ ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) ∈ ℂ ) |
| 3 |
2
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( √ ‘ 𝐴 ) ∈ ℂ ) |
| 4 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( √ ‘ 𝐴 ) ) ∈ ℂ ) |
| 5 |
1 3 4
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( i · ( √ ‘ 𝐴 ) ) ∈ ℂ ) |
| 6 |
|
imval |
⊢ ( ( i · ( √ ‘ 𝐴 ) ) ∈ ℂ → ( ℑ ‘ ( i · ( √ ‘ 𝐴 ) ) ) = ( ℜ ‘ ( ( i · ( √ ‘ 𝐴 ) ) / i ) ) ) |
| 7 |
5 6
|
syl |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℑ ‘ ( i · ( √ ‘ 𝐴 ) ) ) = ( ℜ ‘ ( ( i · ( √ ‘ 𝐴 ) ) / i ) ) ) |
| 8 |
|
ine0 |
⊢ i ≠ 0 |
| 9 |
|
divcan3 |
⊢ ( ( ( √ ‘ 𝐴 ) ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( i · ( √ ‘ 𝐴 ) ) / i ) = ( √ ‘ 𝐴 ) ) |
| 10 |
1 8 9
|
mp3an23 |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℂ → ( ( i · ( √ ‘ 𝐴 ) ) / i ) = ( √ ‘ 𝐴 ) ) |
| 11 |
3 10
|
syl |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ( i · ( √ ‘ 𝐴 ) ) / i ) = ( √ ‘ 𝐴 ) ) |
| 12 |
11
|
fveq2d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ ( ( i · ( √ ‘ 𝐴 ) ) / i ) ) = ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) |
| 13 |
|
halfre |
⊢ ( 1 / 2 ) ∈ ℝ |
| 14 |
13
|
recni |
⊢ ( 1 / 2 ) ∈ ℂ |
| 15 |
|
logcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ ) |
| 16 |
|
mulcl |
⊢ ( ( ( 1 / 2 ) ∈ ℂ ∧ ( log ‘ 𝐴 ) ∈ ℂ ) → ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ∈ ℂ ) |
| 17 |
14 15 16
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ∈ ℂ ) |
| 18 |
17
|
recld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ∈ ℝ ) |
| 19 |
18
|
reefcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℝ ) |
| 20 |
17
|
imcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ∈ ℝ ) |
| 21 |
20
|
recoscld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℝ ) |
| 22 |
18
|
rpefcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℝ+ ) |
| 23 |
22
|
rpge0d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 0 ≤ ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) |
| 24 |
|
immul2 |
⊢ ( ( ( 1 / 2 ) ∈ ℝ ∧ ( log ‘ 𝐴 ) ∈ ℂ ) → ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) = ( ( 1 / 2 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 25 |
13 15 24
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) = ( ( 1 / 2 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 26 |
15
|
imcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ) |
| 27 |
26
|
recnd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ) |
| 28 |
|
mulcom |
⊢ ( ( ( 1 / 2 ) ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ) → ( ( 1 / 2 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) · ( 1 / 2 ) ) ) |
| 29 |
14 27 28
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 1 / 2 ) · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) · ( 1 / 2 ) ) ) |
| 30 |
25 29
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) = ( ( ℑ ‘ ( log ‘ 𝐴 ) ) · ( 1 / 2 ) ) ) |
| 31 |
|
logimcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) |
| 32 |
31
|
simpld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ) |
| 33 |
|
pire |
⊢ π ∈ ℝ |
| 34 |
33
|
renegcli |
⊢ - π ∈ ℝ |
| 35 |
|
ltle |
⊢ ( ( - π ∈ ℝ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 36 |
34 26 35
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) |
| 37 |
32 36
|
mpd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) |
| 38 |
31
|
simprd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) |
| 39 |
34 33
|
elicc2i |
⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - π [,] π ) ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) |
| 40 |
26 37 38 39
|
syl3anbrc |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - π [,] π ) ) |
| 41 |
|
halfgt0 |
⊢ 0 < ( 1 / 2 ) |
| 42 |
13 41
|
elrpii |
⊢ ( 1 / 2 ) ∈ ℝ+ |
| 43 |
33
|
recni |
⊢ π ∈ ℂ |
| 44 |
|
2cn |
⊢ 2 ∈ ℂ |
| 45 |
|
2ne0 |
⊢ 2 ≠ 0 |
| 46 |
|
divneg |
⊢ ( ( π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( π / 2 ) = ( - π / 2 ) ) |
| 47 |
43 44 45 46
|
mp3an |
⊢ - ( π / 2 ) = ( - π / 2 ) |
| 48 |
34
|
recni |
⊢ - π ∈ ℂ |
| 49 |
48 44 45
|
divreci |
⊢ ( - π / 2 ) = ( - π · ( 1 / 2 ) ) |
| 50 |
47 49
|
eqtr2i |
⊢ ( - π · ( 1 / 2 ) ) = - ( π / 2 ) |
| 51 |
43 44 45
|
divreci |
⊢ ( π / 2 ) = ( π · ( 1 / 2 ) ) |
| 52 |
51
|
eqcomi |
⊢ ( π · ( 1 / 2 ) ) = ( π / 2 ) |
| 53 |
34 33 42 50 52
|
iccdili |
⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - π [,] π ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) · ( 1 / 2 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) |
| 54 |
40 53
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ℑ ‘ ( log ‘ 𝐴 ) ) · ( 1 / 2 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) |
| 55 |
30 54
|
eqeltrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) |
| 56 |
|
cosq14ge0 |
⊢ ( ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 0 ≤ ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) |
| 57 |
55 56
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 0 ≤ ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) |
| 58 |
19 21 23 57
|
mulge0d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 0 ≤ ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) |
| 59 |
|
cxpef |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( 1 / 2 ) ∈ ℂ ) → ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = ( exp ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) |
| 60 |
14 59
|
mp3an3 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = ( exp ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) |
| 61 |
|
efeul |
⊢ ( ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ∈ ℂ → ( exp ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) = ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) ) |
| 62 |
17 61
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) = ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) ) |
| 63 |
60 62
|
eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) ) |
| 64 |
63
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) ) = ( ℜ ‘ ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) ) ) |
| 65 |
21
|
recnd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℂ ) |
| 66 |
20
|
resincld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℝ ) |
| 67 |
66
|
recnd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℂ ) |
| 68 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ∈ ℂ ) → ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ∈ ℂ ) |
| 69 |
1 67 68
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ∈ ℂ ) |
| 70 |
65 69
|
addcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ∈ ℂ ) |
| 71 |
19 70
|
remul2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) ) = ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( ℜ ‘ ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) ) ) |
| 72 |
21 66
|
crred |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) = ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) |
| 73 |
72
|
oveq2d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( ℜ ‘ ( ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) ) ) = ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) |
| 74 |
64 71 73
|
3eqtrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) ) = ( ( exp ‘ ( ℜ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) · ( cos ‘ ( ℑ ‘ ( ( 1 / 2 ) · ( log ‘ 𝐴 ) ) ) ) ) ) |
| 75 |
58 74
|
breqtrrd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 0 ≤ ( ℜ ‘ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) ) ) |
| 76 |
75
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) ) ) |
| 77 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) |
| 78 |
77
|
fveq2d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) ) = ( ℜ ‘ - ( √ ‘ 𝐴 ) ) ) |
| 79 |
3
|
renegd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ - ( √ ‘ 𝐴 ) ) = - ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) |
| 80 |
78 79
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) ) = - ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) |
| 81 |
76 80
|
breqtrd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → 0 ≤ - ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) |
| 82 |
3
|
recld |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ ( √ ‘ 𝐴 ) ) ∈ ℝ ) |
| 83 |
82
|
le0neg1d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ( ℜ ‘ ( √ ‘ 𝐴 ) ) ≤ 0 ↔ 0 ≤ - ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) ) |
| 84 |
81 83
|
mpbird |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ ( √ ‘ 𝐴 ) ) ≤ 0 ) |
| 85 |
|
sqrtrege0 |
⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) |
| 86 |
85
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) |
| 87 |
|
0re |
⊢ 0 ∈ ℝ |
| 88 |
|
letri3 |
⊢ ( ( ( ℜ ‘ ( √ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ℜ ‘ ( √ ‘ 𝐴 ) ) = 0 ↔ ( ( ℜ ‘ ( √ ‘ 𝐴 ) ) ≤ 0 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) ) ) |
| 89 |
82 87 88
|
sylancl |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ( ℜ ‘ ( √ ‘ 𝐴 ) ) = 0 ↔ ( ( ℜ ‘ ( √ ‘ 𝐴 ) ) ≤ 0 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) ) ) |
| 90 |
84 86 89
|
mpbir2and |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℜ ‘ ( √ ‘ 𝐴 ) ) = 0 ) |
| 91 |
7 12 90
|
3eqtrd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( ℑ ‘ ( i · ( √ ‘ 𝐴 ) ) ) = 0 ) |
| 92 |
5 91
|
reim0bd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑𝑐 ( 1 / 2 ) ) = - ( √ ‘ 𝐴 ) ) → ( i · ( √ ‘ 𝐴 ) ) ∈ ℝ ) |