Metamath Proof Explorer

Theorem asinsinlem

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

Ref Expression
Assertion asinsinlem ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → 0 < ℜ ⁡ e i ⁢ A

Proof

Step Hyp Ref Expression
1 ax-icn ⊢ i ∈ ℂ
2 simpl ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → A ∈ ℂ
3 mulcl ⊢ i ∈ ℂ ∧ A ∈ ℂ → i ⁢ A ∈ ℂ
4 1 2 3 sylancr ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → i ⁢ A ∈ ℂ
5 4 recld ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℜ ⁡ i ⁢ A ∈ ℝ
6 5 reefcld ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → e ℜ ⁡ i ⁢ A ∈ ℝ
7 simpr ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℜ ⁡ A ∈ − π 2 π 2
8 neghalfpirx ⊢ − π 2 ∈ ℝ *
9 halfpire ⊢ π 2 ∈ ℝ
10 9 rexri ⊢ π 2 ∈ ℝ *
11 elioo2 ⊢ − π 2 ∈ ℝ * ∧ π 2 ∈ ℝ * → ℜ ⁡ A ∈ − π 2 π 2 ↔ ℜ ⁡ A ∈ ℝ ∧ − π 2 < ℜ ⁡ A ∧ ℜ ⁡ A < π 2
12 8 10 11 mp2an ⊢ ℜ ⁡ A ∈ − π 2 π 2 ↔ ℜ ⁡ A ∈ ℝ ∧ − π 2 < ℜ ⁡ A ∧ ℜ ⁡ A < π 2
13 7 12 sylib ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℜ ⁡ A ∈ ℝ ∧ − π 2 < ℜ ⁡ A ∧ ℜ ⁡ A < π 2
14 13 simp1d ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℜ ⁡ A ∈ ℝ
15 14 recoscld ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → cos ⁡ ℜ ⁡ A ∈ ℝ
16 efgt0 ⊢ ℜ ⁡ i ⁢ A ∈ ℝ → 0 < e ℜ ⁡ i ⁢ A
17 5 16 syl ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → 0 < e ℜ ⁡ i ⁢ A
18 cosq14gt0 ⊢ ℜ ⁡ A ∈ − π 2 π 2 → 0 < cos ⁡ ℜ ⁡ A
19 18 adantl ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → 0 < cos ⁡ ℜ ⁡ A
20 6 15 17 19 mulgt0d ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → 0 < e ℜ ⁡ i ⁢ A ⁢ cos ⁡ ℜ ⁡ A
21 efeul ⊢ i ⁢ A ∈ ℂ → e i ⁢ A = e ℜ ⁡ i ⁢ A ⁢ cos ⁡ ℑ ⁡ i ⁢ A + i ⁢ sin ⁡ ℑ ⁡ i ⁢ A
22 4 21 syl ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → e i ⁢ A = e ℜ ⁡ i ⁢ A ⁢ cos ⁡ ℑ ⁡ i ⁢ A + i ⁢ sin ⁡ ℑ ⁡ i ⁢ A
23 22 fveq2d ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℜ ⁡ e i ⁢ A = ℜ ⁡ e ℜ ⁡ i ⁢ A ⁢ cos ⁡ ℑ ⁡ i ⁢ A + i ⁢ sin ⁡ ℑ ⁡ i ⁢ A
24 4 imcld ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℑ ⁡ i ⁢ A ∈ ℝ
25 24 recoscld ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → cos ⁡ ℑ ⁡ i ⁢ A ∈ ℝ
26 25 recnd ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → cos ⁡ ℑ ⁡ i ⁢ A ∈ ℂ
27 24 resincld ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → sin ⁡ ℑ ⁡ i ⁢ A ∈ ℝ
28 27 recnd ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → sin ⁡ ℑ ⁡ i ⁢ A ∈ ℂ
29 mulcl ⊢ i ∈ ℂ ∧ sin ⁡ ℑ ⁡ i ⁢ A ∈ ℂ → i ⁢ sin ⁡ ℑ ⁡ i ⁢ A ∈ ℂ
30 1 28 29 sylancr ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → i ⁢ sin ⁡ ℑ ⁡ i ⁢ A ∈ ℂ
31 26 30 addcld ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → cos ⁡ ℑ ⁡ i ⁢ A + i ⁢ sin ⁡ ℑ ⁡ i ⁢ A ∈ ℂ
32 6 31 remul2d ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℜ ⁡ e ℜ ⁡ i ⁢ A ⁢ cos ⁡ ℑ ⁡ i ⁢ A + i ⁢ sin ⁡ ℑ ⁡ i ⁢ A = e ℜ ⁡ i ⁢ A ⁢ ℜ ⁡ cos ⁡ ℑ ⁡ i ⁢ A + i ⁢ sin ⁡ ℑ ⁡ i ⁢ A
33 25 27 crred ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℜ ⁡ cos ⁡ ℑ ⁡ i ⁢ A + i ⁢ sin ⁡ ℑ ⁡ i ⁢ A = cos ⁡ ℑ ⁡ i ⁢ A
34 imre ⊢ i ⁢ A ∈ ℂ → ℑ ⁡ i ⁢ A = ℜ ⁡ − i ⁢ i ⁢ A
35 4 34 syl ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℑ ⁡ i ⁢ A = ℜ ⁡ − i ⁢ i ⁢ A
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 ⁢ A = 1 ⁢ A
42 negicn ⊢ − i ∈ ℂ
43 42 a1i ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → − i ∈ ℂ
44 1 a1i ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → i ∈ ℂ
45 43 44 2 mulassd ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → − i ⁢ i ⁢ A = − i ⁢ i ⁢ A
46 mullid ⊢ A ∈ ℂ → 1 ⁢ A = A
47 46 adantr ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → 1 ⁢ A = A
48 41 45 47 3eqtr3a ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → − i ⁢ i ⁢ A = A
49 48 fveq2d ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℜ ⁡ − i ⁢ i ⁢ A = ℜ ⁡ A
50 35 49 eqtrd ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℑ ⁡ i ⁢ A = ℜ ⁡ A
51 50 fveq2d ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → cos ⁡ ℑ ⁡ i ⁢ A = cos ⁡ ℜ ⁡ A
52 33 51 eqtrd ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℜ ⁡ cos ⁡ ℑ ⁡ i ⁢ A + i ⁢ sin ⁡ ℑ ⁡ i ⁢ A = cos ⁡ ℜ ⁡ A
53 52 oveq2d ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → e ℜ ⁡ i ⁢ A ⁢ ℜ ⁡ cos ⁡ ℑ ⁡ i ⁢ A + i ⁢ sin ⁡ ℑ ⁡ i ⁢ A = e ℜ ⁡ i ⁢ A ⁢ cos ⁡ ℜ ⁡ A
54 23 32 53 3eqtrd ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → ℜ ⁡ e i ⁢ A = e ℜ ⁡ i ⁢ A ⁢ cos ⁡ ℜ ⁡ A
55 20 54 breqtrrd ⊢ A ∈ ℂ ∧ ℜ ⁡ A ∈ − π 2 π 2 → 0 < ℜ ⁡ e i ⁢ A