Metamath Proof Explorer


Theorem asinlem3

Description: The argument to the logarithm in df-asin has nonnegative real part. (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion asinlem3 A 0 i A + 1 A 2

Proof

Step Hyp Ref Expression
1 0red A 0
2 imcl A A
3 ax-icn i
4 negcl A A
5 4 adantr A 0 A A
6 mulcl i A i A
7 3 5 6 sylancr A 0 A i A
8 ax-1cn 1
9 5 sqcld A 0 A A 2
10 subcl 1 A 2 1 A 2
11 8 9 10 sylancr A 0 A 1 A 2
12 11 sqrtcld A 0 A 1 A 2
13 7 12 addcld A 0 A i A + 1 A 2
14 asinlem A i A + 1 A 2 0
15 5 14 syl A 0 A i A + 1 A 2 0
16 13 15 absrpcld A 0 A i A + 1 A 2 +
17 2z 2
18 rpexpcl i A + 1 A 2 + 2 i A + 1 A 2 2 +
19 16 17 18 sylancl A 0 A i A + 1 A 2 2 +
20 19 rprecred A 0 A 1 i A + 1 A 2 2
21 13 cjcld A 0 A i A + 1 A 2
22 21 recld A 0 A i A + 1 A 2
23 19 rpreccld A 0 A 1 i A + 1 A 2 2 +
24 23 rpge0d A 0 A 0 1 i A + 1 A 2 2
25 imneg A A = A
26 25 adantr A 0 A A = A
27 2 le0neg2d A 0 A A 0
28 27 biimpa A 0 A A 0
29 26 28 eqbrtrd A 0 A A 0
30 asinlem3a A A 0 0 i A + 1 A 2
31 5 29 30 syl2anc A 0 A 0 i A + 1 A 2
32 13 recjd A 0 A i A + 1 A 2 = i A + 1 A 2
33 31 32 breqtrrd A 0 A 0 i A + 1 A 2
34 20 22 24 33 mulge0d A 0 A 0 1 i A + 1 A 2 2 i A + 1 A 2
35 recval i A + 1 A 2 i A + 1 A 2 0 1 i A + 1 A 2 = i A + 1 A 2 i A + 1 A 2 2
36 13 15 35 syl2anc A 0 A 1 i A + 1 A 2 = i A + 1 A 2 i A + 1 A 2 2
37 asinlem2 A i A + 1 A 2 i A + 1 A 2 = 1
38 37 adantr A 0 A i A + 1 A 2 i A + 1 A 2 = 1
39 38 eqcomd A 0 A 1 = i A + 1 A 2 i A + 1 A 2
40 1cnd A 0 A 1
41 simpl A 0 A A
42 mulcl i A i A
43 3 41 42 sylancr A 0 A i A
44 sqcl A A 2
45 44 adantr A 0 A A 2
46 subcl 1 A 2 1 A 2
47 8 45 46 sylancr A 0 A 1 A 2
48 47 sqrtcld A 0 A 1 A 2
49 43 48 addcld A 0 A i A + 1 A 2
50 40 49 13 15 divmul3d A 0 A 1 i A + 1 A 2 = i A + 1 A 2 1 = i A + 1 A 2 i A + 1 A 2
51 39 50 mpbird A 0 A 1 i A + 1 A 2 = i A + 1 A 2
52 19 rpcnd A 0 A i A + 1 A 2 2
53 19 rpne0d A 0 A i A + 1 A 2 2 0
54 21 52 53 divrec2d A 0 A i A + 1 A 2 i A + 1 A 2 2 = 1 i A + 1 A 2 2 i A + 1 A 2
55 36 51 54 3eqtr3d A 0 A i A + 1 A 2 = 1 i A + 1 A 2 2 i A + 1 A 2
56 55 fveq2d A 0 A i A + 1 A 2 = 1 i A + 1 A 2 2 i A + 1 A 2
57 20 21 remul2d A 0 A 1 i A + 1 A 2 2 i A + 1 A 2 = 1 i A + 1 A 2 2 i A + 1 A 2
58 56 57 eqtrd A 0 A i A + 1 A 2 = 1 i A + 1 A 2 2 i A + 1 A 2
59 34 58 breqtrrd A 0 A 0 i A + 1 A 2
60 asinlem3a A A 0 0 i A + 1 A 2
61 1 2 59 60 lecasei A 0 i A + 1 A 2