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 )