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 = ℂ ∖ −∞ − 1 ∪ 1 +∞
Assertion asindmre ⊢ D ∩ ℝ = − 1 1

Proof

Step Hyp Ref Expression
1 dvasin.d ⊢ D = ℂ ∖ −∞ − 1 ∪ 1 +∞
2 un12 ⊢ − 1 1 ∪ −∞ − 1 ∪ 1 +∞ = −∞ − 1 ∪ − 1 1 ∪ 1 +∞
3 neg1rr ⊢ − 1 ∈ ℝ
4 3 rexri ⊢ − 1 ∈ ℝ *
5 1xr ⊢ 1 ∈ ℝ *
6 pnfxr ⊢ +∞ ∈ ℝ *
7 4 5 6 3pm3.2i ⊢ − 1 ∈ ℝ * ∧ 1 ∈ ℝ * ∧ +∞ ∈ ℝ *
8 neg1lt0 ⊢ − 1 < 0
9 0lt1 ⊢ 0 < 1
10 0re ⊢ 0 ∈ ℝ
11 1re ⊢ 1 ∈ ℝ
12 3 10 11 lttri ⊢ − 1 < 0 ∧ 0 < 1 → − 1 < 1
13 8 9 12 mp2an ⊢ − 1 < 1
14 ltpnf ⊢ 1 ∈ ℝ → 1 < +∞
15 11 14 ax-mp ⊢ 1 < +∞
16 13 15 pm3.2i ⊢ − 1 < 1 ∧ 1 < +∞
17 df-ioo ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x < z ∧ z < y
18 df-ico ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x ≤ z ∧ z < y
19 xrlenlt ⊢ 1 ∈ ℝ * ∧ w ∈ ℝ * → 1 ≤ w ↔ ¬ w < 1
20 xrlttr ⊢ w ∈ ℝ * ∧ 1 ∈ ℝ * ∧ +∞ ∈ ℝ * → w < 1 ∧ 1 < +∞ → w < +∞
21 xrltletr ⊢ − 1 ∈ ℝ * ∧ 1 ∈ ℝ * ∧ w ∈ ℝ * → − 1 < 1 ∧ 1 ≤ w → − 1 < w
22 17 18 19 17 20 21 ixxun ⊢ − 1 ∈ ℝ * ∧ 1 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ − 1 < 1 ∧ 1 < +∞ → − 1 1 ∪ 1 +∞ = − 1 +∞
23 7 16 22 mp2an ⊢ − 1 1 ∪ 1 +∞ = − 1 +∞
24 23 uneq2i ⊢ −∞ − 1 ∪ − 1 1 ∪ 1 +∞ = −∞ − 1 ∪ − 1 +∞
25 mnfxr ⊢ −∞ ∈ ℝ *
26 25 4 6 3pm3.2i ⊢ −∞ ∈ ℝ * ∧ − 1 ∈ ℝ * ∧ +∞ ∈ ℝ *
27 mnflt ⊢ − 1 ∈ ℝ → −∞ < − 1
28 ltpnf ⊢ − 1 ∈ ℝ → − 1 < +∞
29 27 28 jca ⊢ − 1 ∈ ℝ → −∞ < − 1 ∧ − 1 < +∞
30 3 29 ax-mp ⊢ −∞ < − 1 ∧ − 1 < +∞
31 df-ioc ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x < z ∧ z ≤ y
32 xrltnle ⊢ − 1 ∈ ℝ * ∧ w ∈ ℝ * → − 1 < w ↔ ¬ w ≤ − 1
33 xrlelttr ⊢ w ∈ ℝ * ∧ − 1 ∈ ℝ * ∧ +∞ ∈ ℝ * → w ≤ − 1 ∧ − 1 < +∞ → w < +∞
34 xrlttr ⊢ −∞ ∈ ℝ * ∧ − 1 ∈ ℝ * ∧ w ∈ ℝ * → −∞ < − 1 ∧ − 1 < w → −∞ < w
35 31 17 32 17 33 34 ixxun ⊢ −∞ ∈ ℝ * ∧ − 1 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ −∞ < − 1 ∧ − 1 < +∞ → −∞ − 1 ∪ − 1 +∞ = −∞ +∞
36 26 30 35 mp2an ⊢ −∞ − 1 ∪ − 1 +∞ = −∞ +∞
37 24 36 eqtri ⊢ −∞ − 1 ∪ − 1 1 ∪ 1 +∞ = −∞ +∞
38 ioomax ⊢ −∞ +∞ = ℝ
39 2 37 38 3eqtri ⊢ − 1 1 ∪ −∞ − 1 ∪ 1 +∞ = ℝ
40 39 difeq1i ⊢ − 1 1 ∪ −∞ − 1 ∪ 1 +∞ ∖ −∞ − 1 ∪ 1 +∞ = ℝ ∖ −∞ − 1 ∪ 1 +∞
41 difun2 ⊢ − 1 1 ∪ −∞ − 1 ∪ 1 +∞ ∖ −∞ − 1 ∪ 1 +∞ = − 1 1 ∖ −∞ − 1 ∪ 1 +∞
42 ax-resscn ⊢ ℝ ⊆ ℂ
43 difin2 ⊢ ℝ ⊆ ℂ → ℝ ∖ −∞ − 1 ∪ 1 +∞ = ℂ ∖ −∞ − 1 ∪ 1 +∞ ∩ ℝ
44 42 43 ax-mp ⊢ ℝ ∖ −∞ − 1 ∪ 1 +∞ = ℂ ∖ −∞ − 1 ∪ 1 +∞ ∩ ℝ
45 40 41 44 3eqtr3ri ⊢ ℂ ∖ −∞ − 1 ∪ 1 +∞ ∩ ℝ = − 1 1 ∖ −∞ − 1 ∪ 1 +∞
46 1 ineq1i ⊢ D ∩ ℝ = ℂ ∖ −∞ − 1 ∪ 1 +∞ ∩ ℝ
47 incom ⊢ − 1 1 ∩ −∞ − 1 = −∞ − 1 ∩ − 1 1
48 31 17 32 ixxdisj ⊢ −∞ ∈ ℝ * ∧ − 1 ∈ ℝ * ∧ 1 ∈ ℝ * → −∞ − 1 ∩ − 1 1 = ∅
49 25 4 5 48 mp3an ⊢ −∞ − 1 ∩ − 1 1 = ∅
50 47 49 eqtri ⊢ − 1 1 ∩ −∞ − 1 = ∅
51 17 18 19 ixxdisj ⊢ − 1 ∈ ℝ * ∧ 1 ∈ ℝ * ∧ +∞ ∈ ℝ * → − 1 1 ∩ 1 +∞ = ∅
52 4 5 6 51 mp3an ⊢ − 1 1 ∩ 1 +∞ = ∅
53 50 52 pm3.2i ⊢ − 1 1 ∩ −∞ − 1 = ∅ ∧ − 1 1 ∩ 1 +∞ = ∅
54 un00 ⊢ − 1 1 ∩ −∞ − 1 = ∅ ∧ − 1 1 ∩ 1 +∞ = ∅ ↔ − 1 1 ∩ −∞ − 1 ∪ − 1 1 ∩ 1 +∞ = ∅
55 indi ⊢ − 1 1 ∩ −∞ − 1 ∪ 1 +∞ = − 1 1 ∩ −∞ − 1 ∪ − 1 1 ∩ 1 +∞
56 55 eqeq1i ⊢ − 1 1 ∩ −∞ − 1 ∪ 1 +∞ = ∅ ↔ − 1 1 ∩ −∞ − 1 ∪ − 1 1 ∩ 1 +∞ = ∅
57 disj3 ⊢ − 1 1 ∩ −∞ − 1 ∪ 1 +∞ = ∅ ↔ − 1 1 = − 1 1 ∖ −∞ − 1 ∪ 1 +∞
58 54 56 57 3bitr2i ⊢ − 1 1 ∩ −∞ − 1 = ∅ ∧ − 1 1 ∩ 1 +∞ = ∅ ↔ − 1 1 = − 1 1 ∖ −∞ − 1 ∪ 1 +∞
59 53 58 mpbi ⊢ − 1 1 = − 1 1 ∖ −∞ − 1 ∪ 1 +∞
60 45 46 59 3eqtr4i ⊢ D ∩ ℝ = − 1 1