Metamath Proof Explorer

Theorem asinsinlem

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

Ref Expression
Assertion asinsinlem ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 𝐴 ∈ ℂ )
3 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
4 1 2 3 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · 𝐴 ) ∈ ℂ )
5 4 recld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( i · 𝐴 ) ) ∈ ℝ )
6 5 reefcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) ∈ ℝ )
7 neghalfpirx ⊢ - ( π / 2 ) ∈ ℝ*
8 halfpire ⊢ ( π / 2 ) ∈ ℝ
9 8 rexri ⊢ ( π / 2 ) ∈ ℝ*
10 elioo2 ⊢ ( ( - ( π / 2 ) ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ) → ( ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ - ( π / 2 ) < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) ) )
11 7 9 10 mp2an ⊢ ( ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ↔ ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ - ( π / 2 ) < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) )
12 11 bilani ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ - ( π / 2 ) < ( ℜ ‘ 𝐴 ) ∧ ( ℜ ‘ 𝐴 ) < ( π / 2 ) ) )
13 12 simp1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
14 13 recoscld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
15 efgt0 ⊢ ( ( ℜ ‘ ( i · 𝐴 ) ) ∈ ℝ → 0 < ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) )
16 5 15 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) )
17 cosq14gt0 ⊢ ( ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) → 0 < ( cos ‘ ( ℜ ‘ 𝐴 ) ) )
18 17 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( cos ‘ ( ℜ ‘ 𝐴 ) ) )
19 6 14 16 18 mulgt0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) · ( cos ‘ ( ℜ ‘ 𝐴 ) ) ) )
20 efeul ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) · ( ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ) ) ) )
21 4 20 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( exp ‘ ( i · 𝐴 ) ) = ( ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) · ( ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ) ) ) )
22 21 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( ℜ ‘ ( ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) · ( ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ) ) ) ) )
23 4 imcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℑ ‘ ( i · 𝐴 ) ) ∈ ℝ )
24 23 recoscld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ∈ ℝ )
25 24 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ∈ ℂ )
26 23 resincld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ∈ ℝ )
27 26 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ∈ ℂ )
28 mulcl ⊢ ( ( i ∈ ℂ ∧ ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ∈ ℂ ) → ( i · ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ) ∈ ℂ )
29 1 27 28 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( i · ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ) ∈ ℂ )
30 25 29 addcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ) ) ∈ ℂ )
31 6 30 remul2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) · ( ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ) ) ) ) = ( ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) · ( ℜ ‘ ( ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ) ) ) ) )
32 24 26 crred ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ) ) ) = ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) )
33 imre ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ ( - i · ( i · 𝐴 ) ) ) )
34 4 33 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ ( - i · ( i · 𝐴 ) ) ) )
35 1 1 mulneg1i ⊢ ( - i · i ) = - ( i · i )
36 ixi ⊢ ( i · i ) = - 1
37 36 negeqi ⊢ - ( i · i ) = - - 1
38 negneg1e1 ⊢ - - 1 = 1
39 35 37 38 3eqtri ⊢ ( - i · i ) = 1
40 39 oveq1i ⊢ ( ( - i · i ) · 𝐴 ) = ( 1 · 𝐴 )
41 negicn ⊢ - i ∈ ℂ
42 41 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → - i ∈ ℂ )
43 1 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → i ∈ ℂ )
44 42 43 2 mulassd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( - i · i ) · 𝐴 ) = ( - i · ( i · 𝐴 ) ) )
45 mullid ⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
46 45 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( 1 · 𝐴 ) = 𝐴 )
47 40 44 46 3eqtr3a ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( - i · ( i · 𝐴 ) ) = 𝐴 )
48 47 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( - i · ( i · 𝐴 ) ) ) = ( ℜ ‘ 𝐴 ) )
49 34 48 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ 𝐴 ) )
50 49 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) = ( cos ‘ ( ℜ ‘ 𝐴 ) ) )
51 32 50 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ) ) ) = ( cos ‘ ( ℜ ‘ 𝐴 ) ) )
52 51 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) · ( ℜ ‘ ( ( cos ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) + ( i · ( sin ‘ ( ℑ ‘ ( i · 𝐴 ) ) ) ) ) ) ) = ( ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) · ( cos ‘ ( ℜ ‘ 𝐴 ) ) ) )
53 22 31 52 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( ( exp ‘ ( ℜ ‘ ( i · 𝐴 ) ) ) · ( cos ‘ ( ℜ ‘ 𝐴 ) ) ) )
54 19 53 breqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → 0 < ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) )