Metamath Proof Explorer

Theorem redvmptabs

Description: The derivative of the absolute value, for real numbers. (Contributed by SN, 30-Sep-2025)

Ref Expression
Hypothesis redvabs.d 
|- D = ( RR \ { 0 } )
Assertion redvmptabs 
|- ( RR _D ( x e. D |-> ( abs ` x ) ) ) = ( x e. D |-> if ( x < 0 , -u 1 , 1 ) )

Proof

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