Metamath Proof Explorer


Theorem asinf

Description: Domain and codomain 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=xilogix+1x2
2 negicn i
3 ax-icn i
4 mulcl ixix
5 3 4 mpan xix
6 ax-1cn 1
7 sqcl xx2
8 subcl 1x21x2
9 6 7 8 sylancr x1x2
10 9 sqrtcld x1x2
11 5 10 addcld xix+1x2
12 asinlem xix+1x20
13 11 12 logcld xlogix+1x2
14 mulcl ilogix+1x2ilogix+1x2
15 2 13 14 sylancr xilogix+1x2
16 1 15 fmpti arcsin: