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