Metamath Proof Explorer

Theorem asindmre

Description: Real part of domain of differentiability of arcsine. (Contributed by Brendan Leahy, 19-Dec-2018)

Ref Expression
Hypothesis dvasin.d 
|- D = ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
Assertion asindmre 
|- ( D i^i RR ) = ( -u 1 (,) 1 )

Proof

Step Hyp Ref Expression
1 dvasin.d 
 |-  D = ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
2 un12 
 |-  ( ( -u 1 (,) 1 ) u. ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) = ( ( -oo (,] -u 1 ) u. ( ( -u 1 (,) 1 ) u. ( 1 [,) +oo ) ) )
3 neg1rr 
 |-  -u 1 e. RR
4 3 rexri 
 |-  -u 1 e. RR*
5 1xr 
 |-  1 e. RR*
6 pnfxr 
 |-  +oo e. RR*
7 4 5 6 3pm3.2i 
 |-  ( -u 1 e. RR* /\ 1 e. RR* /\ +oo e. RR* )
8 neg1lt0 
 |-  -u 1 < 0
9 0lt1 
 |-  0 < 1
10 0re 
 |-  0 e. RR
11 1re 
 |-  1 e. RR
12 3 10 11 lttri 
 |-  ( ( -u 1 < 0 /\ 0 < 1 ) -> -u 1 < 1 )
13 8 9 12 mp2an 
 |-  -u 1 < 1
14 ltpnf 
 |-  ( 1 e. RR -> 1 < +oo )
15 11 14 ax-mp 
 |-  1 < +oo
16 13 15 pm3.2i 
 |-  ( -u 1 < 1 /\ 1 < +oo )
17 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
18 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
19 xrlenlt 
 |-  ( ( 1 e. RR* /\ w e. RR* ) -> ( 1 <_ w <-> -. w < 1 ) )
20 xrlttr 
 |-  ( ( w e. RR* /\ 1 e. RR* /\ +oo e. RR* ) -> ( ( w < 1 /\ 1 < +oo ) -> w < +oo ) )
21 xrltletr 
 |-  ( ( -u 1 e. RR* /\ 1 e. RR* /\ w e. RR* ) -> ( ( -u 1 < 1 /\ 1 <_ w ) -> -u 1 < w ) )
22 17 18 19 17 20 21 ixxun 
 |-  ( ( ( -u 1 e. RR* /\ 1 e. RR* /\ +oo e. RR* ) /\ ( -u 1 < 1 /\ 1 < +oo ) ) -> ( ( -u 1 (,) 1 ) u. ( 1 [,) +oo ) ) = ( -u 1 (,) +oo ) )
23 7 16 22 mp2an 
 |-  ( ( -u 1 (,) 1 ) u. ( 1 [,) +oo ) ) = ( -u 1 (,) +oo )
24 23 uneq2i 
 |-  ( ( -oo (,] -u 1 ) u. ( ( -u 1 (,) 1 ) u. ( 1 [,) +oo ) ) ) = ( ( -oo (,] -u 1 ) u. ( -u 1 (,) +oo ) )
25 mnfxr 
 |-  -oo e. RR*
26 25 4 6 3pm3.2i 
 |-  ( -oo e. RR* /\ -u 1 e. RR* /\ +oo e. RR* )
27 mnflt 
 |-  ( -u 1 e. RR -> -oo < -u 1 )
28 ltpnf 
 |-  ( -u 1 e. RR -> -u 1 < +oo )
29 27 28 jca 
 |-  ( -u 1 e. RR -> ( -oo < -u 1 /\ -u 1 < +oo ) )
30 3 29 ax-mp 
 |-  ( -oo < -u 1 /\ -u 1 < +oo )
31 df-ioc 
 |-  (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
32 xrltnle 
 |-  ( ( -u 1 e. RR* /\ w e. RR* ) -> ( -u 1 < w <-> -. w <_ -u 1 ) )
33 xrlelttr 
 |-  ( ( w e. RR* /\ -u 1 e. RR* /\ +oo e. RR* ) -> ( ( w <_ -u 1 /\ -u 1 < +oo ) -> w < +oo ) )
34 xrlttr 
 |-  ( ( -oo e. RR* /\ -u 1 e. RR* /\ w e. RR* ) -> ( ( -oo < -u 1 /\ -u 1 < w ) -> -oo < w ) )
35 31 17 32 17 33 34 ixxun 
 |-  ( ( ( -oo e. RR* /\ -u 1 e. RR* /\ +oo e. RR* ) /\ ( -oo < -u 1 /\ -u 1 < +oo ) ) -> ( ( -oo (,] -u 1 ) u. ( -u 1 (,) +oo ) ) = ( -oo (,) +oo ) )
36 26 30 35 mp2an 
 |-  ( ( -oo (,] -u 1 ) u. ( -u 1 (,) +oo ) ) = ( -oo (,) +oo )
37 24 36 eqtri 
 |-  ( ( -oo (,] -u 1 ) u. ( ( -u 1 (,) 1 ) u. ( 1 [,) +oo ) ) ) = ( -oo (,) +oo )
38 ioomax 
 |-  ( -oo (,) +oo ) = RR
39 2 37 38 3eqtri 
 |-  ( ( -u 1 (,) 1 ) u. ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) = RR
40 39 difeq1i 
 |-  ( ( ( -u 1 (,) 1 ) u. ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) = ( RR \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
41 difun2 
 |-  ( ( ( -u 1 (,) 1 ) u. ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) = ( ( -u 1 (,) 1 ) \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
42 ax-resscn 
 |-  RR C_ CC
43 difin2 
 |-  ( RR C_ CC -> ( RR \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) = ( ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) i^i RR ) )
44 42 43 ax-mp 
 |-  ( RR \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) = ( ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) i^i RR )
45 40 41 44 3eqtr3ri 
 |-  ( ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) i^i RR ) = ( ( -u 1 (,) 1 ) \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
46 1 ineq1i 
 |-  ( D i^i RR ) = ( ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) i^i RR )
47 incom 
 |-  ( ( -u 1 (,) 1 ) i^i ( -oo (,] -u 1 ) ) = ( ( -oo (,] -u 1 ) i^i ( -u 1 (,) 1 ) )
48 31 17 32 ixxdisj 
 |-  ( ( -oo e. RR* /\ -u 1 e. RR* /\ 1 e. RR* ) -> ( ( -oo (,] -u 1 ) i^i ( -u 1 (,) 1 ) ) = (/) )
49 25 4 5 48 mp3an 
 |-  ( ( -oo (,] -u 1 ) i^i ( -u 1 (,) 1 ) ) = (/)
50 47 49 eqtri 
 |-  ( ( -u 1 (,) 1 ) i^i ( -oo (,] -u 1 ) ) = (/)
51 17 18 19 ixxdisj 
 |-  ( ( -u 1 e. RR* /\ 1 e. RR* /\ +oo e. RR* ) -> ( ( -u 1 (,) 1 ) i^i ( 1 [,) +oo ) ) = (/) )
52 4 5 6 51 mp3an 
 |-  ( ( -u 1 (,) 1 ) i^i ( 1 [,) +oo ) ) = (/)
53 50 52 pm3.2i 
 |-  ( ( ( -u 1 (,) 1 ) i^i ( -oo (,] -u 1 ) ) = (/) /\ ( ( -u 1 (,) 1 ) i^i ( 1 [,) +oo ) ) = (/) )
54 un00 
 |-  ( ( ( ( -u 1 (,) 1 ) i^i ( -oo (,] -u 1 ) ) = (/) /\ ( ( -u 1 (,) 1 ) i^i ( 1 [,) +oo ) ) = (/) ) <-> ( ( ( -u 1 (,) 1 ) i^i ( -oo (,] -u 1 ) ) u. ( ( -u 1 (,) 1 ) i^i ( 1 [,) +oo ) ) ) = (/) )
55 indi 
 |-  ( ( -u 1 (,) 1 ) i^i ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) = ( ( ( -u 1 (,) 1 ) i^i ( -oo (,] -u 1 ) ) u. ( ( -u 1 (,) 1 ) i^i ( 1 [,) +oo ) ) )
56 55 eqeq1i 
 |-  ( ( ( -u 1 (,) 1 ) i^i ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) = (/) <-> ( ( ( -u 1 (,) 1 ) i^i ( -oo (,] -u 1 ) ) u. ( ( -u 1 (,) 1 ) i^i ( 1 [,) +oo ) ) ) = (/) )
57 disj3 
 |-  ( ( ( -u 1 (,) 1 ) i^i ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) = (/) <-> ( -u 1 (,) 1 ) = ( ( -u 1 (,) 1 ) \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) )
58 54 56 57 3bitr2i 
 |-  ( ( ( ( -u 1 (,) 1 ) i^i ( -oo (,] -u 1 ) ) = (/) /\ ( ( -u 1 (,) 1 ) i^i ( 1 [,) +oo ) ) = (/) ) <-> ( -u 1 (,) 1 ) = ( ( -u 1 (,) 1 ) \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) )
59 53 58 mpbi 
 |-  ( -u 1 (,) 1 ) = ( ( -u 1 (,) 1 ) \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
60 45 46 59 3eqtr4i 
 |-  ( D i^i RR ) = ( -u 1 (,) 1 )