Metamath Proof Explorer

Theorem asinsinlem

Description: Lemma for asinsin . (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion asinsinlem 
|- ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( Re ` ( exp ` ( _i x. A ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 simpl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> A e. CC )
3 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
4 1 2 3 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. A ) e. CC )
5 4 recld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( _i x. A ) ) e. RR )
6 5 reefcld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( Re ` ( _i x. A ) ) ) e. RR )
7 simpr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
8 neghalfpirx 
 |-  -u ( _pi / 2 ) e. RR*
9 halfpire 
 |-  ( _pi / 2 ) e. RR
10 9 rexri 
 |-  ( _pi / 2 ) e. RR*
11 elioo2 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( ( Re ` A ) e. RR /\ -u ( _pi / 2 ) < ( Re ` A ) /\ ( Re ` A ) < ( _pi / 2 ) ) ) )
12 8 10 11 mp2an 
 |-  ( ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> ( ( Re ` A ) e. RR /\ -u ( _pi / 2 ) < ( Re ` A ) /\ ( Re ` A ) < ( _pi / 2 ) ) )
13 7 12 sylib 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( Re ` A ) e. RR /\ -u ( _pi / 2 ) < ( Re ` A ) /\ ( Re ` A ) < ( _pi / 2 ) ) )
14 13 simp1d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` A ) e. RR )
15 14 recoscld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` ( Re ` A ) ) e. RR )
16 efgt0 
 |-  ( ( Re ` ( _i x. A ) ) e. RR -> 0 < ( exp ` ( Re ` ( _i x. A ) ) ) )
17 5 16 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( exp ` ( Re ` ( _i x. A ) ) ) )
18 cosq14gt0 
 |-  ( ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> 0 < ( cos ` ( Re ` A ) ) )
19 18 adantl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( cos ` ( Re ` A ) ) )
20 6 15 17 19 mulgt0d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( ( exp ` ( Re ` ( _i x. A ) ) ) x. ( cos ` ( Re ` A ) ) ) )
21 efeul 
 |-  ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) = ( ( exp ` ( Re ` ( _i x. A ) ) ) x. ( ( cos ` ( Im ` ( _i x. A ) ) ) + ( _i x. ( sin ` ( Im ` ( _i x. A ) ) ) ) ) ) )
22 4 21 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( _i x. A ) ) = ( ( exp ` ( Re ` ( _i x. A ) ) ) x. ( ( cos ` ( Im ` ( _i x. A ) ) ) + ( _i x. ( sin ` ( Im ` ( _i x. A ) ) ) ) ) ) )
23 22 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( exp ` ( _i x. A ) ) ) = ( Re ` ( ( exp ` ( Re ` ( _i x. A ) ) ) x. ( ( cos ` ( Im ` ( _i x. A ) ) ) + ( _i x. ( sin ` ( Im ` ( _i x. A ) ) ) ) ) ) ) )
24 4 imcld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Im ` ( _i x. A ) ) e. RR )
25 24 recoscld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` ( Im ` ( _i x. A ) ) ) e. RR )
26 25 recnd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` ( Im ` ( _i x. A ) ) ) e. CC )
27 24 resincld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( sin ` ( Im ` ( _i x. A ) ) ) e. RR )
28 27 recnd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( sin ` ( Im ` ( _i x. A ) ) ) e. CC )
29 mulcl 
 |-  ( ( _i e. CC /\ ( sin ` ( Im ` ( _i x. A ) ) ) e. CC ) -> ( _i x. ( sin ` ( Im ` ( _i x. A ) ) ) ) e. CC )
30 1 28 29 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. ( sin ` ( Im ` ( _i x. A ) ) ) ) e. CC )
31 26 30 addcld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( cos ` ( Im ` ( _i x. A ) ) ) + ( _i x. ( sin ` ( Im ` ( _i x. A ) ) ) ) ) e. CC )
32 6 31 remul2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( ( exp ` ( Re ` ( _i x. A ) ) ) x. ( ( cos ` ( Im ` ( _i x. A ) ) ) + ( _i x. ( sin ` ( Im ` ( _i x. A ) ) ) ) ) ) ) = ( ( exp ` ( Re ` ( _i x. A ) ) ) x. ( Re ` ( ( cos ` ( Im ` ( _i x. A ) ) ) + ( _i x. ( sin ` ( Im ` ( _i x. A ) ) ) ) ) ) ) )
33 25 27 crred 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( ( cos ` ( Im ` ( _i x. A ) ) ) + ( _i x. ( sin ` ( Im ` ( _i x. A ) ) ) ) ) ) = ( cos ` ( Im ` ( _i x. A ) ) ) )
34 imre 
 |-  ( ( _i x. A ) e. CC -> ( Im ` ( _i x. A ) ) = ( Re ` ( -u _i x. ( _i x. A ) ) ) )
35 4 34 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Im ` ( _i x. A ) ) = ( Re ` ( -u _i x. ( _i x. A ) ) ) )
36 1 1 mulneg1i 
 |-  ( -u _i x. _i ) = -u ( _i x. _i )
37 ixi 
 |-  ( _i x. _i ) = -u 1
38 37 negeqi 
 |-  -u ( _i x. _i ) = -u -u 1
39 negneg1e1 
 |-  -u -u 1 = 1
40 36 38 39 3eqtri 
 |-  ( -u _i x. _i ) = 1
41 40 oveq1i 
 |-  ( ( -u _i x. _i ) x. A ) = ( 1 x. A )
42 negicn 
 |-  -u _i e. CC
43 42 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u _i e. CC )
44 1 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> _i e. CC )
45 43 44 2 mulassd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( -u _i x. _i ) x. A ) = ( -u _i x. ( _i x. A ) ) )
46 mulid2 
 |-  ( A e. CC -> ( 1 x. A ) = A )
47 46 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 1 x. A ) = A )
48 41 45 47 3eqtr3a 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( -u _i x. ( _i x. A ) ) = A )
49 48 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( -u _i x. ( _i x. A ) ) ) = ( Re ` A ) )
50 35 49 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Im ` ( _i x. A ) ) = ( Re ` A ) )
51 50 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` ( Im ` ( _i x. A ) ) ) = ( cos ` ( Re ` A ) ) )
52 33 51 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( ( cos ` ( Im ` ( _i x. A ) ) ) + ( _i x. ( sin ` ( Im ` ( _i x. A ) ) ) ) ) ) = ( cos ` ( Re ` A ) ) )
53 52 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` ( Re ` ( _i x. A ) ) ) x. ( Re ` ( ( cos ` ( Im ` ( _i x. A ) ) ) + ( _i x. ( sin ` ( Im ` ( _i x. A ) ) ) ) ) ) ) = ( ( exp ` ( Re ` ( _i x. A ) ) ) x. ( cos ` ( Re ` A ) ) ) )
54 23 32 53 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( exp ` ( _i x. A ) ) ) = ( ( exp ` ( Re ` ( _i x. A ) ) ) x. ( cos ` ( Re ` A ) ) ) )
55 20 54 breqtrrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( Re ` ( exp ` ( _i x. A ) ) ) )