# Metamath Proof Explorer

## Theorem asinsinlem

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

Ref Expression
Assertion asinsinlem ${⊢}\left({A}\in ℂ\wedge \Re \left({A}\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\right)\to 0<\Re \left({\mathrm{e}}^{\mathrm{i}{A}}\right)$

### Proof

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