asindmre - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > asindmre		Structured version Visualization version GIF version

Theorem asindmre 38728

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

**Hypothesis**
Ref	Expression
dvasin.d	⊢ 𝐷 = (ℂ ∖ ((-∞(,] -1) ∪ (1[,)+∞)))

**Assertion**
Ref	Expression
asindmre	⊢ (𝐷 ∩ ℝ) = ( -1(,)1)

Proof of Theorem asindmre Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		un12 4170	. . . . 5 ⊢ (( -1(,)1) ∪ ((-∞(,] -1) ∪ (1[,)+∞))) = ((-∞(,] -1) ∪ (( -1(,)1) ∪ (1[,)+∞)))
2		neg1rr 12311	. . . . . . . . . 10 ⊢ -1 ∈ ℝ
3	2	rexri 11372	. . . . . . . . 9 ⊢ -1 ∈ ℝ^*
4		1xr 11373	. . . . . . . . 9 ⊢ 1 ∈ ℝ^*
5		pnfxr 11368	. . . . . . . . 9 ⊢ +∞ ∈ ℝ^*
6	3, 4, 5	3pm3.2i 1358	. . . . . . . 8 ⊢ ( -1 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ +∞ ∈ ℝ^*)
7		neg1lt0 12313	. . . . . . . . . 10 ⊢ -1 < 0
8		0lt1 11843	. . . . . . . . . 10 ⊢ 0 < 1
9		0re 11315	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
10		1re 11313	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
11	2, 9, 10	lttri 11441	. . . . . . . . . 10 ⊢ (( -1 < 0 ∧ 0 < 1) → -1 < 1)
12	7, 8, 11	mp2an 705	. . . . . . . . 9 ⊢ -1 < 1
13		ltpnf 13254	. . . . . . . . . 10 ⊢ (1 ∈ ℝ → 1 < +∞)
14	10, 13	ax-mp 5	. . . . . . . . 9 ⊢ 1 < +∞
15	12, 14	pm3.2i 476	. . . . . . . 8 ⊢ ( -1 < 1 ∧ 1 < +∞)
16		df-ioo 13485	. . . . . . . . 9 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
17		df-ico 13487	. . . . . . . . 9 ⊢ [,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
18		xrlenlt 11379	. . . . . . . . 9 ⊢ ((1 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (1 ≤ 𝑤 ↔ ¬ 𝑤 < 1))
19		xrlttr 13274	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝑤 < 1 ∧ 1 < +∞) → 𝑤 < +∞))
20		xrltletr 13291	. . . . . . . . 9 ⊢ (( -1 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (( -1 < 1 ∧ 1 ≤ 𝑤) → -1 < 𝑤))
21	16, 17, 18, 16, 19, 20	ixxun 13497	. . . . . . . 8 ⊢ ((( -1 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ ( -1 < 1 ∧ 1 < +∞)) → (( -1(,)1) ∪ (1[,)+∞)) = ( -1(,)+∞))
22	6, 15, 21	mp2an 705	. . . . . . 7 ⊢ (( -1(,)1) ∪ (1[,)+∞)) = ( -1(,)+∞)
23	22	uneq2i 4163	. . . . . 6 ⊢ ((-∞(,] -1) ∪ (( -1(,)1) ∪ (1[,)+∞))) = ((-∞(,] -1) ∪ ( -1(,)+∞))
24		mnfxr 11371	. . . . . . . 8 ⊢ -∞ ∈ ℝ^*
25	24, 3, 5	3pm3.2i 1358	. . . . . . 7 ⊢ (-∞ ∈ ℝ^* ∧ -1 ∈ ℝ^* ∧ +∞ ∈ ℝ^*)
26		mnflt 13257	. . . . . . . . 9 ⊢ ( -1 ∈ ℝ → -∞ < -1)
27		ltpnf 13254	. . . . . . . . 9 ⊢ ( -1 ∈ ℝ → -1 < +∞)
28	26, 27	jca 521	. . . . . . . 8 ⊢ ( -1 ∈ ℝ → (-∞ < -1 ∧ -1 < +∞))
29	2, 28	ax-mp 5	. . . . . . 7 ⊢ (-∞ < -1 ∧ -1 < +∞)
30		df-ioc 13486	. . . . . . . 8 ⊢ (,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
31		xrltnle 11381	. . . . . . . 8 ⊢ (( -1 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → ( -1 < 𝑤 ↔ ¬ 𝑤 ≤ -1))
32		xrlelttr 13290	. . . . . . . 8 ⊢ ((𝑤 ∈ ℝ^* ∧ -1 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((𝑤 ≤ -1 ∧ -1 < +∞) → 𝑤 < +∞))
33		xrlttr 13274	. . . . . . . 8 ⊢ ((-∞ ∈ ℝ^* ∧ -1 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → ((-∞ < -1 ∧ -1 < 𝑤) → -∞ < 𝑤))
34	30, 16, 31, 16, 32, 33	ixxun 13497	. . . . . . 7 ⊢ (((-∞ ∈ ℝ^* ∧ -1 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ < -1 ∧ -1 < +∞)) → ((-∞(,] -1) ∪ ( -1(,)+∞)) = (-∞(,)+∞))
35	25, 29, 34	mp2an 705	. . . . . 6 ⊢ ((-∞(,] -1) ∪ ( -1(,)+∞)) = (-∞(,)+∞)
36	23, 35	eqtri 2783	. . . . 5 ⊢ ((-∞(,] -1) ∪ (( -1(,)1) ∪ (1[,)+∞))) = (-∞(,)+∞)
37		ioomax 13558	. . . . 5 ⊢ (-∞(,)+∞) = ℝ
38	1, 36, 37	3eqtri 2787	. . . 4 ⊢ (( -1(,)1) ∪ ((-∞(,] -1) ∪ (1[,)+∞))) = ℝ
39	38	difeq1i 4058	. . 3 ⊢ ((( -1(,)1) ∪ ((-∞(,] -1) ∪ (1[,)+∞))) ∖ ((-∞(,] -1) ∪ (1[,)+∞))) = (ℝ ∖ ((-∞(,] -1) ∪ (1[,)+∞)))
40		difun2 4436	. . 3 ⊢ ((( -1(,)1) ∪ ((-∞(,] -1) ∪ (1[,)+∞))) ∖ ((-∞(,] -1) ∪ (1[,)+∞))) = (( -1(,)1) ∖ ((-∞(,] -1) ∪ (1[,)+∞)))
41		ax-resscn 11262	. . . 4 ⊢ ℝ ⊆ ℂ
42		difin2 4245	. . . 4 ⊢ (ℝ ⊆ ℂ → (ℝ ∖ ((-∞(,] -1) ∪ (1[,)+∞))) = ((ℂ ∖ ((-∞(,] -1) ∪ (1[,)+∞))) ∩ ℝ))
43	41, 42	ax-mp 5	. . 3 ⊢ (ℝ ∖ ((-∞(,] -1) ∪ (1[,)+∞))) = ((ℂ ∖ ((-∞(,] -1) ∪ (1[,)+∞))) ∩ ℝ)
44	39, 40, 43	3eqtr3ri 2792	. 2 ⊢ ((ℂ ∖ ((-∞(,] -1) ∪ (1[,)+∞))) ∩ ℝ) = (( -1(,)1) ∖ ((-∞(,] -1) ∪ (1[,)+∞)))
45		dvasin.d	. . 3 ⊢ 𝐷 = (ℂ ∖ ((-∞(,] -1) ∪ (1[,)+∞)))
46	45	ineq1i 4112	. 2 ⊢ (𝐷 ∩ ℝ) = ((ℂ ∖ ((-∞(,] -1) ∪ (1[,)+∞))) ∩ ℝ)
47		incom 4105	. . . . 5 ⊢ (( -1(,)1) ∩ (-∞(,] -1)) = ((-∞(,] -1) ∩ ( -1(,)1))
48	30, 16, 31	ixxdisj 13496	. . . . . 6 ⊢ ((-∞ ∈ ℝ^* ∧ -1 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → ((-∞(,] -1) ∩ ( -1(,)1)) = ∅)
49	24, 3, 4, 48	mp3an 1490	. . . . 5 ⊢ ((-∞(,] -1) ∩ ( -1(,)1)) = ∅
50	47, 49	eqtri 2783	. . . 4 ⊢ (( -1(,)1) ∩ (-∞(,] -1)) = ∅
51	16, 17, 18	ixxdisj 13496	. . . . 5 ⊢ (( -1 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (( -1(,)1) ∩ (1[,)+∞)) = ∅)
52	3, 4, 5, 51	mp3an 1490	. . . 4 ⊢ (( -1(,)1) ∩ (1[,)+∞)) = ∅
53	50, 52	pm3.2i 476	. . 3 ⊢ ((( -1(,)1) ∩ (-∞(,] -1)) = ∅ ∧ (( -1(,)1) ∩ (1[,)+∞)) = ∅)
54		un00 4356	. . . 4 ⊢ (((( -1(,)1) ∩ (-∞(,] -1)) = ∅ ∧ (( -1(,)1) ∩ (1[,)+∞)) = ∅) ↔ ((( -1(,)1) ∩ (-∞(,] -1)) ∪ (( -1(,)1) ∩ (1[,)+∞))) = ∅)
55		indi 4228	. . . . 5 ⊢ (( -1(,)1) ∩ ((-∞(,] -1) ∪ (1[,)+∞))) = ((( -1(,)1) ∩ (-∞(,] -1)) ∪ (( -1(,)1) ∩ (1[,)+∞)))
56	55	eqeq1i 2765	. . . 4 ⊢ ((( -1(,)1) ∩ ((-∞(,] -1) ∪ (1[,)+∞))) = ∅ ↔ ((( -1(,)1) ∩ (-∞(,] -1)) ∪ (( -1(,)1) ∩ (1[,)+∞))) = ∅)
57		disj3 4406	. . . 4 ⊢ ((( -1(,)1) ∩ ((-∞(,] -1) ∪ (1[,)+∞))) = ∅ ↔ ( -1(,)1) = (( -1(,)1) ∖ ((-∞(,] -1) ∪ (1[,)+∞))))
58	54, 56, 57	3bitr2i 302	. . 3 ⊢ (((( -1(,)1) ∩ (-∞(,] -1)) = ∅ ∧ (( -1(,)1) ∩ (1[,)+∞)) = ∅) ↔ ( -1(,)1) = (( -1(,)1) ∖ ((-∞(,] -1) ∪ (1[,)+∞))))
59	53, 58	mpbi 233	. 2 ⊢ ( -1(,)1) = (( -1(,)1) ∖ ((-∞(,] -1) ∪ (1[,)+∞)))
60	44, 46, 59	3eqtr4i 2793	1 ⊢ (𝐷 ∩ ℝ) = ( -1(,)1)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ⊆ wss 3896 ∖ cdif 4044 ∩ cin 4088 ∪ cun 4148 ∅c0 4277 class class class wbr 5102 (class class class)co 7422 ℂcc 11203 ℝcr 11204 0cc0 11205 1c1 11206 +∞cpnf 11345 -∞cmnf 11346 ℝ^*cxr 11347 < clt 11348 ≤ cle 11349 -cneg 11547 (,)cioo 13481 (,]cioc 13482 [,)cico 13483

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7753 ax-cnex 11261 ax-resscn 11262 ax-1cn 11263 ax-icn 11264 ax-addcl 11265 ax-addrcl 11266 ax-mulcl 11267 ax-mulrcl 11268 ax-mulcom 11269 ax-addass 11270 ax-mulass 11271 ax-distr 11272 ax-i2m1 11273 ax-1ne0 11274 ax-1rid 11275 ax-rnegex 11276 ax-rrecex 11277 ax-cnre 11278 ax-pre-lttri 11279 ax-pre-lttrn 11280 ax-pre-ltadd 11281 ax-pre-mulgt0 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-po 5558 df-so 5559 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6496 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7379 df-ov 7425 df-oprab 7426 df-mpo 7427 df-1st 8003 df-2nd 8004 df-er 8722 df-en 8979 df-dom 8980 df-sdom 8981 df-pnf 11350 df-mnf 11351 df-xr 11352 df-ltxr 11353 df-le 11354 df-sub 11548 df-neg 11549 df-ioo 13485 df-ioc 13486 df-ico 13487

This theorem is used by: dvasin 38729 dvreasin 38731 dvreacos 38732

W3C validator