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