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 ⊢ 𝐷 = ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) )
Assertion asindmre ( 𝐷 ∩ ℝ ) = ( - 1 (,) 1 )

Proof

Step Hyp Ref Expression
1 dvasin.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 ⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
18 df-ico ⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
19 xrlenlt ⊢ ( ( 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 1 ≤ 𝑤 ↔ ¬ 𝑤 < 1 ) )
20 xrlttr ⊢ ( ( 𝑤 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝑤 < 1 ∧ 1 < +∞ ) → 𝑤 < +∞ ) )
21 xrltletr ⊢ ( ( - 1 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( - 1 < 1 ∧ 1 ≤ 𝑤 ) → - 1 < 𝑤 ) )
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 ⊢ (,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
32 xrltnle ⊢ ( ( - 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( - 1 < 𝑤 ↔ ¬ 𝑤 ≤ - 1 ) )
33 xrlelttr ⊢ ( ( 𝑤 ∈ ℝ* ∧ - 1 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝑤 ≤ - 1 ∧ - 1 < +∞ ) → 𝑤 < +∞ ) )
34 xrlttr ⊢ ( ( -∞ ∈ ℝ* ∧ - 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( -∞ < - 1 ∧ - 1 < 𝑤 ) → -∞ < 𝑤 ) )
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 ⊢ ( 𝐷 ∩ ℝ ) = ( ( ℂ ∖ ( ( -∞ (,] - 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 ⊢ ( 𝐷 ∩ ℝ ) = ( - 1 (,) 1 )