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