| Step | Hyp | Ref
| Expression |
| 1 | | un12 4173 |
. . . . 5
⊢ ((-1(,)1)
∪ ((-∞(,]-1) ∪ (1[,)+∞))) = ((-∞(,]-1) ∪
((-1(,)1) ∪ (1[,)+∞))) |
| 2 | | neg1rr 12381 |
. . . . . . . . . 10
⊢ -1 ∈
ℝ |
| 3 | 2 | rexri 11319 |
. . . . . . . . 9
⊢ -1 ∈
ℝ* |
| 4 | | 1xr 11320 |
. . . . . . . . 9
⊢ 1 ∈
ℝ* |
| 5 | | pnfxr 11315 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
| 6 | 3, 4, 5 | 3pm3.2i 1340 |
. . . . . . . 8
⊢ (-1
∈ ℝ* ∧ 1 ∈ ℝ* ∧ +∞
∈ ℝ*) |
| 7 | | neg1lt0 12383 |
. . . . . . . . . 10
⊢ -1 <
0 |
| 8 | | 0lt1 11785 |
. . . . . . . . . 10
⊢ 0 <
1 |
| 9 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 10 | | 1re 11261 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
| 11 | 2, 9, 10 | lttri 11387 |
. . . . . . . . . 10
⊢ ((-1 <
0 ∧ 0 < 1) → -1 < 1) |
| 12 | 7, 8, 11 | mp2an 692 |
. . . . . . . . 9
⊢ -1 <
1 |
| 13 | | ltpnf 13162 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ → 1 < +∞) |
| 14 | 10, 13 | ax-mp 5 |
. . . . . . . . 9
⊢ 1 <
+∞ |
| 15 | 12, 14 | pm3.2i 470 |
. . . . . . . 8
⊢ (-1 <
1 ∧ 1 < +∞) |
| 16 | | df-ioo 13391 |
. . . . . . . . 9
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
| 17 | | df-ico 13393 |
. . . . . . . . 9
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| 18 | | xrlenlt 11326 |
. . . . . . . . 9
⊢ ((1
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (1 ≤
𝑤 ↔ ¬ 𝑤 < 1)) |
| 19 | | xrlttr 13182 |
. . . . . . . . 9
⊢ ((𝑤 ∈ ℝ*
∧ 1 ∈ ℝ* ∧ +∞ ∈ ℝ*)
→ ((𝑤 < 1 ∧ 1
< +∞) → 𝑤
< +∞)) |
| 20 | | xrltletr 13199 |
. . . . . . . . 9
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
→ ((-1 < 1 ∧ 1 ≤ 𝑤) → -1 < 𝑤)) |
| 21 | 16, 17, 18, 16, 19, 20 | ixxun 13403 |
. . . . . . . 8
⊢ (((-1
∈ ℝ* ∧ 1 ∈ ℝ* ∧ +∞
∈ ℝ*) ∧ (-1 < 1 ∧ 1 < +∞)) →
((-1(,)1) ∪ (1[,)+∞)) = (-1(,)+∞)) |
| 22 | 6, 15, 21 | mp2an 692 |
. . . . . . 7
⊢ ((-1(,)1)
∪ (1[,)+∞)) = (-1(,)+∞) |
| 23 | 22 | uneq2i 4165 |
. . . . . 6
⊢
((-∞(,]-1) ∪ ((-1(,)1) ∪ (1[,)+∞))) =
((-∞(,]-1) ∪ (-1(,)+∞)) |
| 24 | | mnfxr 11318 |
. . . . . . . 8
⊢ -∞
∈ ℝ* |
| 25 | 24, 3, 5 | 3pm3.2i 1340 |
. . . . . . 7
⊢ (-∞
∈ ℝ* ∧ -1 ∈ ℝ* ∧ +∞
∈ ℝ*) |
| 26 | | mnflt 13165 |
. . . . . . . . 9
⊢ (-1
∈ ℝ → -∞ < -1) |
| 27 | | ltpnf 13162 |
. . . . . . . . 9
⊢ (-1
∈ ℝ → -1 < +∞) |
| 28 | 26, 27 | jca 511 |
. . . . . . . 8
⊢ (-1
∈ ℝ → (-∞ < -1 ∧ -1 <
+∞)) |
| 29 | 2, 28 | ax-mp 5 |
. . . . . . 7
⊢ (-∞
< -1 ∧ -1 < +∞) |
| 30 | | df-ioc 13392 |
. . . . . . . 8
⊢ (,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
| 31 | | xrltnle 11328 |
. . . . . . . 8
⊢ ((-1
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (-1 <
𝑤 ↔ ¬ 𝑤 ≤ -1)) |
| 32 | | xrlelttr 13198 |
. . . . . . . 8
⊢ ((𝑤 ∈ ℝ*
∧ -1 ∈ ℝ* ∧ +∞ ∈ ℝ*)
→ ((𝑤 ≤ -1 ∧ -1
< +∞) → 𝑤
< +∞)) |
| 33 | | xrlttr 13182 |
. . . . . . . 8
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ 𝑤
∈ ℝ*) → ((-∞ < -1 ∧ -1 < 𝑤) → -∞ < 𝑤)) |
| 34 | 30, 16, 31, 16, 32, 33 | ixxun 13403 |
. . . . . . 7
⊢
(((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞
< -1 ∧ -1 < +∞)) → ((-∞(,]-1) ∪ (-1(,)+∞))
= (-∞(,)+∞)) |
| 35 | 25, 29, 34 | mp2an 692 |
. . . . . 6
⊢
((-∞(,]-1) ∪ (-1(,)+∞)) =
(-∞(,)+∞) |
| 36 | 23, 35 | eqtri 2765 |
. . . . 5
⊢
((-∞(,]-1) ∪ ((-1(,)1) ∪ (1[,)+∞))) =
(-∞(,)+∞) |
| 37 | | ioomax 13462 |
. . . . 5
⊢
(-∞(,)+∞) = ℝ |
| 38 | 1, 36, 37 | 3eqtri 2769 |
. . . 4
⊢ ((-1(,)1)
∪ ((-∞(,]-1) ∪ (1[,)+∞))) = ℝ |
| 39 | 38 | difeq1i 4122 |
. . 3
⊢
(((-1(,)1) ∪ ((-∞(,]-1) ∪ (1[,)+∞))) ∖
((-∞(,]-1) ∪ (1[,)+∞))) = (ℝ ∖ ((-∞(,]-1)
∪ (1[,)+∞))) |
| 40 | | difun2 4481 |
. . 3
⊢
(((-1(,)1) ∪ ((-∞(,]-1) ∪ (1[,)+∞))) ∖
((-∞(,]-1) ∪ (1[,)+∞))) = ((-1(,)1) ∖ ((-∞(,]-1)
∪ (1[,)+∞))) |
| 41 | | ax-resscn 11212 |
. . . 4
⊢ ℝ
⊆ ℂ |
| 42 | | difin2 4301 |
. . . 4
⊢ (ℝ
⊆ ℂ → (ℝ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
= ((ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∩
ℝ)) |
| 43 | 41, 42 | ax-mp 5 |
. . 3
⊢ (ℝ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) = ((ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) ∩ ℝ) |
| 44 | 39, 40, 43 | 3eqtr3ri 2774 |
. 2
⊢ ((ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∩ ℝ) = ((-1(,)1)
∖ ((-∞(,]-1) ∪ (1[,)+∞))) |
| 45 | | dvasin.d |
. . 3
⊢ 𝐷 = (ℂ ∖
((-∞(,]-1) ∪ (1[,)+∞))) |
| 46 | 45 | ineq1i 4216 |
. 2
⊢ (𝐷 ∩ ℝ) = ((ℂ
∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∩ ℝ) |
| 47 | | incom 4209 |
. . . . 5
⊢ ((-1(,)1)
∩ (-∞(,]-1)) = ((-∞(,]-1) ∩ (-1(,)1)) |
| 48 | 30, 16, 31 | ixxdisj 13402 |
. . . . . 6
⊢
((-∞ ∈ ℝ* ∧ -1 ∈
ℝ* ∧ 1 ∈ ℝ*) → ((-∞(,]-1)
∩ (-1(,)1)) = ∅) |
| 49 | 24, 3, 4, 48 | mp3an 1463 |
. . . . 5
⊢
((-∞(,]-1) ∩ (-1(,)1)) = ∅ |
| 50 | 47, 49 | eqtri 2765 |
. . . 4
⊢ ((-1(,)1)
∩ (-∞(,]-1)) = ∅ |
| 51 | 16, 17, 18 | ixxdisj 13402 |
. . . . 5
⊢ ((-1
∈ ℝ* ∧ 1 ∈ ℝ* ∧ +∞
∈ ℝ*) → ((-1(,)1) ∩ (1[,)+∞)) =
∅) |
| 52 | 3, 4, 5, 51 | mp3an 1463 |
. . . 4
⊢ ((-1(,)1)
∩ (1[,)+∞)) = ∅ |
| 53 | 50, 52 | pm3.2i 470 |
. . 3
⊢
(((-1(,)1) ∩ (-∞(,]-1)) = ∅ ∧ ((-1(,)1) ∩
(1[,)+∞)) = ∅) |
| 54 | | un00 4445 |
. . . 4
⊢
((((-1(,)1) ∩ (-∞(,]-1)) = ∅ ∧ ((-1(,)1) ∩
(1[,)+∞)) = ∅) ↔ (((-1(,)1) ∩ (-∞(,]-1)) ∪
((-1(,)1) ∩ (1[,)+∞))) = ∅) |
| 55 | | indi 4284 |
. . . . 5
⊢ ((-1(,)1)
∩ ((-∞(,]-1) ∪ (1[,)+∞))) = (((-1(,)1) ∩
(-∞(,]-1)) ∪ ((-1(,)1) ∩ (1[,)+∞))) |
| 56 | 55 | eqeq1i 2742 |
. . . 4
⊢
(((-1(,)1) ∩ ((-∞(,]-1) ∪ (1[,)+∞))) = ∅
↔ (((-1(,)1) ∩ (-∞(,]-1)) ∪ ((-1(,)1) ∩ (1[,)+∞)))
= ∅) |
| 57 | | disj3 4454 |
. . . 4
⊢
(((-1(,)1) ∩ ((-∞(,]-1) ∪ (1[,)+∞))) = ∅
↔ (-1(,)1) = ((-1(,)1) ∖ ((-∞(,]-1) ∪
(1[,)+∞)))) |
| 58 | 54, 56, 57 | 3bitr2i 299 |
. . 3
⊢
((((-1(,)1) ∩ (-∞(,]-1)) = ∅ ∧ ((-1(,)1) ∩
(1[,)+∞)) = ∅) ↔ (-1(,)1) = ((-1(,)1) ∖ ((-∞(,]-1)
∪ (1[,)+∞)))) |
| 59 | 53, 58 | mpbi 230 |
. 2
⊢ (-1(,)1)
= ((-1(,)1) ∖ ((-∞(,]-1) ∪ (1[,)+∞))) |
| 60 | 44, 46, 59 | 3eqtr4i 2775 |
1
⊢ (𝐷 ∩ ℝ) =
(-1(,)1) |