(real) antiderivative of 1/x (#5034)

Author: icecream17

changes-set.txt

@@ -92,6 +92,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+ 1-Oct-25 inindif   [same]      Moved from TA's mathbox to main set.mm
 23-Sep-25 coecj     [same]      Removed unneeded hypothesis
 23-Sep-25 plycj     [same]      Removed unneeded hypothesis
 23-Sep-25 elfzolem1 [same]      moved from GS's mathbox to main set.mm

set.mm

@@ -41524,6 +41524,14 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets,
       UGUH $.
   $}
 
+  $( The intersection and class difference of a class with another class are
+     disjoint.  With ~ inundif , this shows that such intersection and class
+     difference partition the class ` A ` .  (Contributed by Thierry Arnoux,
+     13-Sep-2017.) $)
+  inindif $p |- ( ( A i^i C ) i^i ( A \ C ) ) = (/) $=
+    ( cin wss cdif c0 wceq inss2 ssinss1 ax-mp inssdif0 mpbi ) ABCZACBDZMABECFG
+    MBDNABHMABIJMABKL $.
+
   ${
     $d A x $.
     $( The difference between a class and itself is the empty set.  Proposition
@@ -502773,11 +502781,6 @@ Class abstractions (a.k.a. class builders)
   inin $p |- ( A i^i ( A i^i B ) ) = ( A i^i B ) $=
     ( cin in13 inidm ineq2i incom 3eqtri ) AABCZCBAACZCBACIAABDJABAEFBAGH $.
 
-  $( See ~ inundif .  (Contributed by Thierry Arnoux, 13-Sep-2017.) $)
-  inindif $p |- ( ( A i^i C ) i^i ( A \ C ) ) = (/) $=
-    ( cin wss cdif c0 wceq wo inss2 orci inss ax-mp inssdif0 mpbi ) ABCZACBDZOA
-    BECFGOBDZABDZHPQRABIJOABKLOABMN $.
-
   $( Condition for the intersections of two sets with a given set to be equal.
      (Contributed by Thierry Arnoux, 28-Dec-2021.) $)
   difininv $p |- ( ( ( ( A \ C ) i^i B ) = (/) /\ ( ( C \ A ) i^i B ) = (/) )
@@ -697256,6 +697259,11 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
     ( c9 c2 cexp co cmul c8 c1 cdc 9cn sqvali 9t9e81 eqtri ) ABCDAAEDFGHAIJKL
     $.
 
+  $( The positive reals are a subset of the complex numbers.  (Contributed by
+     SN, 1-Oct-2025.) $)
+  rpsscn $p |- RR+ C_ CC $=
+    ( crp cr cc rpssre ax-resscn sstri ) ABCDEF $.
+
   $( 4 is a positive real.  (Contributed by SN, 26-Aug-2025.) $)
   4rp $p |- 4 e. RR+ $=
     ( c4 4re 4pos elrpii ) ABCD $.
@@ -697484,6 +697492,26 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
     ( cr wcel ci cmul co cc0 wceq recn ax-icn a1i mulcomd eleq1d itrere bitrd
     cc ) ABCZADEFZBCDAEFZBCAGHQRSBQADAIDPCQJKLMANO $.
 
+  ${
+    $d A w x y z $.  $d B w x y z $.  $d C w x y z $.
+    ixxdisjd.a $e |- ( ph -> A e. RR* ) $.
+    ixxdisjd.b $e |- ( ph -> B e. RR* ) $.
+    ixxdisjd.c $e |- ( ph -> C e. RR* ) $.
+    $( Adjacent intervals where the lower interval is right-closed and the
+       upper interval is open are disjoint.  (Contributed by SN,
+       1-Oct-2025.) $)
+    iocioodisjd $p |- ( ph -> ( ( A (,] B ) i^i ( B (,) C ) ) = (/) ) $=
+      ( vx vy vz vw cxr wcel cioc co cioo cin c0 wceq clt df-ioc df-ioo xrltnle
+      cle cv ixxdisj syl3anc ) ABLMCLMDLMBCNOCDPOQRSEFGHIJKBCDPTUDTTNHIJUAHIJUB
+      CKUEUCUFUG $.
+  $}
+
+  $( A positive real is its own absolute value.  (Contributed by SN,
+     1-Oct-2025.) $)
+  rpabsid $p |- ( R e. RR+ -> ( abs ` R ) = R ) $=
+    ( crp wcel cr cc0 cle wbr cabs cfv wceq rpre rpge0 absid syl2anc ) ABCADCEA
+    FGAHIAJAKALAMN $.
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -697895,7 +697923,7 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-  Trigonometry
+  Trigonometry and Calculus
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
 $)
 
@@ -697946,6 +697974,152 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
     VLVQVLULJVPVLIVRVLUMUNVLVQJZVLNJZKVLORZVLAORZVLVRPABLMQSUOWBAACDZBORWCGBOAU
     PALQUQURUSUTABALMLSQVAVCKNJANJVSVTWAWBVDVEVFALPKAVLVGTVHVIVLVJTVK $.
 
+  ${
+    dvun.j $e |- J = ( K |`t S ) $.
+    dvun.k $e |- K = ( TopOpen ` CCfld ) $.
+    dvun.s $e |- ( ph -> S C_ CC ) $.
+    dvun.f $e |- ( ph -> F : A --> CC ) $.
+    dvun.g $e |- ( ph -> G : B --> CC ) $.
+    dvun.a $e |- ( ph -> A C_ S ) $.
+    dvun.b $e |- ( ph -> B C_ S ) $.
+    dvun.d $e |- ( ph -> ( A i^i B ) = (/) ) $.
+    dvun.n $e |- ( ph -> ( ( ( int ` J ) ` A ) u. ( ( int ` J ) ` B ) )
+                         = ( ( int ` J ) ` ( A u. B ) ) ) $.
+    $( Condition for the union of the derivatives of two disjoint functions to
+       be equal to the derivative of the union of the two functions.  If ` A `
+       and ` B ` are open sets, this condition (dvun.n) is satisfied by
+       ~ isopn3i .  (Contributed by SN, 30-Sep-2025.) $)
+    dvun $p |- ( ph -> ( ( S _D F ) u. ( S _D G ) ) = ( S _D ( F u. G ) ) ) $=
+      ( cdv cres wceq cun co cnt cfv resundi reseq2d eqtr3id cc wss fun2d unssd
+      wf dvres syl22anc wfn cin c0 ffnd fnunres1 syl3anc oveq2d eqtr3d fnunres2
+      uneq12d fnresdm syl 3eqtr3d ) ADEFUAZRUBZBGUCUDZUDZSZVICVJUDZSZUAZVIBCUAZ
+      VJUDZSZDERUBZDFRUBZUAVIAVOVIVKVMUAZSVRVIVKVMUEAWAVQVIQUFUGAVLVSVNVTADVHBS
+      ZRUBZVLVSADUHUIZVPUHVHULZVPDUIZBDUIWCVLTKABCUHEFLMPUJZABCDNOUKZNVPBDGVHHJ
+      IUMUNAWBEDRAEBUOZFCUOZBCUPUQTZWBETABUHELURZACUHFMURZPBCEFUSUTVAVBADVHCSZR
+      UBZVNVTAWDWEWFCDUIWOVNTKWGWHOVPCDGVHHJIUMUNAWNFDRAWIWJWKWNFTWLWMPBCEFVCUT
+      VAVBVDADVHVPSZRUBZVRVIAWDWEWFWFWQVRTKWGWHWHVPVPDGVHHJIUMUNAWPVHDRAVHVPUOW
+      PVHTAVPUHVHWGURVPVHVEVFVAVBVG $.
+  $}
+
+  $( A good example of ~ dvmptco is ~ dvsinexp . $)
+
+  ${
+    $d x y $.  $d D x $.
+    redvabs.d $e |- D = ( RR \ { 0 } ) $.
+    $( The derivative of the absolute value, for real numbers.  (Contributed by
+       SN, 30-Sep-2025.) $)
+    redvmptabs $p |- ( RR _D ( x e. D |-> ( abs ` x ) ) ) =
+                             ( x e. D |-> if ( x < 0 , -u 1 , 1 ) ) $=
+      ( cr cc0 clt cmpt cun cdv co wcel c1 cfv wceq wtru cc a1i wa wss wn vy cv
+      wbr cab cin cneg cdif cif cabs partfun cpr reelprrecn inss1 difss eqsstri
+      csn ax-resscn sstri sseli adantl 1cnd crn ctg ccnfld ctopn sselda dvmptid
+      cioo 1red ssinss1 mp1i eqid tgioo2 cmnf wne eleq2i eldifsn bitri vex elab
+      breq1 anbi12i lt0ne0 expcom pm4.71d bicomd pm5.32ri elin cxr 0xr elioomnf
+      wb ax-mp 3bitr4i eqriv iooretop eqeltri dvmptres dvmptneg ssdifssd notbii
+      mptru cpnf anass wo elre0re id lttrid ioran bicomi bianbi bitr2di pm5.32i
+      nesym 3bitri eldif repos uneq12i negcld fmpttd ssdifss inindif ctop retop
+      c0 cnt isopn3i mp2an unopn mp3an eqtr4i dvun 3eqtr2ri elioore 0red eqcomd
+      simprbi eleq2s sylbir crp absnidd rpabsid ifeqda mpteq2ia eqtr3i ifbieq2i
+      ltled ioorp oveq2i mpteq2i 3eqtr3i ) DABUAUBZEFUCZUAUDZUEZAUBZUFZGZABUUNU
+      GZUUPGZHZIJZABUUPUUNKZLUFZLUHZGZDABUUPUIMZGZIJABUUPEFUCZUVDLUHZGUVFAUUOUV
+      DGZAUUSLGZHDUURIJZDUUTIJZHZUVBABUUNUVDLUJUVMUVKUVNUVLUVMUVKNOAUUPLDPUUODD
+      PUKKOULQZUUPUUOKZUUPPKOUUOPUUPUUOBPBUUNUMBDPBDEUPZUGZDCDUVRUNUOZUQURURUSU
+      TZOUVQRZVAOAUUPLDVHVBVCMZVDVEMZDDUUOUVPODPUUPDPSOUQQZVFZOUUPDKZRVIZOADUVP
+      VGZBDSZUUODSOUVTBUUNDVJVKZUWDUWDVLZVMZUWLUUOUWCKZOUUOVNEVHJZUWCAUUOUWOUUP
+      BKZUVCRZUWGUVIRZUVQUUPUWOKZUWQUWGUUPEVOZRZUVIRUWRUWPUXAUVCUVIUWPUUPUVSKUX
+      ABUVSUUPCVPUUPDEVQVRZUUMUVIUAUUPAVSUULUUPEFWAVTZWBUVIUXAUWGUVIUWGUXAUVIUW
+      GUWTUWGUVIUWTUUPWCWDWEWFWGVRUUPBUUNWHZEWIKUWSUWRWLWJEUUPWKWMZWNWOZVNEWPWQ
+      ZQWRWSXBUVNUVLNOAUUPLDUWCUWDDDUUSUVPUWFUWHUWIOBDUUNUWJOUVTQWTZUWMUWLUUSUW
+      CKZOUUSEXCVHJZUWCAUUSUXJUWPUVCTZRZUWGEUUPFUCZRZUUPUUSKZUUPUXJKUXLUXAUVITZ
+      RUWGUWTUXPRZRUXNUWPUXAUXKUXPUXBUVCUVIUXCXAWBUWGUWTUXPXDUWGUXQUXMUWGUXMEUU
+      PNZUVIXETZUXQUWGEUUPUUPXFUWGXGXHUXSUXRTZUXPUWTUXRUVIXIUWTUXTUUPEXNXJXKXLX
+      MXOUUPBUUNXPZUUPXQWNWOZEXCWPWQZQWRXBXRUVOUVBNOUUOUUSDUURUUTUWCUWDUWMUWLUW
+      EOAUUOUUQPUWBUUPUWAXSXTOAUUSUUPPOUUSPUUPUUSPSOUUSDPUWJUUSDSUVTBDUUNYAWMUQ
+      URQVFXTUWKUXHUUOUUSUEYENOBUUNYBQUUOUWCYFMZMZUUSUYDMZHZUUOUUSHZUYDMZNOUYGU
+      YHUYIUYEUUOUYFUUSUWCYCKZUWNUYEUUONYDUXGUUOUWCYGYHUYJUXIUYFUUSNYDUYCUUSUWC
+      YGYHXRUYJUYHUWCKZUYIUYHNYDUYJUWNUXIUYKYDUXGUYCUUOUUSUWCYIYJUYHUWCYGYHYKQY
+      LXBYMUVAUVHDIABUVCUUQUUPUHZGUVAUVHABUUNUUQUUPUJABUYLUVGUWPUVCUUQUUPUVGUWQ
+      UVQUUQUVGNZUXDUYMUUPUWOUUOUWSUVGUUQUWSUUPUUPVNEYNZUWSUUPEUYNUWSYOUWSUWGUV
+      IUXEYQUUGUUAYPUXFYRYSUXLUXOUUPUVGNZUYAUYOUUPUXJUUSUYOUUPYTUXJUUPYTKUVGUUP
+      UUPUUBYPUUHYRUYBYRYSUUCUUDUUEUUIABUVEUVJUVCUVILLUVDUXCLVLUUFUUJUUK $.
+
+    $( The antiderivative of 1/x in real numbers, without using the absolute
+       value function.  (Contributed by SN, 1-Oct-2025.) $)
+    readvrec2 $p |- ( RR _D ( x e. D |-> ( ( log ` ( x ^ 2 ) ) / 2 ) ) ) =
+                            ( x e. D |-> ( 1 / x ) ) $=
+      ( vy cr c2 co clog cdiv cmpt cdv c1 cmul wceq wtru cc wcel a1i cc0 crp cv
+      cexp cfv cvv cpr reelprrecn wne csn wa eleq2i eldifsn bitri simplbi recnd
+      cdif sqcld simprbi wb sqne0 syl mpbird logcld adantl cmnf cioc cnelprrecn
+      ovexd cin c0 cpnf cioo incom dfrp2 ineq2i cxr mnfxr 0xr pnfxr iocioodisjd
+      mptru 3eqtri disjdif2 ax-mp wss rpsscn ssdif sqn0rp syl2an2 sselid eldifi
+      eqsstrri wn eldifn clt wbr mnflt0 0le0 elioc1 mp2an mpbir3an eleq1 mpbiri
+      cle w3a necon3bi cmin crn ctg ccnfld ctopn recn eqid cnopn ax-resscn mpbi
+      dfss2 sqcl 2nn dvexp mp1i dvmptres3 ssriv tgioo2 ccld cha rehaus uniretop
+      cn sncld cldopn eqeltri dvmptres 2m1e1 oveq2i oveq2d mpteq2ia 2cnd oveq1d
+      0re 2ne0 exp1d eqtrid eqtrdi cres wf1o logf1o snssi sscon feqresmpt dvlog
+      f1of eqtr3di fveq2 oveq2 dvmptco dvmptdivc resqcld rereccld mul12d mulcld
+      wf divcan3d sqvald recdiv2d reccld divcan1d 3eqtr2d 3eqtrd eqtri ) EABAUA
+      ZFUBGZHUCZFIGJKGZABLUVKIGZFUVJMGZMGZFIGZJZABLUVJIGZJUVMUVRNOAUVLUVPFEUDBE
+      EPUEZQOUFRZUVJBQZUVLPQOUWBUVKUWBUVJUWBUVJUWBUVJEQZUVJSUGZUWBUVJESUHZUOZQU
+      WCUWDUIBUWFUVJCUJUVJESUKULZUMZUNZUPUWBUVKSUGZUWDUWBUWCUWDUWGUQZUWBUVJPQZU
+      WJUWDURUWIUVJUSUTVAZVBVCOUWBUIZUVNUVOMVGOADUVKUVODUAZHUCZLUWOIGZEPUVLUVNU
+      DUDBPVDSVEGZUOZUWAPUVTQOVFRUWNTUWSUVKTTUWRUOZUWSTUWRVHZVINUWTTNUXAUWRTVHU
+      WRSVJVKGZVHZVITUWRVLTUXBUWRVMVNUXCVINOVDSVJVDVOQZOVPRSVOQZOVQRVJVOQOVRRVS
+      VTWATUWRWBWCTPWDUWTUWSWDWETPUWRWFWCWKUWBUWCOUWDUVKTQUWHUWBUWDOUWKVCUVJWGW
+      HWIUWNFUVJMVGUWOUWSQZUWPPQOUXFUWOUWOPUWRWJUXFUWOUWRQZWLUWOSUGUWOPUWRWMUXG
+      UWOSUWOSNUXGSUWRQZUXHUXEVDSWNWOZSSXCWOZVQWPWQUXDUXEUXHUXEUXIUXJXDURVPVQVD
+      SSWRWSWTZUWOSUWRXAXBXEUTVBVCOUXFUILUWOIVGOEABUVKJKGABFUVJFLXFGZUBGZMGZJAB
+      UVOJOAUVKUXNEVKXGXHUCZXIXJUCZUDEBUWAOUWCUIZUVJUWCUWLOUVJXKVCUPUXQFUXMMVGO
+      AUVKUXNEUXPUDPEUXPXLZUWAPUXPQOXMREPVHENZOEPWDUXSXNEPXPXORUWLUVKPQOUVJXQVC
+      OUWLUIFUXMMVGFYHQPAPUVKJKGAPUXNJNOXRAFXSXTYABEWDOABEUWHYBRUXPUXRYCUXRBUXO
+      QOBUWFUXOCUWEUXOYDUCQZUWFUXOQUXOYEQSEQUXTYFYSSUXOEYGYIWSUWEUXOEYGYJWCYKRY
+      LABUXNUVOUWBUXMUVJFMUWBUXMUVJLUBGUVJUXLLUVJUBYMYNUWBUVJUWIUUAUUBYOYPUUCOP
+      HUWSUUDZKGPDUWSUWPJZKGDUWSUWQJOUYAUYBPKODPUWEUOZHXGZUWSHUYCUYDHUUEUYCUYDH
+      UVAOUUFUYCUYDHUUKXTUWEUWRWDZUWSUYCWDOUXHUYEUXKSUWRUUGWCUWEUWRPUUHXTUUIYOD
+      UWSUWSXLUUJUULUWOUVKHUUMUWOUVKLIUUNUUOOYQFSUGZOYTRUUPVTABUVQUVSUWBUVQFUVN
+      UVJMGZMGZFIGUYGUVSUWBUVPUYHFIUWBUVNFUVJUWBUVNUWBUVKUWBUVJUWHUUQUWMUURUNZU
+      WBYQZUWIUUSYRUWBUYGFUWBUVNUVJUYIUWIUUTUYJUYFUWBYTRUVBUWBUYGLUVJUVJMGZIGZU
+      VJMGUVSUVJIGZUVJMGUVSUWBUVNUYLUVJMUWBUVKUYKLIUWBUVJUWIUVCYOYRUWBUYMUYLUVJ
+      MUWBUVJUVJUWIUWIUWKUWKUVDYRUWBUVSUVJUWBUVJUWIUWKUVEUWIUWKUVFUVGUVHYPUVI
+      $.
+
+    $( For real numbers, the antiderivative of 1/x is ln|x|.  (Contributed by
+       SN, 30-Sep-2025.) $)
+    readvrec $p |- ( RR _D ( x e. D |-> ( log ` ( abs ` x ) ) ) ) =
+                            ( x e. D |-> ( 1 / x ) ) $=
+      ( vy cr clog cmpt cdv co c1 cdiv cc0 cmul wceq wtru cc cmnf wcel a1i wa
+      cv cabs cfv clt wbr cneg cif cvv cioc cdif cpr reelprrecn cnelprrecn cpnf
+      crp cioo dfrp2 cin c0 cxr mnfxr pnfxr iocioodisjd mptru ineqcomi disjdif2
+      0xr ax-mp eqtr4i wss ioosscn ssdif eqsstri wne csn eleq2i eldifsn simplbi
+      bitri recnd adantl simprbi absrpcld sselid negex 1ex eldifi eldifn mnflt0
+      ifex wn ubioc1 mp3an eleq1 mpbiri necon3bi syl logcld redvmptabs cres crn
+      ovexd wf1o logf1o f1of feqmptd reseq1i c0ex snss mpbi sscon resmpt eqtr2i
+      wf mp2b oveq2i dvlog eqtri fveq2 oveq2 dvmptco ovif2 simpll abscld simplr
+      eqid absne0d reccld neg1cn mulcomd mulm1d 1cnd divneg2d 0red simpr oveq2d
+      ltled eqtrd sylanb ad2antrr absnidd eqcomd negcon1ad 3eqtrd recn rereccld
+      mulridd cle simpl lenltd biimpar absidd ifeqda eqtrid mpteq2ia ) EABAUAZU
+      BUCZFUCZGHIZABJUUQKIZUUPLUDUEZJUFZJUGZMIZGZABJUUPKIZGUUSUVENOADUUQUVCDUAZ
+      FUCZJUVGKIZEPUURUUTUHUHBPQLUIIZUJZEEPUKZROULSPUVLROUMSOUUPBRZTZUOUVKUUQUO
+      LUNUPIZUVJUJZUVKUOUVOUVPUQUVOUVJURUSNUVPUVONUVJUVOUSUVJUVOURUSNOQLUNQUTRZ
+      OVASLUTRZOVGSUNUTROVBSVCVDVEUVOUVJVFVHVIUVOPVJUVPUVKVJLUNVKUVOPUVJVLVHVMU
+      VNUUPUVMUUPPRZOUVMUUPUVMUUPERZUUPLVNZUVMUUPELVOZUJZRUVTUWATZBUWCUUPCVPUUP
+      ELVQVSZVRVTWAUVMUWAOUVMUVTUWAUWEWBWAWCWDUVCUHRUVNUVAUVBJJWEWFWJSOUVGUVKRZ
+      TZUVGUWFUVGPROUVGPUVJWGWAUWFUVGLVNZOUWFUVGUVJRZWKUWHUVGPUVJWHUWIUVGLUVGLN
+      UWILUVJRZUVQUVRQLUDUEUWJVAVGWIQLWLWMZUVGLUVJWNWOWPWQWAWRUWGJUVGKXBEABUUQG
+      HIABUVCGNOABCWSSPDUVKUVHGZHIZDUVKUVIGZNOUWMPFUVKWTZHIUWNUWLUWOPHUWODPUWBU
+      JZUVHGZUVKWTZUWLFUWQUVKFUWQNODUWPFXAZFUWPUWSFXNZOUWPUWSFXCUWTXDUWPUWSFXEV
+      HSXFVDXGUWBUVJVJZUVKUWPVJUWRUWLNUWJUXAUWKLUVJXHXIXJUWBUVJPXKDUWPUVKUVHXLX
+      OXMXPDUVKUVKYFXQXRSUVGUUQFXSUVGUUQJKXTYAVDABUVDUVFUVMUVDUVAUUTUVBMIZUUTJM
+      IZUGUVFUVAUUTUVBJMYBUVMUVAUXBUXCUVFUVMUWDUVAUXBUVFNUWEUWDUVATZUXBUVBUUTMI
+      UUTUFZUVFUXDUUTUVBUXDUUQUXDUUQUXDUUPUXDUUPUVTUWAUVAYCZVTZYDVTZUXDUUPUXGUV
+      TUWAUVAYEYGZYHZUVBPRUXDYISYJUXDUUTUXJYKUXDUXEJUUQUFZKIUVFUXDJUUQUXDYLUXHU
+      XIYMUXDUXKUUPJKUXDUUPUUQUXGUXDUUQUUPUFUXDUUPUXFUXDUUPLUXFUXDYNUWDUVAYOYQU
+      UAUUBUUCYPYRUUDYSUVMUWDUVAWKZUXCUVFNUWEUWDUXLTZUXCUUTUVFUXMUUTUXMUUTUXMUU
+      QUVTUUQERUWAUXLUVTUUPUUPUUEZYDYTUXMUUPUVTUVSUWAUXLUXNYTUVTUWAUXLYEYGUUFVT
+      UUGUXMUUQUUPJKUXMUUPUVTUWAUXLYCUWDLUUPUUHUEUXLUWDLUUPUWDYNUVTUWAUUIUUJUUK
+      UULYPYRYSUUMUUNUUOXR $.
+  $}
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -750072,8 +750246,7 @@ not even needed (it can be any class).  (Contributed by Glauco
   $( The positive reals form a set.  (Contributed by Glauco Siliprandi,
      11-Oct-2020.) $)
   rpex $p |- RR+ e. _V $=
-    ( crp ccnfld cmgp cfv cc cc0 csn cdif cress co csubg eqid rpmsubg elexi ) A
-    BCDEFGHIJZKDOOLMN $.
+    ( crp cr reex rpssre ssexi ) ABCDE $.
 
   $( A nonnegative extended real is nonnegative.  (Contributed by Glauco
      Siliprandi, 11-Oct-2020.) $)