Metamath Proof Explorer


Theorem asinf

Description: Domain and range of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion asinf arcsin :

Proof

Step Hyp Ref Expression
1 df-asin arcsin = x i log i x + 1 x 2
2 negicn i
3 ax-icn i
4 mulcl i x i x
5 3 4 mpan x i x
6 ax-1cn 1
7 sqcl x x 2
8 subcl 1 x 2 1 x 2
9 6 7 8 sylancr x 1 x 2
10 9 sqrtcld x 1 x 2
11 5 10 addcld x i x + 1 x 2
12 asinlem x i x + 1 x 2 0
13 11 12 logcld x log i x + 1 x 2
14 mulcl i log i x + 1 x 2 i log i x + 1 x 2
15 2 13 14 sylancr x i log i x + 1 x 2
16 1 15 fmpti arcsin :