Step | Hyp | Ref
| Expression |
1 | | un12 3771 |
. . . . 5
⊢ ((-1(,)1)
∪ ((-∞(,]-1) ∪ (1[,)+∞))) = ((-∞(,]-1) ∪
((-1(,)1) ∪ (1[,)+∞))) |
2 | | neg1rr 11125 |
. . . . . . . . . 10
⊢ -1 ∈
ℝ |
3 | 2 | rexri 10097 |
. . . . . . . . 9
⊢ -1 ∈
ℝ* |
4 | | 1re 10039 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
5 | 4 | rexri 10097 |
. . . . . . . . 9
⊢ 1 ∈
ℝ* |
6 | | pnfxr 10092 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
7 | 3, 5, 6 | 3pm3.2i 1239 |
. . . . . . . 8
⊢ (-1
∈ ℝ* ∧ 1 ∈ ℝ* ∧ +∞
∈ ℝ*) |
8 | | neg1lt0 11127 |
. . . . . . . . . 10
⊢ -1 <
0 |
9 | | 0lt1 10550 |
. . . . . . . . . 10
⊢ 0 <
1 |
10 | | 0re 10040 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
11 | 2, 10, 4 | lttri 10163 |
. . . . . . . . . 10
⊢ ((-1 <
0 ∧ 0 < 1) → -1 < 1) |
12 | 8, 9, 11 | mp2an 708 |
. . . . . . . . 9
⊢ -1 <
1 |
13 | | ltpnf 11954 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ → 1 < +∞) |
14 | 4, 13 | ax-mp 5 |
. . . . . . . . 9
⊢ 1 <
+∞ |
15 | 12, 14 | pm3.2i 471 |
. . . . . . . 8
⊢ (-1 <
1 ∧ 1 < +∞) |
16 | | df-ioo 12179 |
. . . . . . . . 9
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
17 | | df-ico 12181 |
. . . . . . . . 9
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
18 | | xrlenlt 10103 |
. . . . . . . . 9
⊢ ((1
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (1 ≤
𝑤 ↔ ¬ 𝑤 < 1)) |
19 | | xrlttr 11973 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℝ*
∧ 1 ∈ ℝ* ∧ +∞ ∈ ℝ*)
→ ((𝑤 < 1 ∧ 1
< +∞) → 𝑤
< +∞)) |
20 | | xrltletr 11988 |
. . . . . . . . 9
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
→ ((-1 < 1 ∧ 1 ≤ 𝑤) → -1 < 𝑤)) |
21 | 16, 17, 18, 16, 19, 20 | ixxun 12191 |
. . . . . . . 8
⊢ (((-1
∈ ℝ* ∧ 1 ∈ ℝ* ∧ +∞
∈ ℝ*) ∧ (-1 < 1 ∧ 1 < +∞)) →
((-1(,)1) ∪ (1[,)+∞)) = (-1(,)+∞)) |
22 | 7, 15, 21 | mp2an 708 |
. . . . . . 7
⊢ ((-1(,)1)
∪ (1[,)+∞)) = (-1(,)+∞) |
23 | 22 | uneq2i 3764 |
. . . . . 6
⊢
((-∞(,]-1) ∪ ((-1(,)1) ∪ (1[,)+∞))) =
((-∞(,]-1) ∪ (-1(,)+∞)) |
24 | | mnfxr 10096 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
25 | 24, 3, 6 | 3pm3.2i 1239 |
. . . . . . 7
⊢ (-∞
∈ ℝ* ∧ -1 ∈ ℝ* ∧ +∞
∈ ℝ*) |
26 | | mnflt 11957 |
. . . . . . . . 9
⊢ (-1
∈ ℝ → -∞ < -1) |
27 | | ltpnf 11954 |
. . . . . . . . 9
⊢ (-1
∈ ℝ → -1 < +∞) |
28 | 26, 27 | jca 554 |
. . . . . . . 8
⊢ (-1
∈ ℝ → (-∞ < -1 ∧ -1 <
+∞)) |
29 | 2, 28 | ax-mp 5 |
. . . . . . 7
⊢ (-∞
< -1 ∧ -1 < +∞) |
30 | | df-ioc 12180 |
. . . . . . . 8
⊢ (,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
31 | | xrltnle 10105 |
. . . . . . . 8
⊢ ((-1
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (-1 <
𝑤 ↔ ¬ 𝑤 ≤ -1)) |
32 | | xrlelttr 11987 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℝ*
∧ -1 ∈ ℝ* ∧ +∞ ∈ ℝ*)
→ ((𝑤 ≤ -1 ∧ -1
< +∞) → 𝑤
< +∞)) |
33 | | xrlttr 11973 |
. . . . . . . 8
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ 𝑤
∈ ℝ*) → ((-∞ < -1 ∧ -1 < 𝑤) → -∞ < 𝑤)) |
34 | 30, 16, 31, 16, 32, 33 | ixxun 12191 |
. . . . . . 7
⊢
(((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞
< -1 ∧ -1 < +∞)) → ((-∞(,]-1) ∪ (-1(,)+∞))
= (-∞(,)+∞)) |
35 | 25, 29, 34 | mp2an 708 |
. . . . . 6
⊢
((-∞(,]-1) ∪ (-1(,)+∞)) =
(-∞(,)+∞) |
36 | 23, 35 | eqtri 2644 |
. . . . 5
⊢
((-∞(,]-1) ∪ ((-1(,)1) ∪ (1[,)+∞))) =
(-∞(,)+∞) |
37 | | ioomax 12248 |
. . . . 5
⊢
(-∞(,)+∞) = ℝ |
38 | 1, 36, 37 | 3eqtri 2648 |
. . . 4
⊢ ((-1(,)1)
∪ ((-∞(,]-1) ∪ (1[,)+∞))) = ℝ |
39 | 38 | difeq1i 3724 |
. . 3
⊢
(((-1(,)1) ∪ ((-∞(,]-1) ∪ (1[,)+∞))) ∖
((-∞(,]-1) ∪ (1[,)+∞))) = (ℝ ∖ ((-∞(,]-1)
∪ (1[,)+∞))) |
40 | | difun2 4048 |
. . 3
⊢
(((-1(,)1) ∪ ((-∞(,]-1) ∪ (1[,)+∞))) ∖
((-∞(,]-1) ∪ (1[,)+∞))) = ((-1(,)1) ∖ ((-∞(,]-1)
∪ (1[,)+∞))) |
41 | | ax-resscn 9993 |
. . . 4
⊢ ℝ
⊆ ℂ |
42 | | difin2 3890 |
. . . 4
⊢ (ℝ
⊆ ℂ → (ℝ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
= ((ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∩
ℝ)) |
43 | 41, 42 | ax-mp 5 |
. . 3
⊢ (ℝ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) = ((ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) ∩ ℝ) |
44 | 39, 40, 43 | 3eqtr3ri 2653 |
. 2
⊢ ((ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∩ ℝ) = ((-1(,)1)
∖ ((-∞(,]-1) ∪ (1[,)+∞))) |
45 | | dvasin.d |
. . 3
⊢ 𝐷 = (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) |
46 | 45 | ineq1i 3810 |
. 2
⊢ (𝐷 ∩ ℝ) = ((ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∩ ℝ) |
47 | | incom 3805 |
. . . . 5
⊢ ((-1(,)1)
∩ (-∞(,]-1)) = ((-∞(,]-1) ∩ (-1(,)1)) |
48 | 30, 16, 31 | ixxdisj 12190 |
. . . . . 6
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ 1 ∈ ℝ*) → ((-∞(,]-1)
∩ (-1(,)1)) = ∅) |
49 | 24, 3, 5, 48 | mp3an 1424 |
. . . . 5
⊢
((-∞(,]-1) ∩ (-1(,)1)) = ∅ |
50 | 47, 49 | eqtri 2644 |
. . . 4
⊢ ((-1(,)1)
∩ (-∞(,]-1)) = ∅ |
51 | 16, 17, 18 | ixxdisj 12190 |
. . . . 5
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ* ∧ +∞
∈ ℝ*) → ((-1(,)1) ∩ (1[,)+∞)) =
∅) |
52 | 3, 5, 6, 51 | mp3an 1424 |
. . . 4
⊢ ((-1(,)1)
∩ (1[,)+∞)) = ∅ |
53 | 50, 52 | pm3.2i 471 |
. . 3
⊢
(((-1(,)1) ∩ (-∞(,]-1)) = ∅ ∧ ((-1(,)1) ∩
(1[,)+∞)) = ∅) |
54 | | un00 4011 |
. . . 4
⊢
((((-1(,)1) ∩ (-∞(,]-1)) = ∅ ∧ ((-1(,)1) ∩
(1[,)+∞)) = ∅) ↔ (((-1(,)1) ∩ (-∞(,]-1)) ∪
((-1(,)1) ∩ (1[,)+∞))) = ∅) |
55 | | indi 3873 |
. . . . 5
⊢ ((-1(,)1)
∩ ((-∞(,]-1) ∪ (1[,)+∞))) = (((-1(,)1) ∩
(-∞(,]-1)) ∪ ((-1(,)1) ∩ (1[,)+∞))) |
56 | 55 | eqeq1i 2627 |
. . . 4
⊢
(((-1(,)1) ∩ ((-∞(,]-1) ∪ (1[,)+∞))) = ∅
↔ (((-1(,)1) ∩ (-∞(,]-1)) ∪ ((-1(,)1) ∩ (1[,)+∞)))
= ∅) |
57 | | disj3 4021 |
. . . 4
⊢
(((-1(,)1) ∩ ((-∞(,]-1) ∪ (1[,)+∞))) = ∅
↔ (-1(,)1) = ((-1(,)1) ∖ ((-∞(,]-1) ∪
(1[,)+∞)))) |
58 | 54, 56, 57 | 3bitr2i 288 |
. . 3
⊢
((((-1(,)1) ∩ (-∞(,]-1)) = ∅ ∧ ((-1(,)1) ∩
(1[,)+∞)) = ∅) ↔ (-1(,)1) = ((-1(,)1) ∖ ((-∞(,]-1)
∪ (1[,)+∞)))) |
59 | 53, 58 | mpbi 220 |
. 2
⊢ (-1(,)1)
= ((-1(,)1) ∖ ((-∞(,]-1) ∪ (1[,)+∞))) |
60 | 44, 46, 59 | 3eqtr4i 2654 |
1
⊢ (𝐷 ∩ ℝ) =
(-1(,)1) |