Metamath Proof Explorer

Theorem cxpsqrtlem

Description: Lemma for cxpsqrt . (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpsqrtlem 
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqrt ` A ) ) -> ( _i x. ( sqrt ` A ) ) e. RR )

Proof

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 )