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 mulid2 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