Step | Hyp | Ref
| Expression |
1 | | un12 4095 |
. . . . 5
⊢ ((-1(,)1)
∪ ((-∞(,]-1) ∪ (1[,)+∞))) = ((-∞(,]-1) ∪
((-1(,)1) ∪ (1[,)+∞))) |
2 | | neg1rr 11969 |
. . . . . . . . . 10
⊢ -1 ∈
ℝ |
3 | 2 | rexri 10915 |
. . . . . . . . 9
⊢ -1 ∈
ℝ* |
4 | | 1xr 10916 |
. . . . . . . . 9
⊢ 1 ∈
ℝ* |
5 | | pnfxr 10911 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
6 | 3, 4, 5 | 3pm3.2i 1341 |
. . . . . . . 8
⊢ (-1
∈ ℝ* ∧ 1 ∈ ℝ* ∧ +∞
∈ ℝ*) |
7 | | neg1lt0 11971 |
. . . . . . . . . 10
⊢ -1 <
0 |
8 | | 0lt1 11378 |
. . . . . . . . . 10
⊢ 0 <
1 |
9 | | 0re 10859 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
10 | | 1re 10857 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
11 | 2, 9, 10 | lttri 10982 |
. . . . . . . . . 10
⊢ ((-1 <
0 ∧ 0 < 1) → -1 < 1) |
12 | 7, 8, 11 | mp2an 692 |
. . . . . . . . 9
⊢ -1 <
1 |
13 | | ltpnf 12736 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ → 1 < +∞) |
14 | 10, 13 | ax-mp 5 |
. . . . . . . . 9
⊢ 1 <
+∞ |
15 | 12, 14 | pm3.2i 474 |
. . . . . . . 8
⊢ (-1 <
1 ∧ 1 < +∞) |
16 | | df-ioo 12963 |
. . . . . . . . 9
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
17 | | df-ico 12965 |
. . . . . . . . 9
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
18 | | xrlenlt 10922 |
. . . . . . . . 9
⊢ ((1
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (1 ≤
𝑤 ↔ ¬ 𝑤 < 1)) |
19 | | xrlttr 12754 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℝ*
∧ 1 ∈ ℝ* ∧ +∞ ∈ ℝ*)
→ ((𝑤 < 1 ∧ 1
< +∞) → 𝑤
< +∞)) |
20 | | xrltletr 12771 |
. . . . . . . . 9
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
→ ((-1 < 1 ∧ 1 ≤ 𝑤) → -1 < 𝑤)) |
21 | 16, 17, 18, 16, 19, 20 | ixxun 12975 |
. . . . . . . 8
⊢ (((-1
∈ ℝ* ∧ 1 ∈ ℝ* ∧ +∞
∈ ℝ*) ∧ (-1 < 1 ∧ 1 < +∞)) →
((-1(,)1) ∪ (1[,)+∞)) = (-1(,)+∞)) |
22 | 6, 15, 21 | mp2an 692 |
. . . . . . 7
⊢ ((-1(,)1)
∪ (1[,)+∞)) = (-1(,)+∞) |
23 | 22 | uneq2i 4088 |
. . . . . 6
⊢
((-∞(,]-1) ∪ ((-1(,)1) ∪ (1[,)+∞))) =
((-∞(,]-1) ∪ (-1(,)+∞)) |
24 | | mnfxr 10914 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
25 | 24, 3, 5 | 3pm3.2i 1341 |
. . . . . . 7
⊢ (-∞
∈ ℝ* ∧ -1 ∈ ℝ* ∧ +∞
∈ ℝ*) |
26 | | mnflt 12739 |
. . . . . . . . 9
⊢ (-1
∈ ℝ → -∞ < -1) |
27 | | ltpnf 12736 |
. . . . . . . . 9
⊢ (-1
∈ ℝ → -1 < +∞) |
28 | 26, 27 | jca 515 |
. . . . . . . 8
⊢ (-1
∈ ℝ → (-∞ < -1 ∧ -1 <
+∞)) |
29 | 2, 28 | ax-mp 5 |
. . . . . . 7
⊢ (-∞
< -1 ∧ -1 < +∞) |
30 | | df-ioc 12964 |
. . . . . . . 8
⊢ (,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
31 | | xrltnle 10924 |
. . . . . . . 8
⊢ ((-1
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (-1 <
𝑤 ↔ ¬ 𝑤 ≤ -1)) |
32 | | xrlelttr 12770 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℝ*
∧ -1 ∈ ℝ* ∧ +∞ ∈ ℝ*)
→ ((𝑤 ≤ -1 ∧ -1
< +∞) → 𝑤
< +∞)) |
33 | | xrlttr 12754 |
. . . . . . . 8
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ 𝑤
∈ ℝ*) → ((-∞ < -1 ∧ -1 < 𝑤) → -∞ < 𝑤)) |
34 | 30, 16, 31, 16, 32, 33 | ixxun 12975 |
. . . . . . 7
⊢
(((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞
< -1 ∧ -1 < +∞)) → ((-∞(,]-1) ∪ (-1(,)+∞))
= (-∞(,)+∞)) |
35 | 25, 29, 34 | mp2an 692 |
. . . . . 6
⊢
((-∞(,]-1) ∪ (-1(,)+∞)) =
(-∞(,)+∞) |
36 | 23, 35 | eqtri 2766 |
. . . . 5
⊢
((-∞(,]-1) ∪ ((-1(,)1) ∪ (1[,)+∞))) =
(-∞(,)+∞) |
37 | | ioomax 13034 |
. . . . 5
⊢
(-∞(,)+∞) = ℝ |
38 | 1, 36, 37 | 3eqtri 2770 |
. . . 4
⊢ ((-1(,)1)
∪ ((-∞(,]-1) ∪ (1[,)+∞))) = ℝ |
39 | 38 | difeq1i 4047 |
. . 3
⊢
(((-1(,)1) ∪ ((-∞(,]-1) ∪ (1[,)+∞))) ∖
((-∞(,]-1) ∪ (1[,)+∞))) = (ℝ ∖ ((-∞(,]-1)
∪ (1[,)+∞))) |
40 | | difun2 4409 |
. . 3
⊢
(((-1(,)1) ∪ ((-∞(,]-1) ∪ (1[,)+∞))) ∖
((-∞(,]-1) ∪ (1[,)+∞))) = ((-1(,)1) ∖ ((-∞(,]-1)
∪ (1[,)+∞))) |
41 | | ax-resscn 10810 |
. . . 4
⊢ ℝ
⊆ ℂ |
42 | | difin2 4220 |
. . . 4
⊢ (ℝ
⊆ ℂ → (ℝ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
= ((ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∩
ℝ)) |
43 | 41, 42 | ax-mp 5 |
. . 3
⊢ (ℝ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) = ((ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) ∩ ℝ) |
44 | 39, 40, 43 | 3eqtr3ri 2775 |
. 2
⊢ ((ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∩ ℝ) = ((-1(,)1)
∖ ((-∞(,]-1) ∪ (1[,)+∞))) |
45 | | dvasin.d |
. . 3
⊢ 𝐷 = (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) |
46 | 45 | ineq1i 4137 |
. 2
⊢ (𝐷 ∩ ℝ) = ((ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∩ ℝ) |
47 | | incom 4129 |
. . . . 5
⊢ ((-1(,)1)
∩ (-∞(,]-1)) = ((-∞(,]-1) ∩ (-1(,)1)) |
48 | 30, 16, 31 | ixxdisj 12974 |
. . . . . 6
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ 1 ∈ ℝ*) → ((-∞(,]-1)
∩ (-1(,)1)) = ∅) |
49 | 24, 3, 4, 48 | mp3an 1463 |
. . . . 5
⊢
((-∞(,]-1) ∩ (-1(,)1)) = ∅ |
50 | 47, 49 | eqtri 2766 |
. . . 4
⊢ ((-1(,)1)
∩ (-∞(,]-1)) = ∅ |
51 | 16, 17, 18 | ixxdisj 12974 |
. . . . 5
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ* ∧ +∞
∈ ℝ*) → ((-1(,)1) ∩ (1[,)+∞)) =
∅) |
52 | 3, 4, 5, 51 | mp3an 1463 |
. . . 4
⊢ ((-1(,)1)
∩ (1[,)+∞)) = ∅ |
53 | 50, 52 | pm3.2i 474 |
. . 3
⊢
(((-1(,)1) ∩ (-∞(,]-1)) = ∅ ∧ ((-1(,)1) ∩
(1[,)+∞)) = ∅) |
54 | | un00 4371 |
. . . 4
⊢
((((-1(,)1) ∩ (-∞(,]-1)) = ∅ ∧ ((-1(,)1) ∩
(1[,)+∞)) = ∅) ↔ (((-1(,)1) ∩ (-∞(,]-1)) ∪
((-1(,)1) ∩ (1[,)+∞))) = ∅) |
55 | | indi 4202 |
. . . . 5
⊢ ((-1(,)1)
∩ ((-∞(,]-1) ∪ (1[,)+∞))) = (((-1(,)1) ∩
(-∞(,]-1)) ∪ ((-1(,)1) ∩ (1[,)+∞))) |
56 | 55 | eqeq1i 2743 |
. . . 4
⊢
(((-1(,)1) ∩ ((-∞(,]-1) ∪ (1[,)+∞))) = ∅
↔ (((-1(,)1) ∩ (-∞(,]-1)) ∪ ((-1(,)1) ∩ (1[,)+∞)))
= ∅) |
57 | | disj3 4382 |
. . . 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 2776 |
1
⊢ (𝐷 ∩ ℝ) =
(-1(,)1) |