asindmre

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

		Ref	Expression
	Hypothesis	dvasin.d	$⊢ D = ℂ ∖ ((−∞, - 1] \cup [1, +∞))$
	Assertion	asindmre	$⊢ D \cap ℝ = (- 1, 1)$

Proof

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

Metamath Proof Explorer

Theorem asindmre

Proof