| Step |
Hyp |
Ref |
Expression |
| 1 |
|
redvabs.d |
⊢ 𝐷 = ( ℝ ∖ { 0 } ) |
| 2 |
|
partfun |
⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 1 , 1 ) ) = ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 1 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 1 ) ) |
| 3 |
|
reelprrecn |
⊢ ℝ ∈ { ℝ , ℂ } |
| 4 |
3
|
a1i |
⊢ ( ⊤ → ℝ ∈ { ℝ , ℂ } ) |
| 5 |
|
inss1 |
⊢ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ 𝐷 |
| 6 |
|
difss |
⊢ ( ℝ ∖ { 0 } ) ⊆ ℝ |
| 7 |
1 6
|
eqsstri |
⊢ 𝐷 ⊆ ℝ |
| 8 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
| 9 |
7 8
|
sstri |
⊢ 𝐷 ⊆ ℂ |
| 10 |
5 9
|
sstri |
⊢ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℂ |
| 11 |
10
|
sseli |
⊢ ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) → 𝑥 ∈ ℂ ) |
| 12 |
11
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) → 𝑥 ∈ ℂ ) |
| 13 |
|
1cnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) → 1 ∈ ℂ ) |
| 14 |
8
|
a1i |
⊢ ( ⊤ → ℝ ⊆ ℂ ) |
| 15 |
14
|
sselda |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ ) |
| 16 |
|
1red |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℝ ) |
| 17 |
4
|
dvmptid |
⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℝ ↦ 1 ) ) |
| 18 |
|
ssinss1 |
⊢ ( 𝐷 ⊆ ℝ → ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℝ ) |
| 19 |
7 18
|
mp1i |
⊢ ( ⊤ → ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℝ ) |
| 20 |
|
tgioo4 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
| 21 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
| 22 |
1
|
eleq2i |
⊢ ( 𝑥 ∈ 𝐷 ↔ 𝑥 ∈ ( ℝ ∖ { 0 } ) ) |
| 23 |
|
eldifsn |
⊢ ( 𝑥 ∈ ( ℝ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ) |
| 24 |
22 23
|
bitri |
⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ) |
| 25 |
|
vex |
⊢ 𝑥 ∈ V |
| 26 |
|
breq1 |
⊢ ( 𝑦 = 𝑥 → ( 𝑦 < 0 ↔ 𝑥 < 0 ) ) |
| 27 |
25 26
|
elab |
⊢ ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ↔ 𝑥 < 0 ) |
| 28 |
24 27
|
anbi12i |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) ) |
| 29 |
|
lt0ne0 |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 < 0 ) → 𝑥 ≠ 0 ) |
| 30 |
29
|
expcom |
⊢ ( 𝑥 < 0 → ( 𝑥 ∈ ℝ → 𝑥 ≠ 0 ) ) |
| 31 |
30
|
pm4.71d |
⊢ ( 𝑥 < 0 → ( 𝑥 ∈ ℝ ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ) ) |
| 32 |
31
|
bicomd |
⊢ ( 𝑥 < 0 → ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ↔ 𝑥 ∈ ℝ ) ) |
| 33 |
32
|
pm5.32ri |
⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ 𝑥 < 0 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 0 ) ) |
| 34 |
28 33
|
bitri |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 0 ) ) |
| 35 |
|
elin |
⊢ ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) ) |
| 36 |
|
0xr |
⊢ 0 ∈ ℝ* |
| 37 |
|
elioomnf |
⊢ ( 0 ∈ ℝ* → ( 𝑥 ∈ ( -∞ (,) 0 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 0 ) ) ) |
| 38 |
36 37
|
ax-mp |
⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < 0 ) ) |
| 39 |
34 35 38
|
3bitr4i |
⊢ ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↔ 𝑥 ∈ ( -∞ (,) 0 ) ) |
| 40 |
39
|
eqriv |
⊢ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) = ( -∞ (,) 0 ) |
| 41 |
|
iooretop |
⊢ ( -∞ (,) 0 ) ∈ ( topGen ‘ ran (,) ) |
| 42 |
40 41
|
eqeltri |
⊢ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) |
| 43 |
42
|
a1i |
⊢ ( ⊤ → ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) ) |
| 44 |
4 15 16 17 19 20 21 43
|
dvmptres |
⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 1 ) ) |
| 45 |
4 12 13 44
|
dvmptneg |
⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ) = ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 1 ) ) |
| 46 |
45
|
mptru |
⊢ ( ℝ D ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ) = ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 1 ) |
| 47 |
7
|
a1i |
⊢ ( ⊤ → 𝐷 ⊆ ℝ ) |
| 48 |
47
|
ssdifssd |
⊢ ( ⊤ → ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℝ ) |
| 49 |
27
|
notbii |
⊢ ( ¬ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ↔ ¬ 𝑥 < 0 ) |
| 50 |
24 49
|
anbi12i |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) ) |
| 51 |
|
anass |
⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≠ 0 ) ∧ ¬ 𝑥 < 0 ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝑥 ≠ 0 ∧ ¬ 𝑥 < 0 ) ) ) |
| 52 |
|
elre0re |
⊢ ( 𝑥 ∈ ℝ → 0 ∈ ℝ ) |
| 53 |
|
id |
⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ ) |
| 54 |
52 53
|
lttrid |
⊢ ( 𝑥 ∈ ℝ → ( 0 < 𝑥 ↔ ¬ ( 0 = 𝑥 ∨ 𝑥 < 0 ) ) ) |
| 55 |
|
ioran |
⊢ ( ¬ ( 0 = 𝑥 ∨ 𝑥 < 0 ) ↔ ( ¬ 0 = 𝑥 ∧ ¬ 𝑥 < 0 ) ) |
| 56 |
|
nesym |
⊢ ( 𝑥 ≠ 0 ↔ ¬ 0 = 𝑥 ) |
| 57 |
56
|
bicomi |
⊢ ( ¬ 0 = 𝑥 ↔ 𝑥 ≠ 0 ) |
| 58 |
55 57
|
bianbi |
⊢ ( ¬ ( 0 = 𝑥 ∨ 𝑥 < 0 ) ↔ ( 𝑥 ≠ 0 ∧ ¬ 𝑥 < 0 ) ) |
| 59 |
54 58
|
bitr2di |
⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 ≠ 0 ∧ ¬ 𝑥 < 0 ) ↔ 0 < 𝑥 ) ) |
| 60 |
59
|
pm5.32i |
⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 ≠ 0 ∧ ¬ 𝑥 < 0 ) ) ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) |
| 61 |
50 51 60
|
3bitri |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) |
| 62 |
|
eldif |
⊢ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↔ ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) ) |
| 63 |
|
repos |
⊢ ( 𝑥 ∈ ( 0 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) |
| 64 |
61 62 63
|
3bitr4i |
⊢ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↔ 𝑥 ∈ ( 0 (,) +∞ ) ) |
| 65 |
64
|
eqriv |
⊢ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) = ( 0 (,) +∞ ) |
| 66 |
|
iooretop |
⊢ ( 0 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) |
| 67 |
65 66
|
eqeltri |
⊢ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) |
| 68 |
67
|
a1i |
⊢ ( ⊤ → ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) ) |
| 69 |
4 15 16 17 48 20 21 68
|
dvmptres |
⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 1 ) ) |
| 70 |
69
|
mptru |
⊢ ( ℝ D ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 1 ) |
| 71 |
46 70
|
uneq12i |
⊢ ( ( ℝ D ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ) ∪ ( ℝ D ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) = ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 1 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 1 ) ) |
| 72 |
12
|
negcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) → - 𝑥 ∈ ℂ ) |
| 73 |
72
|
fmpttd |
⊢ ( ⊤ → ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) : ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ⟶ ℂ ) |
| 74 |
|
ssdifss |
⊢ ( 𝐷 ⊆ ℝ → ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℝ ) |
| 75 |
7 74
|
ax-mp |
⊢ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℝ |
| 76 |
75 8
|
sstri |
⊢ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℂ |
| 77 |
76
|
a1i |
⊢ ( ⊤ → ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ⊆ ℂ ) |
| 78 |
77
|
sselda |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) → 𝑥 ∈ ℂ ) |
| 79 |
78
|
fmpttd |
⊢ ( ⊤ → ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) : ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ⟶ ℂ ) |
| 80 |
|
inindif |
⊢ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∩ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) = ∅ |
| 81 |
80
|
a1i |
⊢ ( ⊤ → ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∩ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) = ∅ ) |
| 82 |
|
retop |
⊢ ( topGen ‘ ran (,) ) ∈ Top |
| 83 |
|
isopn3i |
⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) = ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) |
| 84 |
82 42 83
|
mp2an |
⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) = ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) |
| 85 |
|
isopn3i |
⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) = ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) |
| 86 |
82 67 85
|
mp2an |
⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) = ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) |
| 87 |
84 86
|
uneq12i |
⊢ ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) ∪ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) = ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) |
| 88 |
|
unopn |
⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) ∧ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ∈ ( topGen ‘ ran (,) ) ) → ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ∈ ( topGen ‘ ran (,) ) ) |
| 89 |
82 42 67 88
|
mp3an |
⊢ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ∈ ( topGen ‘ ran (,) ) |
| 90 |
|
isopn3i |
⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) = ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) |
| 91 |
82 89 90
|
mp2an |
⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) = ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) |
| 92 |
87 91
|
eqtr4i |
⊢ ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) ∪ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) = ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) |
| 93 |
92
|
a1i |
⊢ ( ⊤ → ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ) ∪ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) = ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ∪ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ) ) ) |
| 94 |
20 21 14 73 79 19 48 81 93
|
dvun |
⊢ ( ⊤ → ( ( ℝ D ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ) ∪ ( ℝ D ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) = ( ℝ D ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) ) |
| 95 |
94
|
mptru |
⊢ ( ( ℝ D ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ) ∪ ( ℝ D ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) = ( ℝ D ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) |
| 96 |
2 71 95
|
3eqtr2ri |
⊢ ( ℝ D ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 1 , 1 ) ) |
| 97 |
|
partfun |
⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 𝑥 , 𝑥 ) ) = ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) |
| 98 |
|
elioore |
⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) → 𝑥 ∈ ℝ ) |
| 99 |
|
0red |
⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) → 0 ∈ ℝ ) |
| 100 |
38
|
simprbi |
⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) → 𝑥 < 0 ) |
| 101 |
98 99 100
|
ltled |
⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) → 𝑥 ≤ 0 ) |
| 102 |
98 101
|
absnidd |
⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) → ( abs ‘ 𝑥 ) = - 𝑥 ) |
| 103 |
102
|
eqcomd |
⊢ ( 𝑥 ∈ ( -∞ (,) 0 ) → - 𝑥 = ( abs ‘ 𝑥 ) ) |
| 104 |
103 40
|
eleq2s |
⊢ ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) → - 𝑥 = ( abs ‘ 𝑥 ) ) |
| 105 |
35 104
|
sylbir |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) → - 𝑥 = ( abs ‘ 𝑥 ) ) |
| 106 |
|
rpabsid |
⊢ ( 𝑥 ∈ ℝ+ → ( abs ‘ 𝑥 ) = 𝑥 ) |
| 107 |
106
|
eqcomd |
⊢ ( 𝑥 ∈ ℝ+ → 𝑥 = ( abs ‘ 𝑥 ) ) |
| 108 |
|
ioorp |
⊢ ( 0 (,) +∞ ) = ℝ+ |
| 109 |
107 108
|
eleq2s |
⊢ ( 𝑥 ∈ ( 0 (,) +∞ ) → 𝑥 = ( abs ‘ 𝑥 ) ) |
| 110 |
109 65
|
eleq2s |
⊢ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) → 𝑥 = ( abs ‘ 𝑥 ) ) |
| 111 |
62 110
|
sylbir |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } ) → 𝑥 = ( abs ‘ 𝑥 ) ) |
| 112 |
105 111
|
ifeqda |
⊢ ( 𝑥 ∈ 𝐷 → if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 𝑥 , 𝑥 ) = ( abs ‘ 𝑥 ) ) |
| 113 |
112
|
mpteq2ia |
⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 𝑥 , 𝑥 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) ) |
| 114 |
97 113
|
eqtr3i |
⊢ ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) ) |
| 115 |
114
|
oveq2i |
⊢ ( ℝ D ( ( 𝑥 ∈ ( 𝐷 ∩ { 𝑦 ∣ 𝑦 < 0 } ) ↦ - 𝑥 ) ∪ ( 𝑥 ∈ ( 𝐷 ∖ { 𝑦 ∣ 𝑦 < 0 } ) ↦ 𝑥 ) ) ) = ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) ) ) |
| 116 |
|
eqid |
⊢ 1 = 1 |
| 117 |
27 116
|
ifbieq2i |
⊢ if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 1 , 1 ) = if ( 𝑥 < 0 , - 1 , 1 ) |
| 118 |
117
|
mpteq2i |
⊢ ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 ∈ { 𝑦 ∣ 𝑦 < 0 } , - 1 , 1 ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 < 0 , - 1 , 1 ) ) |
| 119 |
96 115 118
|
3eqtr3i |
⊢ ( ℝ D ( 𝑥 ∈ 𝐷 ↦ ( abs ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ if ( 𝑥 < 0 , - 1 , 1 ) ) |