diff --git a/set.mm b/set.mm
index 4eb1f1bd06..2c9709aebd 100644
--- a/set.mm
+++ b/set.mm
@@ -133131,11 +133131,10 @@ the existence of its supremum (see ~ suprcl ).  (Contributed by Paul
   iooneg $p |- ( ( A e. RR /\ B e. RR /\ C e. RR ) ->
                   ( C e. ( A (,) B ) <-> -u C e. ( -u B (,) -u A ) ) ) $=
     ( cr wcel w3a clt wbr wa cneg cioo co ltneg 3adant2 cxr rexr elioo5 renegcl
-    wb syl3an ancoms 3adant1 anbi12d ancom syl6bb 3com12 3bitr4d ) ADEZBDEZCDEZ
-    FZACGHZCBGHZIZBJZCJZGHZUPAJZGHZIZCABKLEZUPUOURKLEZUKUNUSUQIUTUKULUSUMUQUHUJ
-    ULUSSUIACMNUIUJUMUQSZUHUJUIVCCBMUAUBUCUSUQUDUEUHAOEUIBOEUJCOEVAUNSAPBPCPABC
-    QTUIUHUJVBUTSZUIUODEZUHURDEZUJUPDEZVDBRARCRVEUOOEVFUROEVGUPOEVDUOPURPUPPUOU
-    RUPQTTUFUG $.
+    wb syl3an ancoms 3adant1 anbi12d biancomd 3com12 3bitr4d ) ADEZBDEZCDEZFZAC
+    GHZCBGHZIZBJZCJZGHZUOAJZGHZIZCABKLEZUOUNUQKLEZUJUMUPURUJUKURULUPUGUIUKURSUH
+    ACMNUHUIULUPSZUGUIUHVBCBMUAUBUCUDUGAOEUHBOEUICOEUTUMSAPBPCPABCQTUHUGUIVAUSS
+    ZUHUNDEZUGUQDEZUIUODEZVCBRARCRVDUNOEVEUQOEVFUOOEVCUNPUQPUOPUNUQUOQTTUEUF $.
 
   $( Membership in a negated closed real interval.  (Contributed by Paul
      Chapman, 26-Nov-2007.) $)
@@ -133204,12 +133203,12 @@ the existence of its supremum (see ~ suprcl ).  (Contributed by Paul
     icodisj $p |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) ->
                     ( ( A [,) B ) i^i ( B [,) C ) ) = (/) ) $=
       ( vx cxr wcel w3a cico co cin c0 wss wceq wa clt wbr cle wb elico1 biimpa
-      cv 3adant3 simp3d adantrr wn 3adant1 simp2d simpl2 simp1d xrlenlt syl2anc
-      elin mpbid adantrl pm2.65da pm2.21d syl5bi ssrdv ss0 syl ) AEFZBEFZCEFZGZ
-      ABHIZBCHIZJZKLVGKMVDDVGKDUAZVGFVHVEFZVHVFFZNZVDVHKFZVHVEVFULVDVKVLVDVKVHB
-      OPZVDVIVMVJVDVINVHEFZAVHQPZVMVDVIVNVOVMGZVAVBVIVPRVCABVHSUBTUCUDVDVJVMUEZ
-      VIVDVJNZBVHQPZVQVRVNVSVHCOPZVDVJVNVSVTGZVBVCVJWARVABCVHSUFTZUGVRVBVNVSVQR
-      VAVBVCVJUHVRVNVSVTWBUIBVHUJUKUMUNUOUPUQURVGUSUT $.
+      elin 3adant3 simp3d adantrr 3adant1 simp2d simpl2 simp1d xrlenltd adantrl
+      cv wn mpbid pm2.65da pm2.21d syl5bi ssrdv ss0 syl ) AEFZBEFZCEFZGZABHIZBC
+      HIZJZKLVFKMVCDVFKDUKZVFFVGVDFZVGVEFZNZVCVGKFZVGVDVEUAVCVJVKVCVJVGBOPZVCVH
+      VLVIVCVHNVGEFZAVGQPZVLVCVHVMVNVLGZUTVAVHVORVBABVGSUBTUCUDVCVIVLULZVHVCVIN
+      ZBVGQPZVPVQVMVRVGCOPZVCVIVMVRVSGZVAVBVIVTRUTBCVGSUETZUFVQBVGUTVAVBVIUGVQV
+      MVRVSWAUHUIUMUJUNUOUPUQVFURUS $.
 
     ${
       $d A w x y z $.  $d B w x y z $.
@@ -133295,11 +133294,11 @@ the existence of its supremum (see ~ suprcl ).  (Contributed by Paul
     ioodisj $p |- ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) )
      /\ B <_ C ) -> ( ( A (,) B ) i^i ( C (,) D ) ) = (/) ) $=
       ( vx vy vz vw cxr wcel wa cle cioo co cin c0 wss wceq cicc syl wbr iooss1
-      simpllr sylancom ioossicc syl6ss sslin simplll simplrr clt df-ioo xrlenlt
-      df-icc cv ixxdisj syl3anc sseqtrd ss0 ) AIJZBIJZKZCIJZDIJZKZKZBCLUAZKZABM
-      NZCDMNZOZPQVJPRVGVJVHBDSNZOZPVGVIVKQVJVLQVGVIBDMNZVKVEVFUTVIVMQUSUTVDVFUC
-      ZBCDUBUDBDUEUFVIVKVHUGTVGUSUTVCVLPRUSUTVDVFUHVNVAVBVCVFUIEFGHABDSUJUJLLME
-      FGUKEFGUMBHUNULUOUPUQVJURT $.
+      ad4ant24 ioossicc syl6ss sslin simplll simpllr simplrr clt df-ioo xrlenlt
+      df-icc cv ixxdisj syl3anc sseqtrd ss0 ) AIJZBIJZKZCIJZDIJZKZKBCLUAZKZABMN
+      ZCDMNZOZPQVIPRVFVIVGBDSNZOZPVFVHVJQVIVKQVFVHBDMNZVJUTVEVHVLQUSVDBCDUBUCBD
+      UDUEVHVJVGUFTVFUSUTVCVKPRUSUTVDVEUGUSUTVDVEUHVAVBVCVEUIEFGHABDSUJUJLLMEFG
+      UKEFGUMBHUNULUOUPUQVIURT $.
 
     $( Join two open intervals to create a third.  (Contributed by NM,
        11-Aug-2008.)  (Proof shortened by Mario Carneiro, 16-Jun-2014.) $)
@@ -133321,23 +133320,23 @@ the existence of its supremum (see ~ suprcl ).  (Contributed by Paul
       3anass notbii ianor pm2.24d mnflt simpr simpll ltnle bicomd syl2anc mnfxr
       biimpa ad3antrrr sylancr mpbir3and adantll ltpnf ad3antlr sylancl sylbird
       elioo1 pnfxr orim12d jaod sylbid expimpd elun syl6ibr ioossre unssi sseli
-      elioo2 biimpd a1i com13 3impd xrltnle com3l com14 syl imp intnand sylnibr
-      sylibr anim12i mpbird jca impbid syl5bb eqrdv ) ACDZBCDZEZUACABUBFZUCZGAU
-      DFZBHUDFZUEZUAUFZXHDXLCDZXLXGDZIZEZXFXLXKDZXLCXGUGXFXPXQXFXPXLXIDZXLXJDZU
-      HZXQXFXMXOXTXFXMEZXOXLJDZAXLUIKZXLBUIKZLZIZXTYAXNYEXFXNYEMZXMXDAJDZBJDZYG
-      XEAUJZBUJZABXLUKZULNUMYFYBYCYDEZEZIZYAXTYEYNYBYCYDUNZUOYOYBIZYMIZUHYAXTYB
-      YMUPYAYQXTYRXMYQXTOXFXMYBXTXLUJZUQPYRYCIZYDIZUHZYAXTYCYDUPZYAYTXRUUAXSYAY
-      TXRYAYTEZXRYBGXLQKZXLAQKZXMYBXFYTYSRXMUUEXFYTXLURRYAYTUUFYAXMXDYTUUFMXFXM
-      USXDXEXMUTXMXDEZUUFYTXLAVAZVBVCVEUUDGJDZYHXRYBUUEUUFLMVDXDYHXEXMYTYJVFGAX
-      LVNVGVHSYAUUABXLQKZXSXEXMUUJUUAMXDBXLVAVIYAUUJXSYAUUJEZXSYBUUJXLHQKZXMYBX
-      FUUJYSRYAUUJUSXMUULXFUUJXLVJRUUKYIHJDZXSYBUUJUULLZMZXEYIXDXMUUJYKVKVOBHXL
-      VNZVLVHSVMVPTVQTTVRVSXLXIXJVTZWAXFXQXPXFXQEZXMXOXQXMXFXKCXLXIXJCGAWBBHWBW
-      CWDPUURXOYFUURYNYEUURYMYBUURUUBYRXFXQUUBXQXTXFUUBUUQXFXRYTXSUUAXFXRXMUUEU
-      UFLZYTXDXRUUSMZXEXDUUIYHUUTVDYJGAXLWEVGNXFXMUUEUUFYTXDXMUUEUUFYTOZOOXEUUE
-      XMXDUVAXMXDUVAOOUUEXMXDUVAUUGUUFYTUUHWFSWGWHNWIVRXFXSUUNUUAXFYIUUMUUOXEYI
-      XDYKPVOUUPVLXFYBUUJUULUUAXEYBUUJUULUUAOOOZXDXEYIUVBYKUULYBUUJYIUUAYBUUJYI
-      UUAOOOUULYIYBUUJUUAYIYBUUJUUAOYIYBEUUJUUABXLWJWFSWKWGWLWMPWIVRVPTWNUUCWQW
-      OYPWPUURYHYIEZXOYFMXFUVCXQXDYHXEYIYJYKWRNUVCXNYEYLUMWMWSWTSXAXBXC $.
+      elioo2 biimpd a1i com13 3impd xrltnle a1ddd syl imp sylibr intnand mpbird
+      sylnibr anim12i jca impbid syl5bb eqrdv ) ACDZBCDZEZUACABUBFZUCZGAUDFZBHU
+      DFZUEZUAUFZXGDXKCDZXKXFDZIZEZXEXKXJDZXKCXFUGXEXOXPXEXOXKXHDZXKXIDZUHZXPXE
+      XLXNXSXEXLEZXNXKJDZAXKUIKZXKBUIKZLZIZXSXTXMYDXEXMYDMZXLXCAJDZBJDZYFXDAUJZ
+      BUJZABXKUKZULNUMYEYAYBYCEZEZIZXTXSYDYMYAYBYCUNZUOYNYAIZYLIZUHXTXSYAYLUPXT
+      YPXSYQXLYPXSOXEXLYAXSXKUJZUQPYQYBIZYCIZUHZXTXSYBYCUPZXTYSXQYTXRXTYSXQXTYS
+      EZXQYAGXKQKZXKAQKZXLYAXEYSYRRXLUUDXEYSXKURRXTYSUUEXTXLXCYSUUEMXEXLUSXCXDX
+      LUTXLXCEZUUEYSXKAVAZVBVCVEUUCGJDZYGXQYAUUDUUELMVDXCYGXDXLYSYIVFGAXKVNVGVH
+      SXTYTBXKQKZXRXDXLUUIYTMXCBXKVAVIXTUUIXRXTUUIEZXRYAUUIXKHQKZXLYAXEUUIYRRXT
+      UUIUSXLUUKXEUUIXKVJRUUJYHHJDZXRYAUUIUUKLZMZXDYHXCXLUUIYJVKVOBHXKVNZVLVHSV
+      MVPTVQTTVRVSXKXHXIVTZWAXEXPXOXEXPEZXLXNXPXLXEXJCXKXHXICGAWBBHWBWCWDPUUQXN
+      YEUUQYMYDUUQYLYAUUQUUAYQXEXPUUAXPXSXEUUAUUPXEXQYSXRYTXEXQXLUUDUUELZYSXCXQ
+      UURMZXDXCUUHYGUUSVDYIGAXKWEVGNXEXLUUDUUEYSXCXLUUDUUEYSOZOOXDUUDXLXCUUTXLX
+      CUUTOOUUDXLXCUUTUUFUUEYSUUGWFSWGWHNWIVRXEXRUUMYTXEYHUULUUNXDYHXCYJPVOUUOV
+      LXEYAUUIUUKYTXDYAUUIUUKYTOOOZXCXDYHUVAYJYHYAUUIUUKYTYHYAUUIYTOYHYAEUUIYTB
+      XKWJWFSWKWLPWIVRVPTWMUUBWNWOYOWQUUQYGYHEZXNYEMXEUVBXPXCYGXDYHYIYJWRNUVBXM
+      YDYKUMWLWPWSSWTXAXB $.
   $}
 
   ${
@@ -133506,19 +133505,19 @@ the existence of its supremum (see ~ suprcl ).  (Contributed by Paul
      Carneiro, 8-Sep-2015.) $)
   lincmb01cmp $p |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ T e. ( 0 [,] 1 ) )
                   -> ( ( ( 1 - T ) x. A ) + ( T x. B ) ) e. ( A [,] B ) ) $=
-    ( cr wcel wbr cc0 c1 cicc co cmin cmul caddc wb a1i 1re eqid syl22anc recnd
-    cle clt w3a wa simpr crp elicc01 simp1bi adantl difrp biimp3a adantr iccdil
-    0re simpl2 simpl1 resubcld mul02d mulid2d oveq12d eleqtrd remulcld iccshftr
-    mpbid mulcld subadd23d subdid oveq1d resubcl sylancr addcomd subdird oveq2d
-    1cnd eqtrd 3eqtr4d addid2d npcand 3eltr3d ) ADEZBDEZABUAFZUBZCGHIJEZUCZCBAK
-    JZLJZAMJZGAMJZWEAMJZIJZHCKJZALJZCBLJZMJZABIJWDWFGWEIJZEZWGWJEZWDWFGWELJZHWE
-    LJZIJZWOWDWCWFWTEZWBWCUDWDGDEZHDEZCDEZWEUEEZWCXANXBWDUMOZXCWDPOWCXDWBWCXDGC
-    TFCHTFCUFUGUHZWBXEWCVSVTWAXEABUIUJUKGHWRWSWECWRQWSQULRVCWDWRGWSWEIWDWEWDWEW
-    DBAVSVTWAWCUNZVSVTWAWCUOZUPZSZUQWDWEXKURUSUTWDXBWEDEWFDEVSWPWQNXFXJWDCWEXGX
-    JVAXIGWEWHWIAWFWHQWIQVBRVCWDWMCALJZKJZAMJWMAXLKJZMJZWGWNWDWMXLAWDCBWDCXGSZW
-    DBXHSZVDZWDCAXPWDAXISZVDXSVEWDWFXMAMWDCBAXPXQXSVFVGWDWNWMWLMJXOWDWLWMWDWLWD
-    WKAWDXCXDWKDEPXGHCVHVIXIVASXRVJWDWLXNWMMWDWLHALJZXLKJXNWDHCAWDVMXPXSVKWDXTA
-    XLKWDAXSURVGVNVLVNVOWDWHAWIBIWDAXSVPWDBAXQXSVQUSVR $.
+    ( cr wcel wbr cc0 c1 cicc co cmin cmul caddc wb eqid syl22anc mpbid mulid2d
+    cle recnd clt w3a simpr crp 0red 1red elicc01 simp1bi adantl biimp3a adantr
+    difrp iccdil simpl2 simpl1 resubcld mul02d oveq12d remulcld iccshftr mulcld
+    wa eleqtrd subadd23d subdid oveq1d 1re resubcl sylancr addcomd 1cnd subdird
+    eqtrd oveq2d 3eqtr4d addid2d npcand 3eltr3d ) ADEZBDEZABUAFZUBZCGHIJEZVBZCB
+    AKJZLJZAMJZGAMJZWEAMJZIJZHCKJZALJZCBLJZMJZABIJWDWFGWEIJZEZWGWJEZWDWFGWELJZH
+    WELJZIJZWOWDWCWFWTEZWBWCUCWDGDEZHDEZCDEZWEUDEZWCXANWDUEZWDUFWCXDWBWCXDGCSFC
+    HSFCUGUHUIZWBXEWCVSVTWAXEABULUJUKGHWRWSWECWROWSOUMPQWDWRGWSWEIWDWEWDWEWDBAV
+    SVTWAWCUNZVSVTWAWCUOZUPZTZUQWDWEXKRURVCWDXBWEDEWFDEVSWPWQNXFXJWDCWEXGXJUSXI
+    GWEWHWIAWFWHOWIOUTPQWDWMCALJZKJZAMJWMAXLKJZMJZWGWNWDWMXLAWDCBWDCXGTZWDBXHTZ
+    VAZWDCAXPWDAXITZVAXSVDWDWFXMAMWDCBAXPXQXSVEVFWDWNWMWLMJXOWDWLWMWDWLWDWKAWDX
+    CXDWKDEVGXGHCVHVIXIUSTXRVJWDWLXNWMMWDWLHALJZXLKJXNWDHCAWDVKXPXSVLWDXTAXLKWD
+    AXSRVFVMVNVMVOWDWHAWIBIWDAXSVPWDBAXQXSVQURVR $.
 
   ${
     $d x y A $.  $d x y B $.
@@ -133561,10 +133560,10 @@ the existence of its supremum (see ~ suprcl ).  (Contributed by Paul
        Carneiro, 8-Sep-2015.) $)
     iccen $p |- ( ( A e. RR /\ B e. RR /\ A < B ) ->
       ( 0 [,] 1 ) ~~ ( A [,] B ) ) $=
-      ( vx vy cr wcel clt wbr w3a cc0 c1 cicc co cmul cmin caddc cmpt cvv ovex
-      cv wf1o cen ccnv cdiv wceq eqid iccf1o simpld f1oen2g mp3an12 syl ) AEFBE
-      FABGHIZJKLMZABLMZCUMCTZBNMKUOOMANMPMQZUAZUMUNUBHZULUQUPUCDUNDTAOMBAOMUDMQ
-      UECDABUPUPUFUGUHUMRFUNRFUQURJKLSABLSUMUNUPRRUIUJUK $.
+      ( vx vy cc0 c1 cicc co cvv wcel cr clt wbr w3a cmul cmin caddc cmpt ovex
+      cv wf1o cen ccnv cdiv wceq eqid iccf1o simpld f1oen2g mp3an12i ) EFGHZIJA
+      BGHZIJAKJBKJABLMNZUKULCUKCTZBOHFUNPHAOHQHRZUAZUKULUBMEFGSABGSUMUPUOUCDULD
+      TAPHBAPHUDHRUECDABUOUOUFUGUHUKULUOIIUIUJ $.
   $}
 
   ${
@@ -133625,11 +133624,11 @@ the existence of its supremum (see ~ suprcl ).  (Contributed by Paul
     $( The supremum of a bounded set of real numbers is an upper bound.
        (Contributed by Thierry Arnoux, 20-May-2019.) $)
     supiccub $p |- ( ph -> D <_ sup ( A , RR , < ) ) $=
-      ( vx vy cr wss cv cle wbr wral wcel syl2anc c0 wne wrex csup cicc iccssre
-      clt co sstrd wa adantr rexrd sselda iccleub syl3anc ralrimiva brralrspcev
-      cxr suprub syl31anc ) ABMNBUAUBKOZLOPQKBRLMUCZEBSEBMUGUDPQABCDUEUHZMHACMS
-      ZDMSZVCMNFGCDUFTUIIAVEVADPQZKBRVBGAVFKBAVABSZUJZCURSDURSVAVCSVFVHCAVDVGFU
-      KULVHDAVEVGGUKULABVCVAHUMCDVAUNUOUPLKVADPMBUQTJLKBEUSUT $.
+      ( vy vx cr wcel syl2anc cv cle wbr wral cxr cicc co iccssre sstrd wrex wa
+      wss adantr rexrd sselda iccleub syl3anc ralrimiva brralrspcev suprubd ) A
+      KLBEABCDUAUBZMHACMNZDMNZUPMUGFGCDUCOUDIAURLPZDQRZLBSUSKPQRLBSKMUEGAUTLBAU
+      SBNZUFZCTNDTNUSUPNUTVBCAUQVAFUHUIVBDAURVAGUHUIABUPUSHUJCDUSUKULUMKLUSDQMB
+      UNOJUO $.
 
     $d A z $.  $d D z $.
     $( The supremum of a bounded set of real numbers is the least upper bound.
@@ -133647,11 +133646,11 @@ the existence of its supremum (see ~ suprcl ).  (Contributed by Paul
     $( The supremum of a bounded set of real numbers is the least upper bound.
        (Contributed by Thierry Arnoux, 23-May-2019.) $)
     supicclub2 $p |- ( ph -> sup ( A , RR , < ) <_ D ) $=
-      ( clt cle wbr wn wcel cxr wb xrlenlt cr csup cv wrex wa co iccssxr syl6ss
-      sselda sseldd adantr syl2anc nrexdv supicclub mtbird supicc sseldi mpbird
-      cicc mpbid ) ACUAMUBZFNOZFVAMOZPZAVCFBUCZMOZBCUDAVFBCAVECQZUEZVEFNOZVFPZL
-      VHVERQFRQZVIVJSACRVEACDEUSUFZRIDEUGZUHZUIAVKVGACRFVNKUJZUKVEFTULUTUMABCDE
-      FGHIJKUNUOAVARQVKVBVDSAVLRVAVMACDEGHIJUPUQVOVAFTULUR $.
+      ( cr clt csup cicc co cxr wbr wcel iccssxr supicc sseldi syl6ss sseldd cv
+      wrex wa cle sselda adantr xrlenltd mpbid nrexdv supicclub mtbird xrnltled
+      wn ) ACMNOZFADEPQZRUSDEUAZACDEGHIJUBUCACRFACUTRIVAUDZKUEZAFUSNSFBUFZNSZBC
+      UGAVEBCAVDCTZUHZVDFUISVEURLVGVDFACRVDVBUJAFRTVFVCUKULUMUNABCDEFGHIJKUOUPU
+      Q $.
   $}
 
   $( The sum of an integer and a real number between 0 and 1 is less than or
@@ -133721,18 +133720,18 @@ the existence of its supremum (see ~ suprcl ).  (Contributed by Paul
     fzval2 $p |- ( ( M e. ZZ /\ N e. ZZ ) ->
         ( M ... N ) = ( ( M [,] N ) i^i ZZ ) ) $=
       ( vk cz wcel wa cfz co cv cle wbr crab cicc cin fzval wceq cr zssre sseli
-      cxr ressxr sstri iccval syl2an ineq1d inrab2 wss sseqin2 mpbi rabeq ax-mp
-      eqtri syl6req eqtrd ) ADEZBDEZFZABGHACIZJKURBJKFZCDLZABMHZDNZCABOUQVBUSCT
-      LZDNZUTUQVAVCDUOATEBTEVAVCPUPDTADQTRUAUBZSDTBVESCABUCUDUEVDUSCTDNZLZUTUSC
-      TDUFVFDPZVGUTPDTUGVHVEDTUHUIUSCVFDUJUKULUMUN $.
+      cxr ressxr sstri iccval syl2an ineq1d inrab2 sseqin2 rabeqi eqtri syl6req
+      wss mpbi eqtrd ) ADEZBDEZFZABGHACIZJKUQBJKFZCDLZABMHZDNZCABOUPVAURCTLZDNZ
+      USUPUTVBDUNATEBTEUTVBPUODTADQTRUAUBZSDTBVDSCABUCUDUEVCURCTDNZLUSURCTDUFUR
+      CVEDDTUKVEDPVDDTUGULUHUIUJUM $.
 
     $( Establish the domain and codomain of the finite integer sequence
        function.  (Contributed by Scott Fenton, 8-Aug-2013.)  (Revised by Mario
        Carneiro, 16-Nov-2013.) $)
     fzf $p |- ... : ( ZZ X. ZZ ) --> ~P ZZ $=
-      ( vm vk vn cv cle wbr wa cz crab cpw wcel cxp cfz wf wss ssrab2 zex elpw2
-      wral mpbir rgen2w df-fz fmpt2 mpbi ) ADBDZEFUECDEFGZBHIZHJZKZCHSAHSHHLUHM
-      NUIACHHUIUGHOUFBHPUGHQRTUAACHHUGUHMBACUBUCUD $.
+      ( vm vk vn cv cle wbr wa crab cpw wcel wral cxp cfz cvv zex ssrab2 elpwi2
+      cz wf rgen2w df-fz fmpt2 mpbi ) ADBDZEFUDCDEFGZBRHZRIZJZCRKARKRRLUGMSUHAC
+      RRUFRNOUEBRPQTACRRUFUGMBACUAUBUC $.
   $}
 
   ${
@@ -133787,11 +133786,11 @@ the existence of its supremum (see ~ suprcl ).  (Contributed by Paul
      Carneiro, 28-Apr-2015.) $)
   elfzuzb $p |- ( K e. ( M ... N ) <->
          ( K e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) ) $=
-    ( cz wcel w3a cle wbr wa cfz cuz cfv df-3an an6 anandir ancom anbi2i 3bitri
-    co eluz2 anbi1i 3bitr4ri elfz2 anbi12i 3bitr4i ) BDEZCDEZADEZFZBAGHZACGHZIZ
-    IZUFUHUJFZUHUGUKFZIZABCJSEABKLEZCAKLEZIUFUHIZUHUGIZULFUSUTIZULIUPUMUSUTULMU
-    FUHUJUHUGUKNUIVAULUIUFUGIUHIUSUGUHIZIVAUFUGUHMUFUGUHOVBUTUSUGUHPQRUAUBABCUC
-    UQUNURUOBATACTUDUE $.
+    ( cz wcel w3a cle wbr wa cfz cuz cfv df-3an an6 anandir 3bitri anbi1i eluz2
+    co an43 3bitr4ri elfz2 anbi12i 3bitr4i ) BDEZCDEZADEZFZBAGHZACGHZIZIZUEUGUI
+    FZUGUFUJFZIZABCJSEABKLEZCAKLEZIUEUGIZUGUFIZUKFURUSIZUKIUOULURUSUKMUEUGUIUGU
+    FUJNUHUTUKUHUEUFIUGIURUFUGIIUTUEUFUGMUEUFUGOUEUGUFUGTPQUAABCUBUPUMUQUNBARAC
+    RUCUD $.
 
   $( Membership in a finite set of sequential integers.  (Contributed by NM,
      4-Oct-2005.)  (Revised by Mario Carneiro, 28-Apr-2015.) $)
@@ -134055,11 +134054,11 @@ the existence of its supremum (see ~ suprcl ).  (Contributed by Paul
     $( Condition for two finite intervals of integers to be disjoint.
        (Contributed by Jeff Madsen, 17-Jun-2010.) $)
     fzdisj $p |- ( K < M -> ( ( J ... K ) i^i ( M ... N ) ) = (/) ) $=
-      ( vx clt wbr cfz co cin cv wcel wa wn elin cle cz adantl zred adantr cr
-      elfzel1 elfzelz elfzel2 elfzle1 elfzle2 letrd lenltd mpbid sylbi eq0rdv
-      con2i ) BCFGZEABHIZCDHIZJZEKZUPLZUMURUQUNLZUQUOLZMZUMNZUQUNUOOVACBPGVBVAC
-      UQBVACUTCQLUSUQCDUBRSZUTUQUALUSUTUQUQCDUCSRVABUSBQLUTUQABUDTSZUTCUQPGUSUQ
-      CDUERUSUQBPGUTUQABUFTUGVACBVCVDUHUIUJULUK $.
+      ( vx clt wbr cfz co cin cv wcel wa wn elin cz adantl zred adantr cle cr
+      elfzel1 elfzel2 elfzelz elfzle1 elfzle2 letrd lensymd sylbi con2i eq0rdv
+      ) BCFGZEABHIZCDHIZJZEKZUOLZULUQUPUMLZUPUNLZMZULNUPUMUNOUTCBUTCUSCPLURUPCD
+      UBQRZUTBURBPLUSUPABUCSRZUTCUPBVAUSUPUALURUSUPUPCDUDRQVBUSCUPTGURUPCDUEQUR
+      UPBTGUSUPABUFSUGUHUIUJUK $.
   $}
 
   $( 0-based and 1-based finite sets of sequential integers are equinumerous.
@@ -134237,8 +134236,8 @@ the existence of its supremum (see ~ suprcl ).  (Contributed by Paul
   $( Finite sets of sequential integers starting from a natural are a subset of
      the positive integers.  (Contributed by Thierry Arnoux, 4-Aug-2017.) $)
   fzssnn $p |- ( M e. NN -> ( M ... N ) C_ NN ) $=
-    ( cn wcel cfz co c1 wss cuz cfv fzss1 nnuz eleq2s fzssuz sseqtr4i syl6ss )
-    ACDABEFZGBEFZCQRHAGIJZCAGBKLMRSCGBNLOP $.
+    ( cn wcel cfz co c1 wss cuz cfv fzss1 nnuz eleq2s fz1ssnn syl6ss ) ACDABEFZ
+    GBEFZCPQHAGIJCAGBKLMBNO $.
 
   ${
     $d I k $.  $d M k $.  $d N k $.
@@ -134337,13 +134336,13 @@ subset of a (possibly extended) finite sequence of integers.  (Contributed
   fznatpl1 $p |- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) ->
            ( I + 1 ) e. ( 1 ... N ) ) $=
     ( wcel c1 co cfz wa caddc cle wbr cr zred adantl peano2re syl wb 1re mp3an2
-    cz syl2anc cn cmin elfzelz ltp1d elfzle1 leadd1 mp3an13 mpbid ltletrd ltled
+    cz syl2an2 cn cmin elfzelz ltp1d elfzle1 leadd1 mp3an13 mpbid ltletrd ltled
     1red elfzle2 nnz adantr leaddsub mpbird peano2zd 1z elfz mpbir2and ) BUACZA
-    DBDUBEZFECZGZADHEZDBFECZDVEIJZVEBIJZVDDVEVDUKZVDAKCZVEKCVCVJVAVCAADVBUCZLMZ
-    ANOZVDDDDHEZVEVIVDDKCZVNKCVIDNOVMVDDVIUDVDDAIJZVNVEIJZVCVPVAADVBUEMVDVJVPVQ
-    PZVLVOVJVOVRQQDADUFUGOUHUIUJVDVHAVBIJZVCVSVAADVBULMVDVJBKCZVHVSPZVLVDBVABSC
-    ZVCBUMUNZLVJVOVTWAQADBUORTUPVDVESCZWBVFVGVHGPZVCWDVAVCAVKUQMWCWDDSCWBWEURVE
-    DBUSRTUT $.
+    DBDUBEZFECZGZADHEZDBFECZDVEIJZVEBIJZVDDVEVDUKZVDAKCZVEKCVCVJVAVCAADVBUCZLZM
+    ZANOZVDDDDHEZVEVIVDDKCZVOKCVIDNOVNVDDVIUDVDDAIJZVOVEIJZVCVQVAADVBUEMVDVJVQV
+    RPZVMVPVJVPVSQQDADUFUGOUHUIUJVDVHAVBIJZVCVTVAADVBULMVCVJVABKCZVHVTPZVLVDBVA
+    BSCZVCBUMUNZLVJVPWAWBQADBUORTUPVCVESCZVAWCVFVGVHGPZVCAVKUQWDWEDSCWCWFURVEDB
+    USRTUT $.
 
   ${
     $d M m $.
@@ -134411,12 +134410,11 @@ subset of a (possibly extended) finite sequence of integers.  (Contributed
        (Contributed by NM, 5-Sep-2011.) $)
     fzprval $p |- ( A. x e. ( 1 ... 2 ) ( F ` x ) = if ( x = 1 , A , B )
                   <-> ( ( F ` 1 ) = A /\ ( F ` 2 ) = B ) ) $=
-      ( cv cfv c1 wceq cif c2 cfz co wral cpr wa caddc df-2 fveq2 eqeq12d wne
-      cz wcel 1z fzpr ax-mp oveq2i preq2i 3eqtr4i raleqi 1ex iftrue 1ne2 necomi
-      2ex pm13.181 mpan2 neneqd iffalsed ralpr bitri ) AEZDFZVAGHZBCIZHZAGJKLZM
-      VEAGJNZMGDFZBHZJDFZCHZOVEAVFVGGGGPLZKLZGVLNZVFVGGUAUBVMVNHUCGUDUEJVLGKQUF
-      JVLGQUGUHUIVEVIVKAGJUJUNVCVBVHVDBVAGDRVCBCUKSVAJHZVBVJVDCVAJDRVOVCBCVOVAG
-      VOJGTVAGTGJULUMVAJGUOUPUQURSUSUT $.
+      ( cv cfv c1 wceq cif c2 cfz co wral cpr fz12pr raleqi fveq2 eqeq12d wne
+      wa 1ex 2ex iftrue 1ne2 necomi pm13.181 mpan2 neneqd iffalsed ralpr bitri
+      ) AEZDFZULGHZBCIZHZAGJKLZMUPAGJNZMGDFZBHZJDFZCHZTUPAUQUROPUPUTVBAGJUAUBUN
+      UMUSUOBULGDQUNBCUCRULJHZUMVAUOCULJDQVCUNBCVCULGVCJGSULGSGJUDUEULJGUFUGUHU
+      IRUJUK $.
   $}
 
   ${
@@ -134528,24 +134526,24 @@ subset of a (possibly extended) finite sequence of integers.  (Contributed
     uzsplit $p |- ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` M ) =
                   ( ( M ... ( N - 1 ) ) u. ( ZZ>= ` N ) ) ) $=
       ( vk cuz cfv wcel c1 cmin co cfz wo wa cle wbr cr eluzelre syl2an eluzelz
-      cz wb cun clt lelttric eluz eluzel2 w3a elfzm11 df-3an syl6bb syl2anr jca
-      cv eluzle adantl biantrurd bitr4d orbi12d mpbird orcomd elfzuz a1i expcom
-      ex wi uztrn jaod impbid elun syl6bbr eqrdv ) BADEZFZCVKABGHIZJIZBDEZUAZVL
-      CULZVKFZVQVNFZVQVOFZKZVQVPFVLVRWAVLVRWAVLVRLZVTVSWBVTVSKBVQMNZVQBUBNZKZVL
-      BOFVQOFWEVRABPAVQPBVQUCQWBVTWCVSWDVLBSFZVQSFZVTWCTVRABRZAVQRZBVQUDQWBVSWG
-      AVQMNZLZWDLZWDVRASFZWFVSWLTVLAVQUEWHWMWFLVSWGWJWDUFWLVQABUGWGWJWDUHUIUJWB
-      WKWDVRWKVLVRWGWJWIAVQUMUKUNUOUPUQURUSVCVLVSVRVTVSVRVDVLVQAVMUTVAVTVLVRBVQ
-      AVEVBVFVGVQVNVOVHVIVJ $.
+      cz wb cun cv clt lelttric eluzle jca adantl eluzel2 elfzm11 df-3an syl6bb
+      eluz w3a syl2anr mpbirand orbi12d mpbird orcomd ex wi elfzuz uztrn expcom
+      a1i jaod impbid elun syl6bbr eqrdv ) BADEZFZCVJABGHIZJIZBDEZUAZVKCUBZVJFZ
+      VPVMFZVPVNFZKZVPVOFVKVQVTVKVQVTVKVQLZVSVRWAVSVRKBVPMNZVPBUCNZKZVKBOFVPOFW
+      DVQABPAVPPBVPUDQWAVSWBVRWCVKBSFZVPSFZVSWBTVQABRZAVPRZBVPULQWAVRWFAVPMNZLZ
+      WCVQWJVKVQWFWIWHAVPUEUFUGVQASFZWEVRWJWCLZTVKAVPUHWGWKWELVRWFWIWCUMWLVPABU
+      IWFWIWCUJUKUNUOUPUQURUSVKVRVQVSVRVQUTVKVPAVLVAVDVSVKVQBVPAVBVCVEVFVPVMVNV
+      GVHVI $.
 
     $( The first ` N ` elements of an upper integer set are distinct from any
        later members.  (Contributed by Mario Carneiro, 24-Apr-2014.) $)
     uzdisj $p |- ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) = (/) $=
-      ( vk c1 cmin co cfz cuz cfv cin c0 wss wceq wcel wbr cle syl mpbid zred
-      cz cv elin simprbi eluzle eluzel2 eluzelz zlem1lt syl2anc simplbi elfzle2
-      clt wb wn peano2zm lenltd pm2.21dd ssriv ss0 ax-mp ) ABDEFZGFZBHIZJZKLVCK
-      MCVCKCUAZVCNZUTVDUKOZVDKNVEBVDPOZVFVEVDVBNZVGVEVDVANZVHVDVAVBUBZUCZBVDUDQ
-      VEBTNZVDTNZVGVFULVEVHVLVKBVDUEQZVEVHVMVKBVDUFQZBVDUGUHRVEVDUTPOZVFUMVEVIV
-      PVEVIVHVJUIVDAUTUJQVEVDUTVEVDVOSVEUTVEVLUTTNVNBUNQSUORUPUQVCURUS $.
+      ( vk c1 cmin co cfz cuz cfv cin c0 wss wceq cv wcel wbr cle syl cz zred
+      clt elinel2 eluzle eluzel2 eluzelz zlem1lt syl2anc mpbid peano2zm elinel1
+      wb elfzle2 lensymd pm2.21dd ssriv ss0 ax-mp ) ABDEFZGFZBHIZJZKLVAKMCVAKCN
+      ZVAOZURVBUAPZVBKOVCBVBQPZVDVCVBUTOZVEVBUSUTUBZBVBUCRVCBSOZVBSOZVEVDUKVCVF
+      VHVGBVBUDRZVCVFVIVGBVBUERZBVBUFUGUHVCVBURVCVBVKTVCURVCVHURSOVJBUIRTVCVBUS
+      OVBURQPVBUSUTUJVBAURULRUMUNUOVAUPUQ $.
   $}
 
   ${
@@ -134557,33 +134555,32 @@ subset of a (possibly extended) finite sequence of integers.  (Contributed
         ( ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) <->
           ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\
             F = ( G |` ( 1 ... N ) ) ) ) ) $=
-      ( cn0 wcel c1 co wf cun wceq cfv cres csn c0 cn 3syl cfz w3a caddc wa cin
-      simpr1 nn0p1nn adantr simpr2 fsng mpbiri syl2anc snssd fssd fzp1disj fun2
-      cop a1i syl21anc cz cmin cuz simpl cc0 nn0uz 1m1e0 fveq2i eqtr4i syl6eleq
-      1z fzsuc2 sylancr eqcomd feq2d mpbid simpr3 feq1d mpbird ovex fvres ax-mp
-      reseq1d wfn wb ffn fnresdisj uneq1d resundir uncom eqtr2i 3eqtr4g fnresdm
-      snid 3eqtrd fveq1d fveq1i fvsng syl5eq eqtrd syl5eqr incom uneq2d 3eqtrrd
-      un0 eqcomi 3jca wss fzssp1 sylancl nnuz eluzfz2 ffvelrnd eqeltrrd fnressn
-      fssres syl opeq2 sneqd syl6reqr uneq12d reseq2d resundi syl6req impbida )
-      FHIZJFUAKZACLZBAIZDCEMZNZUBZJFJUCKZUAKZADLZYLDOZBNZCDYFPZNZUBZYEYKUDZYNYP
-      YRYTYNYMAYILZYTYFYLQZMZAYILZUUAYTYGUUBAELZYFUUBUEZRNZUUDYEYGYHYJUFZYTUUBB
-      QZAEYTYLSIZYHUUBUUIELZYEUUJYKFUGZUHZYEYGYHYJUIZUUJYHUDZUUKEYLBUQZQZNGYLBS
-      AEUJUKULZYTBAUUNUMUNZUUGYTJFUOURZYFUUBACEUPUSYTUUCYMAYIYTYMUUCYTJUTIZFJJV
-      AKZVBOZIZYMUUCNZVJYTFHUVCYEYKVCHVDVBOUVCVEUVBVDVBVFVGVHZVIJFVKZVLVMVNVOYT
-      YMADYIYEYGYHYJVPZVQVRYTYOYLDUUBPZOZBYLUUBIUVJYONYLFJUCVSWMYLUUBDVTWAYTUVJ
-      YLEOZBYTYLUVIEYTUVIYIUUBPZEUUBPZEYTDYIUUBUVHWBYTCUUBPZUVMMRUVMMZUVLUVMYTU
-      VNRUVMYTUUGUVNRNZUUTYTYGCYFWCZUUGUVPWDUUHYFACWEZYFUUBCWFTVOWGCEUUBWHUVOUV
-      MRMUVMRUVMWIUVMXDWJWKYTUUEEUUBWCZUVMENUUSUUBAEWEUUBEWLTWNWOYTUUJYHUVKBNUU
-      MUUNUUOUVKYLUUQOBYLEUUQGWPYLBSAWQWRULWSWTYTYQYIYFPZCYFPZCYTDYIYFUVHWBYTUW
-      AEYFPZMUWARMZUVTUWAYTUWBRUWAYTUUBYFUEZRNZUWBRNZYTUWDUUFRUUBYFXAUUTWRYTUUK
-      UVSUWEUWFWDUURUUBUUIEWEUUBYFEWFTVOXBCEYFWHUWCUWAUWAXDXEWKYTYGUVQUWACNUUHU
-      VRYFCWLTXCXFYEYSUDZYGYHYJUWGYGYFAYQLZUWGYNYFYMXGUWHYEYNYPYRUFZJFXHYMAYFDX
-      OXIUWGYFACYQYEYNYPYRVPZVQVRUWGYOBAYEYNYPYRUIZUWGYMAYLDUWIUWGYLJVBOZIYLYMI
-      ZUWGYLSUWLYEUUJYSUULUHXJVIJYLXKXPZXLXMUWGYIYQUVIMZDYMPZDUWGCYQEUVIUWJUWGU
-      VIUUQEUWGUVIYLYOUQZQZUUQUWGDYMWCZUWMUVIUWRNUWGYNUWSUWIYMADWEZXPUWNYMYLDXN
-      ULUWGYPUWRUUQNUWKYPUWQUUPYOBYLXQXRXPWSGXSXTUWGUWPDUUCPUWOUWGYMUUCDUWGUVAU
-      VDUVEVJUWGFHUVCYEYSVCUVFVIUVGVLYADYFUUBYBYCUWGYNUWSUWPDNUWIUWTYMDWLTXCXFY
-      D $.
+      ( cn0 wcel c1 co wf cun wceq cfv cres csn cn c0 3syl cfz w3a caddc simpr1
+      nn0p1nn adantr simpr2 cop fsng mpbiri syl2anc snssd fssd cin fzp1disj a1i
+      wa fun2d cz cmin cuz simpl cc0 nn0uz 1m1e0 fveq2i eqtr4i syl6eleq sylancr
+      1z fzsuc2 eqcomd feq2d mpbid simpr3 feq1d mpbird ovex fvres ax-mp reseq1d
+      snid wfn wb ffn fnresdisj uneq1d resundir uncom un0 eqtr2i 3eqtr4g 3eqtrd
+      fnresdm fveq1d fveq1i fvsng syl5eq eqtrd syl5eqr incom uneq2d eqcomi 3jca
+      3eqtrrd wss fzssp1 fssres sylancl nnuz eluzfz2 syl ffvelrnd fnressn opeq2
+      eqeltrrd sneqd syl6reqr uneq12d reseq2d resundi syl6req impbida ) FHIZJFU
+      AKZACLZBAIZDCEMZNZUBZJFJUCKZUAKZADLZYKDOZBNZCDYEPZNZUBZYDYJUQZYMYOYQYSYMY
+      LAYHLZYSYEYKQZMZAYHLYTYSYEUUAACEYDYFYGYIUDZYSUUABQZAEYSYKRIZYGUUAUUDELZYD
+      UUEYJFUEZUFZYDYFYGYIUGZUUEYGUQZUUFEYKBUHZQZNGYKBRAEUIUJUKZYSBAUUIULUMZYEU
+      UAUNZSNZYSJFUOUPZURYSUUBYLAYHYSYLUUBYSJUSIZFJJUTKZVAOZIZYLUUBNZVJYSFHUUTY
+      DYJVBHVCVAOUUTVDUUSVCVAVEVFVGZVHJFVKZVIVLVMVNYSYLADYHYDYFYGYIVOZVPVQYSYNY
+      KDUUAPZOZBYKUUAIUVGYNNYKFJUCVRWBYKUUADVSVTYSUVGYKEOZBYSYKUVFEYSUVFYHUUAPZ
+      EUUAPZEYSDYHUUAUVEWAYSCUUAPZUVJMSUVJMZUVIUVJYSUVKSUVJYSUUPUVKSNZUUQYSYFCY
+      EWCZUUPUVMWDUUCYEACWEZYEUUACWFTVNWGCEUUAWHUVLUVJSMUVJSUVJWIUVJWJWKWLYSUUA
+      AELEUUAWCZUVJENUUNUUAAEWEUUAEWNTWMWOYSUUEYGUVHBNUUHUUIUUJUVHYKUULOBYKEUUL
+      GWPYKBRAWQWRUKWSWTYSYPYHYEPZCYEPZCYSDYHYEUVEWAYSUVREYEPZMUVRSMZUVQUVRYSUV
+      SSUVRYSUUAYEUNZSNZUVSSNZYSUWAUUOSUUAYEXAUUQWRYSUUFUVPUWBUWCWDUUMUUAUUDEWE
+      UUAYEEWFTVNXBCEYEWHUVTUVRUVRWJXCWLYSYFUVNUVRCNUUCUVOYECWNTXEXDYDYRUQZYFYG
+      YIUWDYFYEAYPLZUWDYMYEYLXFUWEYDYMYOYQUDZJFXGYLAYEDXHXIUWDYEACYPYDYMYOYQVOZ
+      VPVQUWDYNBAYDYMYOYQUGZUWDYLAYKDUWFUWDYKJVAOZIYKYLIZUWDYKRUWIYDUUEYRUUGUFX
+      JVHJYKXKXLZXMXPUWDYHYPUVFMZDYLPZDUWDCYPEUVFUWGUWDUVFUULEUWDUVFYKYNUHZQZUU
+      LUWDDYLWCZUWJUVFUWONUWDYMUWPUWFYLADWEZXLUWKYLYKDXNUKUWDYOUWOUULNUWHYOUWNU
+      UKYNBYKXOXQXLWSGXRXSUWDUWMDUUBPUWLUWDYLUUBDUWDUURUVAUVBVJUWDFHUUTYDYRVBUV
+      CVHUVDVIXTDYEUUAYAYBUWDYMUWPUWMDNUWFUWQYLDWNTXEXDYC $.
   $}
 
   ${
@@ -134651,26 +134648,26 @@ subset of a (possibly extended) finite sequence of integers.  (Contributed
                               ( K e. ( M ... ( N - 1 ) ) \/ K = N ) ) ) $=
     ( cuz wcel wceq cfz co c1 wo wb wa eleq2d adantl c0 clt wbr cz adantr mpbid
     cfv cmin wi oveq1 elfz1eq syl6bir olc syl6 noel eluzelz ltm1d breq2 eluzel2
-    zred 1zzd zsubcld syl2anc mtbiri pm2.21d eluzfz2 ad2antrr eleq1 mpbird jaod
-    fzn ex impbid caddc elfzp1 cc zcnd npcan1 oveq2d eqeq2d orbi2d 3bitr3d uzm1
-    syl mpjaodan ) CBDUAZEZCBFZABCGHZEZABCIUBHZGHZEZACFZJZKWEVTEZWAWBLZWDWIWBWD
-    WIUCWAWBWDWHWIWBWDACCGHZEWHWBWLWCACBCGUDMACUEUFWHWGUGUHNWKWGWDWHWKWGWDWKWGA
-    OEAUIWKWFOAWKWEBPQZWFOFZWKWECPQZWMWKCWKCWACREZWBBCUJZSZUNUKWBWOWMKWACBWEPUL
-    NTWKBREZWEREWMWNKWAWSWBBCUMSWKCIWRWKUOUPBWEVEUQTMURUSWKWHWDWKWHLWDCWCEZWAWT
-    WBWHBCUTVAWHWDWTKWKACWCVBNVCVFVDVGWAWJLZABWEIVHHZGHZEZWGAXBFZJZWDWIWJXDXFKW
-    AABWEVINXAXCWCAXAXBCBGXACVJEXBCFXACWAWPWJWQSVKCVLVRZVMMXAXEWHWGXAXBCAXGVNVO
-    VPBCVQVS $.
+    zred 1zzd zsubcld fzn syl2an2r mtbiri pm2.21d eluzfz2 ad2antrr eleq1 mpbird
+    ex jaod impbid caddc elfzp1 cc zcnd npcan1 syl oveq2d eqeq2d orbi2d 3bitr3d
+    uzm1 mpjaodan ) CBDUAZEZCBFZABCGHZEZABCIUBHZGHZEZACFZJZKWEVTEZWAWBLZWDWIWBW
+    DWIUCWAWBWDWHWIWBWDACCGHZEWHWBWLWCACBCGUDMACUEUFWHWGUGUHNWKWGWDWHWKWGWDWKWG
+    AOEAUIWKWFOAWKWEBPQZWFOFZWKWECPQZWMWKCWKCWACREZWBBCUJZSZUNUKWBWOWMKWACBWEPU
+    LNTWABREWBWEREWMWNKBCUMWKCIWRWKUOUPBWEUQURTMUSUTWKWHWDWKWHLWDCWCEZWAWSWBWHB
+    CVAVBWHWDWSKWKACWCVCNVDVEVFVGWAWJLZABWEIVHHZGHZEZWGAXAFZJZWDWIWJXCXEKWAABWE
+    VINWTXBWCAWTXACBGWTCVJEXACFWTCWAWPWJWQSVKCVLVMZVNMWTXDWHWGWTXACAXFVOVPVQBCV
+    RVS $.
 
   $( No finite set of sequential integers equals an upper set of integers.
      (Contributed by NM, 11-Dec-2005.) $)
   fzneuz $p |- ( ( N e. ( ZZ>= ` M ) /\ K e. ZZ )
                -> -. ( M ... N ) = ( ZZ>= ` K ) ) $=
-    ( cuz cfv wcel cz wa cfz co wceq wn c1 caddc peano2uz adantl wbr cr nelneq2
-    ad2antrr cle eluzelre clt wb peano2re ltnle mpdan mpbid syl elfzle2 syl2anc
-    ltp1 nsyl eqcom sylnib eluzfz2 sylancom pm2.61dan ) CBDEFZAGFZHZCADEZFZBCIJ
-    ZVBKZLZVAVCHZVBVDKZVEVGCMNJZVBFZVIVDFZLZVHLVCVJVAACOPUSVLUTVCUSVICUAQZVKUSC
-    RFZVMLZBCUBVNCVIUCQZVOCULVNVIRFVPVOUDCUECVIUFUGUHUIVIBCUJUMTVIVBVDSUKVBVDUN
-    UOVAVCLZCVDFZVFUSVRUTVQBCUPTCVDVBSUQUR $.
+    ( cuz cfv wcel cz wa cfz co wceq wn caddc peano2uz cle wbr ad2antrr nelneq2
+    c1 cr eluzelre clt ltp1 peano2re ltnle mpdan mpbid syl elfzle2 nsyl syl2an2
+    wb eqcom sylnib eluzfz2 sylancom pm2.61dan ) CBDEFZAGFZHZCADEZFZBCIJZVAKZLZ
+    UTVBHVAVCKZVDVBCSMJZVAFUTVGVCFZLZVFLACNURVIUSVBURVGCOPZVHURCTFZVJLZBCUAVKCV
+    GUBPZVLCUCVKVGTFVMVLULCUDCVGUEUFUGUHVGBCUIUJQVGVAVCRUKVAVCUMUNUTVBLZCVCFZVE
+    URVOUSVNBCUOQCVCVARUPUQ $.
 
   $( Disjointness of the upper integers and a finite sequence.  (Contributed by
      Mario Carneiro, 30-Jun-2013.)  (Revised by Mario Carneiro,
@@ -134706,14 +134703,14 @@ subset of a (possibly extended) finite sequence of integers.  (Contributed
      -> ( A. j e. ( M ... N ) ph
          <-> A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph ) ) $=
       ( cz wcel cfz co wral cv cmin wsbc wi wa wb elfzelz syl wceq simpr sylan2
-      w3a fzrev anassrs mpbid rspsbc ex 3impa com23 ralrimdv nfcv nfsbc1v nfral
-      nfv fzrev2i oveq2 sbceq1d rspcv cc zcn zcnd syl2an eqcomd sbceq1a sylibrd
-      nncan ralrimd 3ad2ant3 impbid ) EGHZFGHZDGHZUCZABEFIJZKZABDCLZMJZNZCDFMJZ
-      DEMJZIJZKZVNVPVSCWBVNVQWBHZVPVSVKVLVMWDVPVSOZOVKVLPZVMPZWDWEWGWDPZVRVOHZW
-      EWHWDWIWGWDUAWDWGVQGHZWDWIQZVQVTWARWFVMWJWKDVQEFUDUEUBUFABVRVOUGSUHUIUJUK
-      VMVKWCVPOVLVMWCABVOVMBUOVSBCWBBWBULABVRUMUNVMBLZVOHZWCAVMWMWCAOVMWMPZWCAB
-      DDWLMJZMJZNZAWNWOWBHWCWQODWLEFUPVSWQCWOWBVQWOTABVRWPVQWODMUQURUSSWNWLWPTA
-      WQQWNWPWLVMDUTHWLUTHWPWLTWMDVAWMWLWLEFRVBDWLVGVCVDABWPVESVFUHUJVHVIVJ $.
+      w3a fzrev anassrs mpbid ex3 com23 ralrimdv nfv nfcv nfsbc1v nfral fzrev2i
+      rspsbc oveq2 sbceq1d rspcv cc zcnd nncan syl2an eqcomd sbceq1a sylibrd ex
+      zcn ralrimd 3ad2ant3 impbid ) EGHZFGHZDGHZUCZABEFIJZKZABDCLZMJZNZCDFMJZDE
+      MJZIJZKZVNVPVSCWBVNVQWBHZVPVSVKVLVMWDVPVSOZVKVLPZVMPZWDPZVRVOHZWEWHWDWIWG
+      WDUAWDWGVQGHZWDWIQZVQVTWARWFVMWJWKDVQEFUDUEUBUFABVRVOUOSUGUHUIVMVKWCVPOVL
+      VMWCABVOVMBUJVSBCWBBWBUKABVRULUMVMBLZVOHZWCAVMWMWCAOVMWMPZWCABDDWLMJZMJZN
+      ZAWNWOWBHWCWQODWLEFUNVSWQCWOWBVQWOTABVRWPVQWODMUPUQURSWNWLWPTAWQQWNWPWLVM
+      DUSHWLUSHWPWLTWMDVGWMWLWLEFRUTDWLVAVBVCABWPVDSVEVFUHVHVIVJ $.
 
     $( Reversal of scanning order inside of a quantification over a finite set
        of sequential integers.  (Contributed by NM, 25-Nov-2005.) $)
@@ -134845,9 +134842,9 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
      by OpenAI, 25-Mar-2020.) $)
   elfz0add $p |- ( ( A e. NN0 /\ B e. NN0 )
                    -> ( N e. ( 0 ... A ) -> N e. ( 0 ... ( A + B ) ) ) ) $=
-    ( cn0 wcel wa cc0 cfz co caddc cuz cfv wss cz nn0z uzid syl anim12i uzaddcl
-    id fzss2 sseld ) ADEZBDEZFZGAHIZGABJIZHIZCUEUGAKLZEZUFUHMUEAUIEZUDFUJUCUKUD
-    UDUCANEUKAOAPQUDTRBAASQAGUGUAQUB $.
+    ( cn0 wcel wa cc0 cfz co caddc cuz cfv wss cz nn0z uzid uzaddcl sylan fzss2
+    syl sseld ) ADEZBDEZFZGAHIZGABJIZHIZCUDUFAKLZEZUEUGMUBAUHEZUCUIUBANEUJAOAPT
+    BAAQRAGUFSTUA $.
 
   $( An integer range from 0 to 0 is a singleton.  (Contributed by AV,
      18-Apr-2021.) $)
@@ -135063,13 +135060,13 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
        distinct from any later members.  (Contributed by AV, 8-Nov-2019.) $)
     nn0disj $p |- ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) $=
       ( vk cc0 cfz co c1 caddc cuz cfv c0 wceq wcel clt wbr cle syl cz mpbid wn
-      zred cin wss cv cmin elin simprbi eluzel2 eluzelz zlem1lt syl2anc simplbi
-      eluzle wb elfzle2 elfzel2 adantr sylbi lenltd pncan1 eqcomd breq1d notbid
+      zred cin wss cv elinel2 eluzle wb eluzel2 eluzelz zlem1lt syl2anc elinel1
+      cmin elfzle2 elin elfzel2 adantr sylbi lenltd pncan1 eqcomd breq1d notbid
       wa cc zcnd bitrd pm2.21dd ssriv ss0 ax-mp ) CADEZAFGEZHIZUAZJUBVNJKBVNJBU
-      CZVNLZVLFUDEZVOMNZVOJLVPVLVOONZVRVPVOVMLZVSVPVOVKLZVTVOVKVMUEZUFZVLVOULPV
-      PVLQLZVOQLZVSVRUMVPVTWDWCVLVOUGPVPVTWEWCVLVOUHPZVLVOUIUJRVPVOAONZVRSZVPWA
-      WGVPWAVTWBUKVOCAUNPVPWGAVOMNZSWHVPVOAVPVOWFTVPAVPWAVTVCAQLZWBWAWJVTVOCAUO
-      UPUQZTURVPWIVRVPAVQVOMVPVQAVPAVDLVQAKVPAWKVEAUSPUTVAVBVFRVGVHVNVIVJ $.
+      CZVNLZVLFULEZVOMNZVOJLVPVLVOONZVRVPVOVMLZVSVOVKVMUDZVLVOUEPVPVLQLZVOQLZVS
+      VRUFVPVTWBWAVLVOUGPVPVTWCWAVLVOUHPZVLVOUIUJRVPVOAONZVRSZVPVOVKLZWEVOVKVMU
+      KVOCAUMPVPWEAVOMNZSWFVPVOAVPVOWDTVPAVPWGVTVCAQLZVOVKVMUNWGWIVTVOCAUOUPUQZ
+      TURVPWHVRVPAVQVOMVPVQAVPAVDLVQAKVPAWJVEAUSPUTVAVBVFRVGVHVNVIVJ $.
   $}
 
   $( A finite set of sequential nonnegative integers is the union of the
@@ -135107,22 +135104,20 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
                     -> E. a e. V E. b e. V E. c e. V E. d e. V
                        ( ( ( P ` 0 ) = a /\ ( P ` 1 ) = b )
                       /\ ( ( P ` 2 ) = c /\ ( P ` 3 ) = d ) ) ) $=
-      ( c3 cuz cfv wcel cc0 wa cv wceq wrex c1 c2 rexbii bitri cfz co simpr cn0
-      wf 0nn0 elnn0uz mpbi 3nn0 uzss ax-mp sseli eluzfz sylancr adantr ffvelrnd
-      wss risset eqcom sylib 1eluzge0 cz cle 1z 3z 1le3 eluz2 mpbir3an 2eluzge0
-      wbr jca uzuzle23 mpan r19.42v anbi2i 2rexbii r19.41v anbi1i 3bitri sylibr
-      jca32 ) BHIJZKZLBUAUBZCAUEZMZLAJZDNZOZDCPZQAJZENZOZECPZMZRAJZFNZOZFCPZHAJ
-      ZGNZOZGCPZMZMZWIWMMZWRXBMZMGCPZFCPZECPDCPZWFWOWSXCWFWJWNWFWGCKZWJWFWDCLAW
-      CWEUCZWCLWDKZWEWCLLIJZKZBXNKXMLUDKXOUFLUGUHWBXNBHXNKZWBXNUQHUDKXPUIHUGUHZ
-      LHUJUKULLLBUMUNUOUPXKWHWGOZDCPWJDWGCURXRWIDCWHWGUSSTUTWFWKCKZWNWFWDCQAXLW
-      CQWDKZWEWCQXNKBQIJZKXTVAWBYABHYAKZWBYAUQYBQVBKHVBKQHVCVJVDVEVFQHVGVHQHUJU
-      KULQLBUMUNUOUPXSWLWKOZECPWNEWKCURYCWMECWLWKUSSTUTVKWFWPCKZWSWFWDCRAXLWCRW
-      DKZWEWCRXNKBRIJKYEVIBVLRLBUMUNUOUPYDWQWPOZFCPWSFWPCURYFWRFCWQWPUSSTUTWFWT
-      CKZXCWFWDCHAXLWCHWDKZWEXPWCYHXQHLBUMVMUOUPYGXAWTOZGCPXCGWTCURYIXBGCXAWTUS
-      STUTWAXJXFWRXCMZMZFCPZECPDCPXFXDMZECPZDCPZXEXIYLDECCXHYKFCXHXFXGGCPZMYKXF
-      XGGCVNYPYJXFWRXBGCVNVOTSVPYLYMDECCYLXFYJFCPZMYMXFYJFCVNYQXDXFWRXCFCVQVOTV
-      PYOWIWNMZXDMZDCPYRDCPZXDMXEYNYSDCYNXFECPZXDMYSXFXDECVQUUAYRXDWIWMECVNVRTS
-      YRXDDCVQYTWOXDWIWNDCVQVRVSVSVT $.
+      ( c3 cuz cfv wcel cc0 wa cv wceq wrex c1 c2 eluzfz adantr cfz co wf simpr
+      cn0 0nn0 elnn0uz mpbi wss 3nn0 uzss ax-mp sseli sylancr ffvelrnd 1eluzge0
+      clel5 sylib cz cle wbr 1z 1le3 eluz2 mpbir3an jca 2eluzge0 uzuzle23 jca32
+      3z mpan r19.42v anbi2i bitri rexbii 2rexbii r19.41v anbi1i 3bitri sylibr
+      ) BHIJZKZLBUAUBZCAUCZMZLAJZDNOZDCPZQAJZENOZECPZMZRAJZFNOZFCPZHAJZGNOZGCPZ
+      MZMZWGWJMZWNWQMZMGCPZFCPZECPDCPZWEWLWOWRWEWHWKWEWFCKWHWEWCCLAWBWDUDZWBLWC
+      KZWDWBLLIJZKZBXHKXGLUEKXIUFLUGUHWAXHBHXHKZWAXHUIHUEKXJUJHUGUHZLHUKULUMLLB
+      SUNTUODCWFUQURWEWICKWKWEWCCQAXFWBQWCKZWDWBQXHKBQIJZKXLUPWAXMBHXMKZWAXMUIX
+      NQUSKHUSKQHUTVAVBVJVCQHVDVEQHUKULUMQLBSUNTUOECWIUQURVFWEWMCKWOWEWCCRAXFWB
+      RWCKZWDWBRXHKBRIJKXOVGBVHRLBSUNTUOFCWMUQURWEWPCKWRWEWCCHAXFWBHWCKZWDXJWBX
+      PXKHLBSVKTUOGCWPUQURVIXEXAWNWRMZMZFCPZECPDCPXAWSMZECPZDCPZWTXDXSDECCXCXRF
+      CXCXAXBGCPZMXRXAXBGCVLYCXQXAWNWQGCVLVMVNVOVPXSXTDECCXSXAXQFCPZMXTXAXQFCVL
+      YDWSXAWNWRFCVQVMVNVPYBWGWKMZWSMZDCPYEDCPZWSMWTYAYFDCYAXAECPZWSMYFXAWSECVQ
+      YHYEWSWGWJECVLVRVNVOYEWSDCVQYGWLWSWGWKDCVQVRVSVSVT $.
   $}
 
   ${
@@ -135214,10 +135209,9 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
     $( Functionality of the half-open integer set function.  (Contributed by
        Stefan O'Rear, 14-Aug-2015.) $)
     fzof $p |- ..^ : ( ZZ X. ZZ ) --> ~P ZZ $=
-      ( vm vn cv c1 cmin co cfz cz cpw wcel wral cxp cfzo wf wss cuz cfv fzssuz
-      uzssz sstri ovex elpw mpbir rgen2w df-fzo fmpt2 mpbi ) ACZBCDEFZGFZHIZJZB
-      HKAHKHHLUKMNULABHHULUJHOUJUHPQHUHUIRUHSTUJHUHUIGUAUBUCUDABHHUJUKMABUEUFUG
-      $.
+      ( vm vn cv c1 cmin co cfz cz cpw wcel wral cxp cfzo fzssz ovex elpw mpbir
+      wf wss rgen2w df-fzo fmpt2 mpbi ) ACZBCDEFZGFZHIZJZBHKAHKHHLUGMRUHABHHUHU
+      FHSUDUENUFHUDUEGOPQTABHHUFUGMABUAUBUC $.
 
     $( Reverse closure for half-open integer sets.  (Contributed by Stefan
        O'Rear, 14-Aug-2015.) $)
@@ -135456,12 +135450,12 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
   fzospliti $p |- ( ( A e. ( B ..^ C ) /\ D e. ZZ ) ->
       ( A e. ( B ..^ D ) \/ A e. ( D ..^ C ) ) ) $=
     ( cfzo co wcel cz wa wo cle wbr clt cr zre adantr a1d wb elfzo syl3anc zred
-    adantl elfzoelz lelttric syl2anc orcomd elfzole1 ancrd elfzolt2 orim12d mpd
-    ancld elfzoel1 simpr elfzoel2 orbi12d mpbird ) ABCEFGZDHGZIZABDEFGZADCEFGZJ
-    BAKLZADMLZIZDAKLZACMLZIZJZUTVDVFJVIUTVFVDUTDNGZANGVFVDJUSVJURDOUBUTAURAHGZU
-    SABCUCPZUADAUDUEUFUTVDVEVFVHUTVDVCUTVCVDURVCUSABCUGPQUHUTVFVGUTVGVFURVGUSAB
-    CUIPQULUJUKUTVAVEVBVHUTVKBHGZUSVAVERVLURVMUSABCUMPURUSUNZABDSTUTVKUSCHGZVBV
-    HRVLVNURVOUSABCUOPADCSTUPUQ $.
+    elfzoelz lelttric syl2an2 orcomd elfzole1 ancrd elfzolt2 ancld mpd elfzoel1
+    orim12d simpr elfzoel2 orbi12d mpbird ) ABCEFGZDHGZIZABDEFGZADCEFGZJBAKLZAD
+    MLZIZDAKLZACMLZIZJZUSVCVEJVHUSVEVCURDNGUQANGVEVCJDOUSAUQAHGZURABCUBPZUADAUC
+    UDUEUSVCVDVEVGUSVCVBUSVBVCUQVBURABCUFPQUGUSVEVFUSVFVEUQVFURABCUHPQUIULUJUSU
+    TVDVAVGUSVIBHGZURUTVDRVJUQVKURABCUKPUQURUMZABDSTUSVIURCHGZVAVGRVJVLUQVMURAB
+    CUNPADCSTUOUP $.
 
   ${
     $d x A $.  $d x B $.  $d x C $.  $d x D $.
@@ -135499,10 +135493,10 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
        starting at the endpoint of the first range.  (Contributed by Mario
        Carneiro, 21-Sep-2016.) $)
     fzouzdisj $p |- ( ( A ..^ B ) i^i ( ZZ>= ` B ) ) = (/) $=
-      ( vx cfzo co cuz cfv cin cv wcel wa clt wbr elfzolt2 adantr cle wn eluzle
-      adantl cz eluzel2 zred cr eluzelre lenltd mpbid pm2.65i elin mtbir nel0 )
-      CABDEZBFGZHZCIZUMJUNUKJZUNULJZKZUQUNBLMZUOURUPUNABNOUQBUNPMZURQUPUSUOBUNR
-      SUQBUNUQBUPBTJUOBUNUASUBUPUNUCJUOBUNUDSUEUFUGUNUKULUHUIUJ $.
+      ( vx cfzo co cuz cfv cin cv wcel wa clt elfzolt2 adantr cz eluzel2 adantl
+      wbr zred cr eluzelre cle eluzle lensymd pm2.65i elin mtbir nel0 ) CABDEZB
+      FGZHZCIZUKJULUIJZULUJJZKZUOULBLRZUMUPUNULABMNUOBULUOBUNBOJUMBULPQSUNULTJU
+      MBULUAQUNBULUBRUMBULUCQUDUEULUIUJUFUGUH $.
   $}
 
   $( A half-open integer range as union of two half-open integer ranges.
@@ -135620,18 +135614,15 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
   $( Translation of one between closed and open integer ranges.  (Contributed
      by Thierry Arnoux, 28-Jul-2020.) $)
   fz1fzo0m1 $p |- ( M e. ( 1 ... N ) -> ( M - 1 ) e. ( 0 ..^ N ) ) $=
-    ( c1 cfz co wcel cmin cc0 cfzo cz 1zzd elfzel2 elfzelz fzsubel syl22anc ibi
-    wb 1m1e0 oveq1i syl6eleq wceq fzoval syl eleqtrrd ) ACBDEFZACGEZHBCGEZDEZHB
-    IEZUEUFCCGEZUGDEZUHUEUFUKFZUECJFZBJFZAJFUMUEULQUEKZACBLZACBMUOACCBNOPUJHUGD
-    RSTUEUNUIUHUAUPHBUBUCUD $.
+    ( c1 cfz co wcel cmin cc0 cfzo elfzmlbm cz wceq elfzel2 fzoval syl eleqtrrd
+    ) ACBDEFZACGEHBCGEDEZHBIEZACBJQBKFSRLACBMHBNOP $.
 
   ${
     $d k N $.
     $( Half-open integer ranges starting with 1 are subsets of NN. (Contributed
        by Thierry Arnoux, 28-Dec-2016.) $)
     fzossnn $p |- ( 1 ..^ N ) C_ NN $=
-      ( vk c1 cfzo co cfz cn fzossfz cv elfznn ssriv sstri ) CADECAFEZGCAHBMGBI
-      AJKL $.
+      ( c1 cfzo co cfz cn fzossfz fz1ssnn sstri ) BACDBAEDFBAGAHI $.
   $}
 
   $( Membership in a half-open integer range based at 1.  (Contributed by
@@ -135810,20 +135801,20 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
     ( cc0 co wcel wi cn0 cle wbr w3a wa clt cz adantr cr nn0re adantl imp caddc
     cfz cmin cfzo elfz2nn0 cn elfzo0 wb nn0z znnsub syl2an simpr simpll syl2anr
     nn0addcl 0red 3jca nn0ge0 anim1i lelttr sylc ex ltletr syl3anc simplbi2 syl
-    elnnz syld exp4b com24 com13 readdcl ltaddsubd exbiri impd anasss syl3anbrc
-    com23 exp53 sylbird 3adant3 com14 3imp sylbi 3adant1 com12 ) CEDUBFGZDEAUBF
-    GZBEDCUCFZUDFGZBCUAFZEAUDFGZHZWGCIGZDIGZCDJKZLZWHWMHCDUEWHWQWMWHWOAIGZDAJKZ
-    LWQWMHZDAUEWRWSWTWOWJWQWRWSMZWLWJBIGZWIUFGZBWINKZLWQXAWLHZHZBWIUGXBXCXDXFWQ
-    XCXDXBXEWNWOXCXDXBXEHHZHWPWNWOMZXCCDNKZXGWNCOGDOGXIXCUHWOCUIDUICDUJUKXHXIXD
-    XBXAWLXHXIMZXDXBMZMZXAMWKIGZAUFGZWKANKZWLXLXMXAXKXBWNXMXJXDXBULWNWOXIUMBCUO
-    UNPXLXAXNXJXAXNHZXKXHXIXPXHXIEDNKZXPXHXIXQXJEQGZCQGZDQGZLZECJKZXIMXQXHYAXIX
-    HXRXSXTXHUPWNXSWOCRPZWOXTWNDRZSZUQPXHYBXIWNYBWOCURPUSECDUTVAVBWOXQXPHWNXAXQ
-    WOXNWRWSXQWOXNHHWRWOXQWSXNWRWOXQWSXNWRWOMZXQWSMZEANKZXNYFXRXTAQGZYGYHHYFUPW
-    OXTWRYDSWRYIWOARZPEDAVCVDWRYHXNHZWOWRAOGZYKAUIXNYLYHAVGVEVFPVHVIVJTVKSVHTPT
-    XLWRWSXOXLWRMZWSMWKQGZXTYILZWKDNKZWSMXOYMYOWSYMYNXTYIXLYNWRXKBQGZXSYNXJXBYQ
-    XDBRZSXHXSXIYCPBCVLUNPXLXTWRXJXTXKXHXTXIYEPPPWRYIXLYJSUQPYMYPWSXLYPWRXJXKYP
-    XHXKYPHXIXHXDXBYPXHXBXDYPXHXBYPXDXHXBMBCDXBYQXHYRSXHXSXBYCPXHXTXBYEPVMVNVRV
-    OPTPUSWKDAVCVAVPWKAUGVQVSVTWAWBWCWDVKWEWDWFWDT $.
+    elnnz exp4b com24 readdcl ltaddsubd exbiri impcomd anasss syl3anbrc sylbird
+    syld com13 exp53 3adant3 com14 3imp sylbi 3adant1 com12 ) CEDUBFGZDEAUBFGZB
+    EDCUCFZUDFGZBCUAFZEAUDFGZHZWFCIGZDIGZCDJKZLZWGWLHCDUEWGWPWLWGWNAIGZDAJKZLWP
+    WLHZDAUEWQWRWSWNWIWPWQWRMZWKWIBIGZWHUFGZBWHNKZLWPWTWKHZHZBWHUGXAXBXCXEWPXBX
+    CXAXDWMWNXBXCXAXDHHZHWOWMWNMZXBCDNKZXFWMCOGDOGXHXBUHWNCUIDUICDUJUKXGXHXCXAW
+    TWKXGXHMZXCXAMZMZWTMWJIGZAUFGZWJANKZWKXKXLWTXJXAWMXLXIXCXAULWMWNXHUMBCUOUNP
+    XKWTXMXIWTXMHZXJXGXHXOXGXHEDNKZXOXGXHXPXIEQGZCQGZDQGZLZECJKZXHMXPXGXTXHXGXQ
+    XRXSXGUPWMXRWNCRPZWNXSWMDRZSZUQPXGYAXHWMYAWNCURPUSECDUTVAVBWNXPXOHWMWTXPWNX
+    MWQWRXPWNXMHHWQWNXPWRXMWQWNXPWRXMWQWNMZXPWRMZEANKZXMYEXQXSAQGZYFYGHYEUPWNXS
+    WQYCSWQYHWNARZPEDAVCVDWQYGXMHZWNWQAOGZYJAUIXMYKYGAVGVEVFPVQVHVITVRSVQTPTXKW
+    QWRXNXKWQMZWRMWJQGZXSYHLZWJDNKZWRMXNYLYNWRYLYMXSYHXKYMWQXJBQGZXRYMXIXAYPXCB
+    RZSXGXRXHYBPBCVJUNPXKXSWQXIXSXJXGXSXHYDPPPWQYHXKYISUQPYLYOWRXKYOWQXIXJYOXGX
+    JYOHXHXGXAXCYOXGXAYOXCXGXAMBCDXAYPXGYQSXGXRXAYBPXGXSXAYDPVKVLVMPTPUSWJDAVCV
+    AVNWJAUGVOVSVPVTWAWBWCVRWDWCWEWCT $.
 
   $( Membership of an integer incremented by one in a half-open range of
      nonnegative integers.  (Contributed by Alexander van der Vekens,
@@ -136003,13 +135994,12 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
   $( A half-open integer range from 0 to 4 is a union of two unordered pairs.
      (Contributed by Alexander van der Vekens, 17-Nov-2017.) $)
   fzo0to42pr $p |- ( 0 ..^ 4 ) = ( { 0 , 1 } u. { 2 , 3 } ) $=
-    ( cc0 c4 cfzo co c2 cun c1 cpr c3 cfz wcel wceq ax-mp caddc cz ax-1cn eqtri
-    cn0 3cn eqcomi cle wbr 2nn0 4nn0 2re 2lt4 ltleii elfz2nn0 mpbir3an fzosplit
-    4re fzo0to2pr cmin 4z fzoval 4cn df-4 addcomi subaddrii df-3 oveq2i 2z fzpr
-    preq2i 3eqtri uneq12i ) ABCDZAECDZEBCDZFZAGHZEIHZFEABJDKZVGVJLVMERKBRKEBUAU
-    BUCUDEBUEUKUFUGEBUHUIABEUJMVHVKVIVLULVIEBGUMDZJDZEEGNDZHZVLBOKVIVOLUNEBUOMV
-    OEVPJDZVQVNVPEJVNIVPBGIUPPSBGINDZBIGNDVSUQIGSPURQTUSUTQVAEOKVRVQLVBEVCMQVPI
-    EIVPUTTVDVEVFQ $.
+    ( cc0 c4 cfzo co c2 cun c1 cpr c3 cfz wcel wceq cn0 cle wbr 2nn0 4nn0 ax-mp
+    cz eqtri 2re 2lt4 ltleii elfz2nn0 mpbir3an fzosplit fzo0to2pr cmin caddc 4z
+    4re fzoval 4m1e3 df-3 oveq2i 2z fzpr 2p1e3 preq2i 3eqtri uneq12i ) ABCDZAEC
+    DZEBCDZFZAGHZEIHZFEABJDKZVBVELVHEMKBMKEBNOPQEBUAUKUBUCEBUDUEABEUFRVCVFVDVGU
+    GVDEBGUHDZJDZEEGUIDZHZVGBSKVDVJLUJEBULRVJEVKJDZVLVIVKEJVIIVKUMUNTUOESKVMVLL
+    UPEUQRTVKIEURUSUTVAT $.
 
   $( A half-open integer range from 1 to 4 is an unordered triple.
      (Contributed by AV, 28-Jul-2021.) $)
@@ -136074,13 +136064,13 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
     ( wcel cz w3a cle wbr cc0 cfzo co wi wa wn cr zre 3adant1 syl3anc letr imp
     cn0 wo wss simpl2 simpl3 wb ltnle syl2an biimpar ssfzo12 adantl 0red adantr
     clt expcomd con3d ex com23 nn0re 3anim123i 3coml syl expdimp impancom ioran
-    anim12d ancom bitri syl6ibr syld con2d con4d ) CUADZAEDZBEDZFZCAGHZBIGHZUBZ
-    ABJKICJKUCZBAGHZLVPVSMWAVTVPWANZVSVTNVPWBMZVTVSWCVTIAGHZBCGHZMZVSNZWCVNVOAB
-    UNHZVTWFLVMVNVOWBUDVMVNVOWBUEVPWHWBVNVOWHWBUFZVMVNAODZBODZWIVOAPZBPZABUGUHQ
-    UIABICUJRWCWFVRNZVQNZMZWGWCWDWNWEWOVPWBWDWNLVPWDWBWNVNVOWDWBWNLZLVMVNVOMZWD
-    WQWRWDMVRWAWRWDVRWALWRVRWDWAWRWKIODWJVRWDMWALVOWKVNWMUKWRULVNWJVOWLUMBIASRU
-    OTUPUQQURTVPWEWBWOVPWEMVQWAVPWEVQWAVPWKCODZWJFZWEVQMWALVOVMVNWTVOWKVMWSVNWJ
-    WMCUSWLUTVABCASVBVCUPVDVFWGWOWNMWPVQVRVEWOWNVGVHVIVJVKVDVLUQ $.
+    anim12d biancomi syl6ibr syld con2d con4d ) CUADZAEDZBEDZFZCAGHZBIGHZUBZABJ
+    KICJKUCZBAGHZLVOVRMVTVSVOVTNZVRVSNVOWAMZVSVRWBVSIAGHZBCGHZMZVRNZWBVMVNABUNH
+    ZVSWELVLVMVNWAUDVLVMVNWAUEVOWGWAVMVNWGWAUFZVLVMAODZBODZWHVNAPZBPZABUGUHQUIA
+    BICUJRWBWEVQNZVPNZMWFWBWCWMWDWNVOWAWCWMLVOWCWAWMVMVNWCWAWMLZLVLVMVNMZWCWOWP
+    WCMVQVTWPWCVQVTLWPVQWCVTWPWJIODWIVQWCMVTLVNWJVMWLUKWPULVMWIVNWKUMBIASRUOTUP
+    UQQURTVOWDWAWNVOWDMVPVTVOWDVPVTVOWJCODZWIFZWDVPMVTLVNVLVMWRVNWJVLWQVMWIWLCU
+    SWKUTVABCASVBVCUPVDVFWFWMWNVPVQVEVGVHVIVJVDVKUQ $.
 
   ${
     $d K x $.  $d L x $.  $d M x $.  $d N x $.
@@ -136091,19 +136081,19 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
                 -> ( ( K ..^ L ) C_ ( M ..^ N ) <-> ( M <_ K /\ L <_ N ) ) ) $=
       ( vx cz wcel wa clt wbr w3a cfzo cle wi adantr cr zre adantl imp com12 co
       wss df-3an biimpri 3adant2 ssfzo12 syl cv cuz elfzo2 eluz2 simprrl simpll
-      cfv letr syl3anc exp31 com23 expdimp impancom com13 3adant3 impcom sylibr
-      simpl2r ad3antlr ltletr ex expcomd adantld syl3anbrc 3adant1 sylbi impbid
-      3jca ssrdv ) AFGZBFGZHZCFGZDFGZHZABIJZKZABLUAZCDLUAZUBZCAMJZBDMJZHZWDVQVR
-      WCKZWGWJNVSWCWKWBWKVSWCHVQVRWCUCUDUEABCDUFUGWDWJWGWDWJHZEWEWFEUHZWEGZWLWM
-      WFGZWNWMAUIUNGZVRWMBIJZKWLWONZWMABUJWPWQWRVRWPWQWRWPVQWMFGZAWMMJZKWQWRNZA
-      WMUKWSWTXAVQWSWTHZWQWLWOXBWQHZWLHZWMCUIUNGZWAWMDIJZWOXDVTWSCWMMJZKZXEXCWL
-      XHXBWLXHNWQWLXBXHWJWDXBXHNZWHWDXINWIWDWHXIVSWBWHXINWCXBWHVSWBHZXHWSWHWTXJ
-      XHNZWSWHWTXKWSXJWHWTHZXHWSXJXLXHWSXJHZXLHVTWSXGXMVTXLWSVSVTWAULOWSXJXLUMX
-      MXLXGXMCPGZAPGZWMPGZXLXGNXJXNWSWBXNVSVTXNWACQORRXJXOWSVSXOWBVQXOVRAQOORWS
-      XPXJWMQZOCAWMUOUPSVOUQURUSUTVAVBTOVCTOSCWMUKVDWLWAXCVTWAVSWCWJVERXCWLXFXB
-      WQWLXFNZWSWQXRNWTWLWQWSXFWDWJWQWSXFNZNZWDWIXTWHWDWQWIXSVSWBWQWIHZXSNWCXJW
-      SYAXFXJWSYAXFNZXJWSHXPBPGZDPGZYBWSXPXJXQRVRYCVQWBWSBQVFXJYDWSWBYDVSWAYDVT
-      DQRROWMBDVGUPVHURVBVIVJSVAOSSWMCDUJVKUQVLVMSUEVMTVPVHVN $.
+      cfv letr syl2an23an 3jca exp31 com23 expdimp impancom com13 impcom sylibr
+      3adant3 simpl2r ad3antlr ltletr syl3anc expcomd adantld syl3anbrc 3adant1
+      ex sylbi ssrdv impbid ) AFGZBFGZHZCFGZDFGZHZABIJZKZABLUAZCDLUAZUBZCAMJZBD
+      MJZHZWEVRVSWDKZWHWKNVTWDWLWCWLVTWDHVRVSWDUCUDUEABCDUFUGWEWKWHWEWKHZEWFWGE
+      UHZWFGZWMWNWGGZWOWNAUIUNGZVSWNBIJZKWMWPNZWNABUJWQWRWSVSWQWRWSWQVRWNFGZAWN
+      MJZKWRWSNZAWNUKWTXAXBVRWTXAHZWRWMWPXCWRHZWMHZWNCUIUNGZWBWNDIJZWPXEWAWTCWN
+      MJZKZXFXDWMXIXCWMXINWRWMXCXIWKWEXCXINZWIWEXJNWJWEWIXJVTWCWIXJNWDXCWIVTWCH
+      ZXIWTWIXAXKXINZWTWIXAXLWTXKWIXAHZXIWTXKXMXIWTXKHZXMHWAWTXHXNWAXMWTVTWAWBU
+      LOWTXKXMUMXNXMXHXKCPGZAPGZWTWNPGZXMXHNWCXOVTWAXOWBCQORVTXPWCVRXPVSAQOOWTX
+      QXKWNQZOCAWNUOUPSUQURUSUTVAVBVETOVCTOSCWNUKVDWMWBXDWAWBVTWDWKVFRXDWMXGXCW
+      RWMXGNZWTWRXSNXAWMWRWTXGWEWKWRWTXGNZNZWEWJYAWIWEWRWJXTVTWCWRWJHZXTNWDXKWT
+      YBXGXKWTYBXGNZXKWTHXQBPGZDPGZYCWTXQXKXRRVSYDVRWCWTBQVGXKYEWTWCYEVTWBYEWAD
+      QRROWNBDVHVIVNUSVEVJVKSVBOSSWNCDUJVLURVMVOSUEVOTVPVNVQ $.
   $}
 
   $( The result of subtracting 1 and an integer of a half-open range of
@@ -136454,28 +136444,28 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
                    /\ Fun `' ( F |` ( 1 ..^ K ) ) /\ ( F ` 0 ) =/= ( F ` K ) )
                       -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/)
                            -> Fun `' F ) ) ) $=
-      ( vx vy vv vw cc0 co cfv wcel wceq wi wa cv wral ex wn imp41 exp41 cfz wf
-      c1 cfzo cres ccnv wfun wne w3a cn0 cpr cima cin wf1 fzo0ss1 fzossfz sstri
-      wss fssres mpan2 biantrud ancom df-f1 bitr4i syl6bb simp-4r dff13 fveqeq2
-      equequ1 imbi12d fveq2 eqeq2d equequ2 fvres eqcomd eqeqan12d biimpd imim1d
-      c0 rspc2va imp 2a1d expcom syl pm2.43a wo ianor eqcom injresinjlem syl6ib
-      syl5bi ancomsd jaoi a1d sylbi pm2.61i ralrimivv adantl com13 com24 impcom
-      sylanbrc biantrurd syl6bbr mpbird syl6bi 3imp com12 ) HBUAIZCAUBZAUCBUDIZ
-      UEZUFUGZHAJBAJUHZUIBUJKZAHBUKULAXKULUMVSLZAUFUGZMZXJXMXNXOXRMZXMXJXNXSMZX
-      JXMXKCXLUNZXJXTMXJXMXMXKCXLUBZNZYAXJYBXMXJXKXIURYBXKHBUDIXIBUOHBUPUQXICXK
-      AUSUTVAYCYBXMNYAXMYBVBXKCXLVCVDVEYAXJXNXOXRYAXJNZXNNXONZXPXQYEXPNZXQXICAU
-      NZYFXJDOZAJZEOZAJZLZYHYJLZMZEXIPDXIPZYGYAXJXNXOXPVFZYDXNXOXPYOXJYAXNXOXPY
-      OMZMMXJXOXNYAYQXJXOXNYAYQMMYAXNXJXONZYQYAYBFOZXLJGOZXLJZLZYSYTLZMZGXKPFXK
-      PZNXNYRYQMMZFGXKCXLVGUUEUUFYBUUEXNYRXPYOUUEXNNYRNXPNYNDEXIXIUUEXNYRXPYHXI
-      KZYJXIKZNZYNMZYHXKKZYJXKKZNZUUEXNYRXPUUJMZMMZMZUUEUUMUUOUUMUUEUUMUUOMZUUM
-      UUENYHXLJZYJXLJZLZYMMZUUQUUDUVAUURUUALZYHYTLZMFGYHYJXKXKYSYHLUUBUVBUUCUVC
-      YSYHUUAXLVHFDGVIVJYTYJLZUVBUUTUVCYMUVDUUAUUSUURYTYJXLVKVLGEDVMVJVTUUMUVAU
-      UOUUMUVANZUUNXNYRUVEYNXPUUIUUMUVAYNUUMYLUUTYMUUMYLUUTUUKUULYIUURYKUUSUUKU
-      URYIYHXKAVNVOUULUUSYKYJXKAVNVOVPVQVRWAWBWBWCWDQWEUUMRUUKRZUULRZWFZUUPUUKU
-      ULWGUVHUUOUUEUVFUUOUVGUVFXNYRXPUUJUVFXNNZYRNXPNZUUHUUGYNUVJUUHUUGNZYNYLYK
-      YILZUVJUVKNZYMYIYKWHUVMUVLYJYHLZYMUVIYRXPUVKUVLUVNMZUVFXNYRXPUVKUVOMMMABC
-      YJYHWIWASYJYHWHWJWKQWLTABCYHYJWIWMWNWOWPSWQTWRWOWSQWTXASDEXICAVGXBYFXQXJX
-      QNYGYFXJXQYPXCXICAVCXDXEQTXFWEXGXH $.
+      ( vx vy vv vw cc0 co cfv wcel wceq wi wa cv weq wral ex wn imp41 cfz cfzo
+      wf c1 cres ccnv wfun wne w3a cn0 cpr cin c0 wf1 wss fzo0ss1 fzossfz sstri
+      cima fssres mpan2 ancom df-f1 bitr4i syl6bb simp-4r dff13 fveqeq2 equequ1
+      imbi12d fveq2 eqeq2d equequ2 rspc2va fvres eqcomd eqeqan12d biimpd imim1d
+      biantrud imp expcom syl pm2.43a wo ianor eqcom injresinjlem syl6ib syl5bi
+      2a1d ancomsd exp41 jaoi a1d sylbi pm2.61i ralrimivv simplbiim com13 com24
+      impcom sylanbrc biantrurd syl6bbr mpbird syl6bi 3imp com12 ) HBUAIZCAUCZA
+      UDBUBIZUEZUFUGZHAJBAJUHZUIBUJKZAHBUKUSAXLUSULUMLZAUFUGZMZXKXNXOXPXSMZXNXK
+      XOXTMZXKXNXLCXMUNZXKYAMXKXNXNXLCXMUCZNZYBXKYCXNXKXLXJUOYCXLHBUBIXJBUPHBUQ
+      URXJCXLAUTVAVTYDYCXNNYBXNYCVBXLCXMVCVDVEYBXKXOXPXSYBXKNZXONXPNZXQXRYFXQNZ
+      XRXJCAUNZYGXKDOZAJZEOZAJZLZDEPZMZEXJQDXJQZYHYBXKXOXPXQVFZYEXOXPXQYPXKYBXO
+      XPXQYPMZMMXKXPXOYBYRXKXPXOYBYRMMYBXOXKXPNZYRYBYCFOZXMJGOZXMJZLZFGPZMZGXLQ
+      FXLQZXOYSYRMMFGXLCXMVGUUFXOYSXQYPUUFXONYSNXQNYODEXJXJUUFXOYSXQYIXJKZYKXJK
+      ZNZYOMZYIXLKZYKXLKZNZUUFXOYSXQUUJMZMMZMZUUFUUMUUOUUMUUFUUMUUOMZUUMUUFNYIX
+      MJZYKXMJZLZYNMZUUQUUEUVAUURUUBLZDGPZMFGYIYKXLXLFDPUUCUVBUUDUVCYTYIUUBXMVH
+      FDGVIVJGEPZUVBUUTUVCYNUVDUUBUUSUURUUAYKXMVKVLGEDVMVJVNUUMUVAUUOUUMUVANZUU
+      NXOYSUVEYOXQUUIUUMUVAYOUUMYMUUTYNUUMYMUUTUUKUULYJUURYLUUSUUKUURYJYIXLAVOV
+      PUULUUSYLYKXLAVOVPVQVRVSWAWKWKWBWCRWDUUMSUUKSZUULSZWEZUUPUUKUULWFUVHUUOUU
+      FUVFUUOUVGUVFXOYSXQUUJUVFXONZYSNXQNZUUHUUGYOUVJUUHUUGNZYOYMYLYJLZUVJUVKNZ
+      YNYJYLWGUVMUVLEDPZYNUVIYSXQUVKUVLUVNMZUVFXOYSXQUVKUVOMMMABCYKYIWHWATYKYIW
+      GWIWJRWLWMABCYIYKWHWNWOWPWQTWRWMWSWTRXAXBTDEXJCAVGXCYGXRXKXRNYHYGXKXRYQXD
+      XJCAVCXEXFRWMXGWDXHXI $.
   $}
 
   $( The difference between two elements in a half-open range of nonnegative
@@ -136731,15 +136721,14 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
        6-Sep-2014.) $)
     flval3 $p |- ( A e. RR ->
                   ( |_ ` A ) = sup ( { x e. ZZ | x <_ A } , RR , < ) ) $=
-      ( vz vy cr wcel cfl cfv cv cle wbr cz crab csup wral breq1 elrab syl31anc
-      clt wa wceq wss wne wrex ssrab2 zssre sstri a1i flcl flle sylanbrc reflcl
-      c0 ne0d flge biimpd expimpd syl5bi ralrimiv brralrspcev syl2anc suprub wb
-      suprleub mpbird suprcl syl3anc letri3d mpbir2and ) BEFZBGHZAIZBJKZALMZESN
-      ZUAVKVOJKZVOVKJKZVJVNEUBZVNUMUCZCIZDIJKCVNODEUDZVKVNFZVPVRVJVNLEVMALUEUFU
-      GUHZVJVNVKVJVKLFVKBJKZWBBUIBUJVMWDAVKLVLVKBJPQUKZUNZVJVKEFZVTVKJKZCVNOZWA
-      BULZVJWHCVNVTVNFVTLFZVTBJKZTVJWHVMWLAVTLVLVTBJPQVJWKWLWHVJWKTWLWHBVTUOUPU
-      QURUSZDCVTVKJEVNUTVAZWEDCVNVKVBRVJVQWIWMVJVRVSWAWGVQWIVCWCWFWNWJDCCVNVKVD
-      RVEVJVKVOWJVJVRVSWAVOEFWCWFWNDCVNVFVGVHVI $.
+      ( vy vz cr wcel cfl cfv cv cle wbr cz crab clt csup wceq wss breq1 wral
+      wa ssrab2 zssre sstri flcl flle elrabd ne0d wrex reflcl elrab flge biimpd
+      a1i expimpd syl5bi ralrimiv brralrspcev syl2anc suprubd suprleub syl31anc
+      c0 wne wb mpbird suprcld letri3d mpbir2and ) BEFZBGHZAIZBJKZALMZENOZPVJVN
+      JKVNVJJKZVICDVMVJVMEQZVIVMLEVLALUAUBUCUMZVIVMVJVIVLVJBJKAVJLVKVJBJRBUDBUE
+      UFZUGZVIVJEFZDIZVJJKZDVMSZWACIJKDVMSCEUHZBUIZVIWBDVMWAVMFWALFZWABJKZTVIWB
+      VLWGAWALVKWABJRUJVIWFWGWBVIWFTWGWBBWAUKULUNUOUPZCDWAVJJEVMUQURZVRUSVIVOWC
+      WHVIVPVMVBVCWDVTVOWCVDVQVSWIWECDDVMVJUTVAVEVIVJVNWEVICDVMVQVSWIVFVGVH $.
 
     $( A condition equivalent to floor.  (Contributed by NM, 11-Mar-2005.)
        (Revised by Mario Carneiro, 2-Nov-2013.) $)
@@ -136816,11 +136805,11 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
   divfl0 $p |- ( ( A e. NN0 /\ B e. NN )
                  -> ( A < B <-> ( |_ ` ( A / B ) ) = 0 ) ) $=
     ( cn0 wcel cn wa cdiv co cfl cfv cc0 wceq caddc cle wbr c1 clt cc cr wb syl
-    nn0nndivcl recnd addid2 eqcomd fveqeq2d cz flbi2 nn0ge0div biantrurd bicomd
-    0z sylancr crp nn0re nnrp divlt1lt syl2an bitrd 3bitrrd ) ACDZBEDZFZABGHZIJ
-    KLKVDMHZIJKLZKVDNOZVDPQOZFZABQOZVCVDVEKIVCVDRDZVDVELVCVDABUBZUCVKVEVDVDUDUE
-    UAUFVCKUGDVDSDVFVITULVLVDKUHUMVCVIVHVJVCVHVIVCVGVHABUIUJUKVAASDBUNDVHVJTVBA
-    UOBUPABUQURUSUT $.
+    nn0nndivcl recnd addid2 eqcomd fveqeq2d cz 0z flbi2 nn0ge0div biantrurd crp
+    sylancr nn0re nnrp divlt1lt syl2an bitr3d 3bitrrd ) ACDZBEDZFZABGHZIJKLKVCM
+    HZIJKLZKVCNOZVCPQOZFZABQOZVBVCVDKIVBVCRDZVCVDLVBVCABUBZUCVJVDVCVCUDUEUAUFVB
+    KUGDVCSDVEVHTUHVKVCKUIUMVBVGVHVIVBVFVGABUJUKUTASDBULDVGVITVAAUNBUOABUPUQURU
+    S $.
 
   $( An integer can be moved in and out of the floor of a sum.  (Contributed by
      NM, 27-Apr-2005.)  (Proof shortened by Fan Zheng, 16-Jun-2016.) $)
@@ -136925,16 +136914,16 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
                           -> ( ( |_ ` ( A / B ) ) + 1 ) < ( C / B ) ) ) $=
     ( cr wcel co clt wbr cdiv c1 caddc wa syl 3adant3 adantr cmul recn 3ad2ant2
     wb cc crp w3a cmin cfl cfv refldivcl peano2re rerpdivcl ancoms 3adant1 1red
-    cle 3simpa fldivle leadd1dd rpre ltaddsub syl3an2 biimpar 1cnd rpcn adddird
-    3ad2ant1 cc0 wne rpne0 divcan1d wceq mulid2d oveq12d eqtrd 3ad2ant3 breq12d
-    mpbird simp2 ltmul1d lelttrd ex ) ADEZBUAEZCDEZUBZACBUCFGHZABIFZUDUEZJKFZCB
-    IFZGHWBWCLZWFWDJKFZWGWBWFDEZWCVSVTWJWAVSVTLZWEDEZWJABUFZWEUGMNOWBWIDEZWCVSV
-    TWNWAWKWDDEZWNABUHZWDUGZMNOWBWGDEZWCVTWAWRVSWAVTWRCBUHUIUJZOWHWEWDJWBWLWCVS
-    VTWLWAWMNOWBWOWCVSVTWOWAWPNZOWHUKWHWKWEWDULHWBWKWCVSVTWAUMOABUNMUOWHWIWGGHZ
-    WIBPFZWGBPFZGHZWHXDABKFZCGHZWBXFWCVTVSBDEWAXFWCSBUPABCUQURUSWBXDXFSWCWBXBXE
-    XCCGWBXBWDBPFZJBPFZKFXEWBWDJBVSVTWDTEZWAWKWOXIWPWDQMNWBUTVTVSBTEWABVAZRZVBW
-    BXGAXHBKWBABVSVTATEWAAQVCXKVTVSBVDVEWABVFRZVGVTVSXHBVHWAVTBXJVIRVJVKWBCBWAV
-    SCTEVTCQVLXKXLVGVMOVNWBXAXDSWCWBWIWGBWBWOWNWTWQMWSVSVTWAVOVPOVNVQVR $.
+    cle 3simpa fldivle leadd1dd rpre ltaddsub syl3an2 biimpar rpcn 3ad2ant1 cc0
+    1cnd wne rpne0 divcan1d wceq mulid2d oveq12d joinlmuladdmuld breq12d mpbird
+    3ad2ant3 simp2 ltmul1d lelttrd ex ) ADEZBUAEZCDEZUBZACBUCFGHZABIFZUDUEZJKFZ
+    CBIFZGHWAWBLZWEWCJKFZWFWAWEDEZWBVRVSWIVTVRVSLZWDDEZWIABUFZWDUGMNOWAWHDEZWBV
+    RVSWMVTWJWCDEZWMABUHZWCUGZMNOWAWFDEZWBVSVTWQVRVTVSWQCBUHUIUJZOWGWDWCJWAWKWB
+    VRVSWKVTWLNOWAWNWBVRVSWNVTWONZOWGUKWGWJWDWCULHWAWJWBVRVSVTUMOABUNMUOWGWHWFG
+    HZWHBPFZWFBPFZGHZWGXCABKFZCGHZWAXEWBVSVRBDEVTXEWBSBUPABCUQURUSWAXCXESWBWAXA
+    XDXBCGWAWCBJXDVRVSWCTEZVTWJWNXFWOWCQMNVSVRBTEVTBUTZRZWAVCWAWCBPFAJBPFZBKWAA
+    BVRVSATEVTAQVAXHVSVRBVBVDVTBVERZVFVSVRXIBVGVTVSBXGVHRVIVJWACBVTVRCTEVSCQVMX
+    HXJVFVKOVLWAWTXCSWBWAWHWFBWAWNWMWSWPMWRVRVSVTVNVOOVLVPVQ $.
 
   $( The floor of an integer equal to 3 or greater than 4, increased by 1, is
      less than or equal to the half of the integer minus 1.  (Contributed by
@@ -136944,24 +136933,23 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
     ( c3 c4 cdiv co cfl cfv c1 caddc cmin c2 cle wbr c5 wcel a1i cc0 syl6eq syl
     cr wceq cuz 1le1 fvoveq1 clt 3lt4 cn0 cn 3nn0 4nn divfl0 mp2an oveq1d 0p1e1
     wb mpbi oveq1 3m1e2 2div2e1 3brtr4d wo uzp1 2re df-5 oveq1i 4cn ax-1cn 4ne0
-    leidi divdiri dividi eqtri fveq2i 1re 0le1 4pos divge0 mp4an 1lt4 recgt1 cz
-    4re wa 1z rereccli flbi2 mpbir2an 1p1e2 mvrraddi 4d2e2 c6 w3a eluz2 zre wne
-    redivcld flle 3syl adantr flcld zred 3jca leadd1 mpbid div4p1lem1div2 sylan
-    id peano2re peano2rem rehalfcld letr mp2and 3adant1 sylbi 5p1e6 eleq2s jaoi
-    wi ) ABUAZACDEZFGZHIEZAHJEZKDEZLMZANUBGOZXSHHYBYDLHHLMXSUCPXSYBQHIEHXSYAQHI
-    XSYABCDEFGZQABCFDUDBCUEMZYGQUAZUFBUGOCUHOYHYIUOUIUJBCUKULUPRUMUNRXSYDKKDEHX
-    SYCKKDXSYCBHJEKABHJUQURRUMUSRUTYFANUAZANHIEZUBGZOZVAYENAVBYJYEYMYJKKYBYDLKK
-    LMYJKVCVIPYJYBHHIEKYJYAHHIYJYANCDEZFGZHANCFDUDYOHHCDEZIEZFGZHYNYQFYNCHIEZCD
-    EZYQNYSCDVDVEYTCCDEZYPIEYQCHCVFVGVFVHVJUUAHYPICVFVHVKVEVLVLVMYRHUAZQYPLMZYP
-    HUEMZHTOZQHLMCTOZQCUEMZUUCVNVOWBVPHCVQVRHCUEMZUUDVSUUFUUGUUHUUDUOWBVPCVTULU
-    PHWAOYPTOUUBUUCUUDWCUOWDCWBVHWEYPHWFULWGVLRUMWHRYJYDCKDEKYJYCCKDYJYCNHJECAN
-    HJUQNCHVFVGVDWIRUMWJRUTYEAWKUBGZYLAUUIOWKWAOZAWAOZWKALMZWLYEWKAWMUUKUULYEUU
-    JUUKUULWCZYBXTHIEZLMZUUNYDLMZYEUUMYAXTLMZUUOUUKUUQUULUUKATOZXTTOZUUQAWNZUUR
-    ACUURXGUUFUURWBPCQWOUURVHPWPZXTWQWRWSUUMYATOZUUSUUEWLZUUQUUOUOUUKUVCUULUUKU
-    URUVCUUTUURUVBUUSUUEUURYAUURXTUVAWTXAZUVAUUEUURVNPXBSWSYAXTHXCSXDUUKUURUULU
-    UPUUTAXEXFUUMYBTOZUUNTOZYDTOZWLZUUOUUPWCYEXRUUKUVHUULUUKUURUVHUUTUURUVEUVFU
-    VGUURUVBUVEUVDYAXHSUURUUSUVFUVAXTXHSUURYCAXIXJXBSWSYBUUNYDXKSXLXMXNYKWKUBXO
-    VMXPXQSXQ $.
+    leidi divdiri dividi 3eqtri fveq2i 1re 0le1 4re 4pos divge0 mp4an recgt1 cz
+    1lt4 wa 1z rereccli flbi2 mpbir2an eqtri 1p1e2 5m1e4 4d2e2 c6 w3a eluz2 zre
+    id wne redivcld flle 3syl adantr flcld zred 3jca mpbid div4p1lem1div2 sylan
+    leadd1 wi peano2re peano2rem rehalfcld letr mp2and 3adant1 sylbi 5p1e6 jaoi
+    eleq2s ) ABUAZACDEZFGZHIEZAHJEZKDEZLMZANUBGOZXTHHYCYELHHLMXTUCPXTYCQHIEHXTY
+    BQHIXTYBBCDEFGZQABCFDUDBCUEMZYHQUAZUFBUGOCUHOYIYJUOUIUJBCUKULUPRUMUNRXTYEKK
+    DEHXTYDKKDXTYDBHJEKABHJUQURRUMUSRUTYGANUAZANHIEZUBGZOZVAYFNAVBYKYFYNYKKKYCY
+    ELKKLMYKKVCVIPYKYCHHIEKYKYBHHIYKYBNCDEZFGZHANCFDUDYPHHCDEZIEZFGZHYOYRFYOCHI
+    EZCDECCDEZYQIEYRNYTCDVDVECHCVFVGVFVHVJUUAHYQICVFVHVKVEVLVMYSHUAZQYQLMZYQHUE
+    MZHTOZQHLMCTOZQCUEMZUUCVNVOVPVQHCVRVSHCUEMZUUDWBUUFUUGUUHUUDUOVPVQCVTULUPHW
+    AOYQTOUUBUUCUUDWCUOWDCVPVHWEYQHWFULWGWHRUMWIRYKYECKDEKYKYDCKDYKYDNHJECANHJU
+    QWJRUMWKRUTYFAWLUBGZYMAUUIOWLWAOZAWAOZWLALMZWMYFWLAWNUUKUULYFUUJUUKUULWCZYC
+    YAHIEZLMZUUNYELMZYFUUMYBYALMZUUOUUKUUQUULUUKATOZYATOZUUQAWOZUURACUURWPUUFUU
+    RVPPCQWQUURVHPWRZYAWSWTXAUUMYBTOZUUSUUEWMZUUQUUOUOUUKUVCUULUUKUURUVCUUTUURU
+    VBUUSUUEUURYBUURYAUVAXBXCZUVAUUEUURVNPXDSXAYBYAHXHSXEUUKUURUULUUPUUTAXFXGUU
+    MYCTOZUUNTOZYETOZWMZUUOUUPWCYFXIUUKUVHUULUUKUURUVHUUTUURUVEUVFUVGUURUVBUVEU
+    VDYBXJSUURUUSUVFUVAYAXJSUURYDAXKXLXDSXAYCUUNYEXMSXNXOXPYLWLUBXQVMXSXRSXR $.
 
   $( The floor of an integer greater than 1, divided by 4 is less than or equal
      to the half of the integer minus 1.  (Contributed by AV, 5-Jul-2021.)
@@ -137008,17 +136996,17 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
     dfceil2 $p |- |^ = ( x e. RR |->
                          ( iota_ y e. ZZ ( x <_ y /\ y < ( x + 1 ) ) ) ) $=
       ( vz cr cv cneg cmpt cle wbr c1 caddc co clt wa cz crio wcel wb syl wceq
-      cceil cfl cfv df-ceil zre lenegcon2 peano2re anim2i ancoms ltnegcon1 recn
-      1cnd negdid adantr breq1d cmin renegcl neg1rr a1i simpr ltaddsubd subnegd
-      adantl breq2d bitrd 3bitrd anbi12d sylan2 riotabidva negeqd zbtwnre breq2
-      wreu breq1 zriotaneg flval 3eqtr4rd mpteq2ia eqtri ) UAADAEZFZUBUCZFZGADV
-      TBEZHIZWDVTJKLZMIZNZBOPZGAUDADWCWIVTDQZVTCEZFZHIZWLWFMIZNZCOPZFZWKWAHIZWA
-      WKJKLZMIZNZCOPZFWIWCWJWPXBWJWOXACOWKOQWJWKDQZWOXARWKUEWJXCNZWMWRWNWTVTWKU
-      FXDWNWFFZWKMIZWAJFZKLZWKMIZWTXDXCWFDQZNZWNXFRXCWJXKWJXJXCVTUGUHUIWKWFUJSX
-      DXEXHWKMWJXEXHTXCWJVTJVTUKWJULUMUNUOXDXIWAWKXGUPLZMIWTXDWAXGWKWJWADQZXCVT
-      UQZUNXGDQXDURUSWJXCUTVAXDXLWSWAMXCXLWSTWJXCWKJWKUKXCULVBVCVDVEVFVGVHVIVJW
-      JWHBOVMWIWQTBVTVKWHWOBCWDWLTWEWMWGWNWDWLVTHVLWDWLWFMVNVGVOSWJWBXBWJXMWBXB
-      TXNCWAVPSVJVQVRVS $.
+      cfl cfv df-ceil zre lenegcon2 peano2re anim1ci ltnegcon1 recn 1cnd negdid
+      cceil adantr breq1d cmin renegcl neg1rr a1i simpr ltaddsubd adantl breq2d
+      subnegd bitrd 3bitrd anbi12d sylan2 riotabidva negeqd zbtwnre breq2 breq1
+      wreu zriotaneg flval 3eqtr4rd mpteq2ia eqtri ) ULADAEZFZUAUBZFZGADVSBEZHI
+      ZWCVSJKLZMIZNZBOPZGAUCADWBWHVSDQZVSCEZFZHIZWKWEMIZNZCOPZFZWJVTHIZVTWJJKLZ
+      MIZNZCOPZFWHWBWIWOXAWIWNWTCOWJOQWIWJDQZWNWTRWJUDWIXBNZWLWQWMWSVSWJUEXCWMW
+      EFZWJMIZVTJFZKLZWJMIZWSXCXBWEDQZNWMXERWIXIXBVSUFUGWJWEUHSXCXDXGWJMWIXDXGT
+      XBWIVSJVSUIWIUJUKUMUNXCXHVTWJXFUOLZMIWSXCVTXFWJWIVTDQZXBVSUPZUMXFDQXCUQUR
+      WIXBUSUTXCXJWRVTMXBXJWRTWIXBWJJWJUIXBUJVCVAVBVDVEVFVGVHVIWIWGBOVMWHWPTBVS
+      VJWGWNBCWCWKTWDWLWFWMWCWKVSHVKWCWKWEMVLVFVNSWIWAXAWIXKWAXATXLCVTVOSVIVPVQ
+      VR $.
   $}
 
   ${
@@ -137213,26 +137201,26 @@ Finite intervals of nonnegative integers (or "finite sets of sequential
      (Contributed by NM, 16-Aug-2008.) $)
   fldiv $p |- ( ( A e. RR /\ N e. NN )
                   -> ( |_ ` ( ( |_ ` A ) / N ) ) = ( |_ ` ( A / N ) ) ) $=
-    ( cr wcel wa cdiv co cfl caddc wceq cc0 cle wbr c1 clt adantr cc jca adantl
-    recnd cn cfv cmin eqid intfrac2 simp3d oveq1d wne reflcl resubcl mpdan nncn
-    nnne0 divdir syl3anc eqtrd cz flcl intfracq sylan nnre redivcld syl addassd
-    resubcld 3eqtrd fveq2d simp1d fracge0 nngt0 divge0 syl2an addge0d peano2rem
-    nnrecre jca31 simp2d fraclt1 wb 1re ltdiv1 mp3an2 mpbid leltadd sylc ax-1cn
-    npcan sylancl syl12anc dividd 3eqtr3d breqtrd flcld flbi2 syl2anc mpbir2and
-    readdcld eqtr2d ) ACDZBUADZEZABFGZHUBAHUBZBFGZHUBZXDXEUCGZAXCUCGZBFGZIGZIGZ
-    HUBZXEXAXBXJHXAXBXDXHIGZXEXFIGZXHIGXJXAXBXCXGIGZBFGZXLXAAXNBFWSAXNJZWTWSKXG
-    LMZXGNOMZXPAXGXCXCUDXGUDUEUFPUGXAXCQDZXGQDZBQDZBKUHZEZXOXLJWSXSWTWSXCAUIZTP
-    WSXTWTWSXGWSXCCDZXGCDZYDAXCUJUKZTPWTYCWSWTYAYBBULZBUMZRSXCXGBUNUOUPXAXDXMXH
-    IWSXCUQDZWTXDXMJZAURZYJWTEZKXFLMZXFBNUCGZBFGZLMZYKXFXCBXEXEUDXFUDUSZUFUTUGX
-    AXEXFXHXAXEXAXDCDXECDXAXCBWSYEWTYDPWTBCDZWSBVAZSZWTYBWSYISZVBZXDUIVCZTXAXFX
-    AXDXEUUCUUDVEZTXAXHXAXGBWSYFWTYGPUUAUUBVBZTVDVFVGXAXKXEJZKXILMZXINOMZXAXFXH
-    UUEUUFWSYJWTYNYLYMYNYQYKYRVHUTWSYFXQEYSKBOMZEZKXHLMWTWSYFXQYGAVIRWTYSUUJYTB
-    VJRZXGBVKVLVMXAXIYPNBFGZIGZNOXAXFCDZXHCDZEYPCDZUUMCDZEZEYQXHUUMOMZEXIUUNOMX
-    AUUOUUPUUSUUEUUFWTUUSWSWTUUQUURWTYOBWTYSYOCDYTBVNVCZYTYIVBBVORSVPXAYQUUTWSY
-    JWTYQYLYMYNYQYKYRVQUTXAXRUUTWSXRWTAVRPWSYFUUKXRUUTVSZWTYGUULYFNCDUUKUVBVTXG
-    NBWAWBVLWCRXFXHYPUUMWDWEWTUUNNJWSWTYONIGZBFGZBBFGUUNNWTUVCBBFWTYANQDZUVCBJY
-    HWFBNWGWHUGWTYOQDZYAYBUVDUUNJZWTYOUVATYHYIUVFUVEYCUVGWFYONBUNWBWIWTBYHYIWJW
-    KSWLXAXEUQDXICDUUGUUHUUIEVSXAXDUUCWMXAXFXHUUEUUFWQXIXEWNWOWPWR $.
+    ( cr wcel wa cdiv co cfl cfv caddc wceq cc0 cle wbr c1 clt eqid recnd jca
+    cc cmin intfrac2 simp3d adantr oveq1d wne reflcl resubcl mpdan nnne0 divdir
+    cn nncn syl2an3an eqtrd cz flcl intfracq sylan adantl redivcld syl resubcld
+    addassd 3eqtrd fveq2d simp1d fracge0 nngt0 divge0 addge0d peano2rem nnrecre
+    nnre syl2an jca31 simp2d fraclt1 wb ltdiv1 mp3an2 mpbid leltadd sylc ax-1cn
+    1re npcan sylancl syl12anc 3eqtr3d breqtrd flcld readdcld syl2anc mpbir2and
+    dividd flbi2 eqtr2d ) ACDZBULDZEZABFGZHIAHIZBFGZHIZXDXEUAGZAXCUAGZBFGZJGZJG
+    ZHIZXEXAXBXJHXAXBXDXHJGZXEXFJGZXHJGXJXAXBXCXGJGZBFGZXLXAAXNBFWSAXNKZWTWSLXG
+    MNZXGOPNZXPAXGXCXCQXGQUBUCUDUEWSXCTDXGTDWTBTDZBLUFZEZXOXLKWSXCAUGZRWSXGWSXC
+    CDZXGCDZYBAXCUHUIZRWTXSXTBUMZBUJZSXCXGBUKUNUOXAXDXMXHJWSXCUPDZWTXDXMKZAUQZY
+    HWTEZLXFMNZXFBOUAGZBFGZMNZYIXFXCBXEXEQXFQURZUCUSUEXAXEXFXHXAXEXAXDCDXECDXAX
+    CBWSYCWTYBUDWTBCDZWSBVNZUTZWTXTWSYGUTZVAZXDUGVBZRXAXFXAXDXEUUAUUBVCZRXAXHXA
+    XGBWSYDWTYEUDYSYTVAZRVDVEVFXAXKXEKZLXIMNZXIOPNZXAXFXHUUCUUDWSYHWTYLYJYKYLYO
+    YIYPVGUSWSYDXQEYQLBPNZEZLXHMNWTWSYDXQYEAVHSWTYQUUHYRBVISZXGBVJVOVKXAXIYNOBF
+    GZJGZOPXAXFCDZXHCDZEYNCDZUUKCDZEZEYOXHUUKPNZEXIUULPNXAUUMUUNUUQUUCUUDWTUUQW
+    SWTUUOUUPWTYMBWTYQYMCDYRBVLVBZYRYGVABVMSUTVPXAYOUURWSYHWTYOYJYKYLYOYIYPVQUS
+    XAXRUURWSXRWTAVRUDWSYDUUIXRUURVSZWTYEUUJYDOCDUUIUUTWFXGOBVTWAVOWBSXFXHYNUUK
+    WCWDWTUULOKWSWTYMOJGZBFGZBBFGUULOWTUVABBFWTXSOTDZUVABKYFWEBOWGWHUEWTYMTDZXS
+    XTUVBUULKZWTYMUUSRYFYGUVDUVCYAUVEWEYMOBUKWAWIWTBYFYGWPWJUTWKXAXEUPDXICDUUEU
+    UFUUGEVSXAXDUUAWLXAXFXHUUCUUDWMXIXEWQWNWOWR $.
 
   $( Cancellation of an embedded floor of a ratio.  Generalization of Equation
      2.4 in [CormenLeisersonRivest] p. 33 (where ` A ` must be an integer).
@@ -137502,20 +137490,20 @@ The modulo (remainder) operation
      modulo operation.  (Contributed by NM, 2-Jan-2009.) $)
   modmulnn $p |- ( ( N e. NN /\ A e. RR /\ M e. NN ) -> ( ( N x. ( |_ ` A ) )
            mod ( N x. M ) ) <_ ( ( |_ ` ( N x. A ) ) mod ( N x. M ) ) ) $=
-    ( cn wcel cr cfl cfv cmul co cdiv cmin reflcl 3adant3 wa 3adant2 cc0 wne cc
-    wceq w3a cmo cle nnre remulcl syl2an sylan syl nnmulcl nnred nncn nnne0 jca
-    mulne0 redivcld remulcld wbr cn0 nnnn0 flmulnn0 lesub1dd crp modval syl2anc
-    nnrpd fldiv recnd divcan5 syl3an fveq2d 3eqtr4rd 3comr eqtrd oveq2d 3brtr4d
-    recn ) CDEZAFEZBDEZUAZCAGHZIJZCBIJZWBWCKJZGHZIJZLJZCAIJZGHZWFLJZWBWCUBJZWIW
-    CUBJZUCVTWBWIWFVQVRWBFEZVSVQCFEZWAFEWMVRCUDZAMZCWAUEUFNZVQVRWIFEZVSVQVROWHF
-    EZWRVQWNVRWSWOCAUEUGZWHMUHNZVTWCWEVQVSWCFEVRVQVSOZWCCBUIZUJPZVTWDFEWEFEVTWB
-    WCWQXDVQVSWCQRZVRVQCSEZCQRZOZBSEZBQRZOZXEVSVQXFXGCUKCULUMZVSXIXJBUKBULUMZCB
-    UNUFPUOWDMUHUPVQVRWBWIUCUQZVSVQCUREVRXNCUSACUTUGNVAVTWMWCVBEZWKWGTWQVQVSXOV
-    RXBWCXCVEPZWBWCVCVDVTWLWIWCWIWCKJGHZIJZLJZWJVTWRXOWLXSTXAXPWIWCVCVDVTXRWFWI
-    LVTXQWEWCIVTXQWHWCKJZGHZWEVTWSWCDEZXQYATVQVRWSVSWTNVQVSYBVRXCPWHWCVFVDVRVSV
-    QYAWETVRVSVQUAZWABKJZGHZABKJZGHZWEYAVRVSYEYGTVQABVFNYCWDYDGVRWASEVSXKVQXHWD
-    YDTVRWAWPVGXMXLWABCVHVIVJYCXTYFGVRASEVSXKVQXHXTYFTAVPXMXLABCVHVIVJVKVLVMVNV
-    NVMVO $.
+    ( cn wcel cr cfl cfv cmul co cdiv cmin reflcl 3adant3 wa cc0 wceq 3imp3i2an
+    wne cc w3a cmo cle nnre remulcl syl2an sylan syl nnmulcl nnred 3adant2 nncn
+    nnne0 jca mulne0 redivcld remulcld wbr nnnn0 flmulnn0 lesub1dd nnrpd modval
+    cn0 crp fldiv recnd divcan5 syl3an fveq2d recn 3eqtr4rd 3comr eqtrd 3brtr4d
+    oveq2d ) CDEZAFEZBDEZUAZCAGHZIJZCBIJZWBWCKJZGHZIJZLJZCAIJZGHZWFLJZWBWCUBJZW
+    IWCUBJZUCVTWBWIWFVQVRWBFEZVSVQCFEZWAFEWMVRCUDZAMZCWAUEUFNZVQVRWIFEZVSVQVROW
+    HFEZWRVQWNVRWSWOCAUEUGZWHMUHNZVTWCWEVQVSWCFEVRVQVSOZWCCBUIZUJUKZVTWDFEWEFEV
+    TWBWCWQXDVQVSWCPSZVRVQCTEZCPSZOZBTEZBPSZOZXEVSVQXFXGCULCUMUNZVSXIXJBULBUMUN
+    ZCBUOUFUKUPWDMUHUQVQVRWBWIUCURZVSVQCVDEVRXNCUSACUTUGNVAVQVRVSWMWCVEEZWKWGQW
+    QXBWCXCVBZWBWCVCRVTWLWIWCWIWCKJGHZIJZLJZWJVQVRVSWRXOWLXSQXAXPWIWCVCRVTXRWFW
+    ILVTXQWEWCIVTXQWHWCKJZGHZWEVQVRVSWSWCDEXQYAQVQVRWSVSWTNXCWHWCVFRVRVSVQYAWEQ
+    VRVSVQUAZWABKJZGHZABKJZGHZWEYAVRVSYDYFQVQABVFNYBWDYCGVRWATEVSXKVQXHWDYCQVRW
+    AWPVGXMXLWABCVHVIVJYBXTYEGVRATEVSXKVQXHXTYEQAVKXMXLABCVHVIVJVLVMVNVPVPVNVO
+    $.
 
   $( The value of the modulo operation (expressed with sum of denominator and
      nominator).  (Contributed by Alexander van der Vekens, 14-Apr-2018.) $)
@@ -137997,12 +137985,12 @@ The modulo (remainder) operation
     ( cr wcel crp wa cle wbr c2 cmul clt cmin cmo wceq syl adantl adantr sylan2
     co c1 rpre ax-1rid oveq2d oveq1d cz w3a simpl 1zzd 3jca modcyc2 cc0 resubcl
     simpr wb subge0 bicomd caddc 2timesd breq2d ltsubaddd bitr4d anbi12d biimpa
-    jca rpcn modid syl2anc 3eqtr3d ) ACDZBEDZFZBAGHZAIBJSZKHZFZFZABTJSZLSZBMSZA
-    BLSZBMSZABMSZVTVKVSWANVOVKVRVTBMVKVQBALVJVQBNZVIVJBCDZWCBUAZBUBOPUCUDQVPVIV
-    JTUEDZUFZVSWBNVKWGVOVKVIVJWFVIVJUGZVIVJUMZVKUHUIQABTUJOVPVTCDZVJFZUKVTGHZVT
-    BKHZFZWAVTNVKWKVOVKWJVJVJVIWDWJWEABULRWIVDQVKVOWNVKVLWLVNWMVKWLVLVJVIWDWLVL
-    UNWEABUORUPVKVNABBUQSZKHWMVKVMWOAKVJVMWONVIVJBBVEURPUSVKABBWHVJWDVIWEPZWPUT
-    VAVBVCVTBVFVGVH $.
+    jca rpcn modid syl2an2r 3eqtr3d ) ACDZBEDZFZBAGHZAIBJSZKHZFZFZABTJSZLSZBMSZ
+    ABLSZBMSZABMSZVTVKVSWANVOVKVRVTBMVKVQBALVJVQBNZVIVJBCDZWCBUAZBUBOPUCUDQVPVI
+    VJTUEDZUFZVSWBNVKWGVOVKVIVJWFVIVJUGZVIVJUMZVKUHUIQABTUJOVKVTCDZVJFVOUKVTGHZ
+    VTBKHZFZWAVTNVKWJVJVJVIWDWJWEABULRWIVDVKVOWMVKVLWKVNWLVKWKVLVJVIWDWKVLUNWEA
+    BUORUPVKVNABBUQSZKHWLVKVMWNAKVJVMWNNVIVJBBVEURPUSVKABBWHVJWDVIWEPZWOUTVAVBV
+    CVTBVFVGVH $.
 
   $( If a nonnegative integer is less than twice a positive integer, the
      nonnegative integer modulo the positive integer equals the nonnegative
@@ -138010,14 +137998,14 @@ The modulo (remainder) operation
      (Contributed by Alexander van der Vekens, 21-May-2018.) $)
   modifeq2int $p |- ( ( A e. NN0 /\ B e. NN /\ A < ( 2 x. B ) )
                       -> ( A mod B ) = if ( A < B , A , ( A - B ) ) ) $=
-    ( clt wbr cn0 wcel cn c2 cmul co w3a wa cr cle 3adant3 adantl eqcomd adantr
-    wceq eqtrd cmo cmin cif wi crp cc0 nn0re nnrp nn0ge0 3ad2ant1 anim1i ancoms
-    anim12i modid syl2anc iftrue ex wn wb lenlt syl2anr biimpar simpl3 syl12anc
-    nnre 2submod iffalse expcom pm2.61i ) ABCDZAEFZBGFZAHBIJCDZKZABUAJZVJAABUBJ
-    ZUCZSZUDVJVNVRVJVNLZVOAVQVSAMFZBUEFZLZUFANDZVJLZVOASVNWBVJVKVLWBVMVKVTVLWAA
-    UGZBUHUMOZPVNVJWDVNWCVJVKVLWCVMAUIUJUKULABUNUOVJAVQSVNVJVQAVJAVPUPQRTUQVNVJ
-    URZVRVNWGLZVOVPVQWHWBBANDZVMVOVPSVNWBWGWFRVNWIWGVKVLWIWGUSZVMVLBMFVTWJVKBVE
-    WEBAUTVAOVBVKVLVMWGVCABVFVDWHVQVPWGVQVPSVNVJAVPVGPQTVHVI $.
+    ( clt wbr cn0 wcel cn c2 cmul co w3a cmo wceq wa cr cle eqcomd adantr eqtrd
+    3adant3 cmin cif wi crp cc0 nn0re nnrp anim12i nn0ge0 3ad2ant1 anim1i modid
+    ancoms syl2an2 iftrue ex wn wb nnre syl2anr biimpar simpl3 2submod syl12anc
+    lenlt iffalse adantl expcom pm2.61i ) ABCDZAEFZBGFZAHBIJCDZKZABLJZVJAABUAJZ
+    UBZMZUCVJVNVRVJVNNVOAVQVNAOFZBUDFZNZVJUEAPDZVJNZVOAMVKVLWAVMVKVSVLVTAUFZBUG
+    UHTZVNVJWCVNWBVJVKVLWBVMAUIUJUKUMABULUNVJAVQMVNVJVQAVJAVPUOQRSUPVNVJUQZVRVN
+    WFNZVOVPVQWGWABAPDZVMVOVPMVNWAWFWERVNWHWFVKVLWHWFURZVMVLBOFVSWIVKBUSWDBAVEU
+    TTVAVKVLVMWFVBABVCVDWGVQVPWFVQVPMVNVJAVPVFVGQSVHVI $.
 
   $( The sum of an integer modulo a positive integer and another integer minus
      the positive integer equals the sum of the two integers modulo the
@@ -138104,13 +138092,13 @@ The modulo (remainder) operation
     ( crp wcel cr cdiv co cfl cfv cmul cmin cmo cc rpcn 3ad2ant1 3adant1 oveq2d
     wa wceq w3a recn 3ad2ant2 rpre adantl refldivcl remulcld subdid cc0 rpcnne0
     recnd wne 3ad2ant3 divcan5 syl3anc fveq2d rerpdivcl reflcl syl eqtr2d eqtrd
-    mulassd modval remulcl sylan 3adant3 rpmulcl 3adant2 syl2anc 3eqtr4d ) ADEZ
-    BFEZCDEZUAZABCBCGHZIJZKHZLHZKHZABKHZACKHZVTWAGHZIJZKHZLHZABCMHZKHVTWAMHZVNV
-    SVTAVQKHZLHWEVNABVQVKVLANEZVMAOPZVLVKBNEZVMBUBUCZVLVMVQNEVKVLVMSZVQWMCVPVMC
-    FEVLCUDUEBCUFUGUKQUHVNWHWDVTLVNWDWAVPKHWHVNWCVPWAKVNWBVOIVNWKCNEZCUIULSZWIA
-    UIULSZWBVOTWLVMVKWOVLCUJUMVKVLWPVMAUJPBCAUNUOUPRVNACVPWJVMVKWNVLCOUMVLVMVPN
-    EZVKWMVOFEZWQBCUQWRVPVOURUKUSQVBUTRVAVNWFVRAKVLVMWFVRTVKBCVCQRVNVTFEZWADEZW
-    GWETVKVLWSVMVKAFEVLWSAUDABVDVEVFVKVMWTVLACVGVHVTWAVCVIVJ $.
+    mulassd modval remulcl sylan 3adant3 rpmulcl 3imp3i2an 3eqtr4d ) ADEZBFEZCD
+    EZUAZABCBCGHZIJZKHZLHZKHZABKHZACKHZVSVTGHZIJZKHZLHZABCMHZKHVSVTMHZVMVRVSAVP
+    KHZLHWDVMABVPVJVKANEZVLAOPZVKVJBNEZVLBUBUCZVKVLVPNEVJVKVLSZVPWLCVOVLCFEVKCU
+    DUEBCUFUGUKQUHVMWGWCVSLVMWCVTVOKHWGVMWBVOVTKVMWAVNIVMWJCNEZCUIULSZWHAUIULSZ
+    WAVNTWKVLVJWNVKCUJUMVJVKWOVLAUJPBCAUNUOUPRVMACVOWIVLVJWMVKCOUMVKVLVONEZVJWL
+    VNFEZWPBCUQWQVOVNURUKUSQVBUTRVAVMWEVQAKVKVLWEVQTVJBCVCQRVJVKVLVSFEZVTDEWFWD
+    TVJVKWRVLVJAFEVKWRAUDABVDVEVFACVGVSVTVCVHVI $.
 
   $( Distribute the modulo operation over a subtraction.  (Contributed by NM,
      30-Dec-2008.) $)
@@ -138213,45 +138201,44 @@ The modulo (remainder) operation
     ( caddc co clt wbr cc0 wcel wa cr wceq w3a adantr adantl sylbi wne syl cz
     wi cfzo c1 cmo csn cdif crp cle cn0 cn elfzoelz zred nn0re 3ad2ant1 readdcl
     elfzo0 syl2anr nnrp 3ad2ant2 jca sylanb elfzo1 nnnn0 elfzonn0 nn0ge0d simpl
-    nn0addcl modid syl2anc simp2 syl3anbrc zcnd nnne0 addneintr2d addid2 eqcomd
-    cc 0cnd neeqtrrd eldifsn sylanbrc eqeltrd wn cmin cneg cmul elfzoel2 mulm1d
-    oveq2d zaddcl negsub eqtrd oveq1d syl2an ancoms resubcld nnrpd nnre 3adant3
-    simp3 lenltd biimprd subge0d sylibrd syl3anc anim12ci simpr jca31 lt2add wb
-    imp ltsubadd mpbird jctird ex syl5bi 3adant2 impcom neg1z modcyc syl2an23an
-    zsubcld sylbird elnn0z expcom com12 3jca subcl ltned subne0d addsub 3netr4d
-    a1i nncn pm2.61ian ) BADEZCFGZAHCUAEZIZBUBCUAEIZJZYOCUCEZYQAUDUEZIYPYTJZUUA
-    YOUUBUUCYOKIZCUFIZJZHYOUGGZYPJUUAYOLYTUUFYPYRAUHIZCUIIZACFGZMZYSUUFACUOZUUK
-    YSJUUDUUEYSBKIZAKIZUUDUUKYSBBUBCUJZUKZUUHUUIUUNUUJAULZUMBAUNZUPUUKUUEYSUUIU
-    UHUUEUUJCUQURZNUSUTOUUCUUGYPUUCYOYTYOUHIZYPYSBUHIZUUHUUTYRYSBUIIZUUIBCFGZMZ
-    UVACBVAZUVBUUIUVAUVCBVBUMPACVCBAVFUPOZVDYPYTVEZUSYOCVGVHUUCYOYQIZYOAQYOUUBI
-    UUCUUTUUIYPUVHUVFYTUUIYPYRUUIYSYRUUKUUIUULUUHUUIUUJVIZPNZOUVGYOCUOVJUUCYOHA
-    DEZAYTYOUVKQYPYTBHAYSBVPIZYRYSBUUOVKZOZYTVQYRAVPIZYSYRAAHCUJZVKNZYSBHQZYRYS
-    UVDUVRUVEUVBUUIUVRUVCBVLUMPOVMOUUCUVOAUVKLYTUVOYPUVQOUVOUVKAAVNZVORVRYOYQAV
-    SVTWAYPWBZYTJZUUAYOCWCEZUUBUWAUWBUUAUWAUWBYOUBWDZCWEEZDEZCUCEZUUAUWAUWFUWBU
-    WAUWFUWBCUCEZUWBUWAUWEUWBCUCUWAUWEYOCWDZDEZUWBUWAUWDUWHYODUWACYTCVPIZUVTYRU
-    WJYSYRCAHCWFZVKNZOWGWHUWAYOVPIZUWJJZUWIUWBLYTUWNUVTYTUWMUWJYTYOYSBSIZASIZYO
-    SIZYRUUOUVPBAWIZUPZVKUWLUSOYOCWJRWKWLUWAUWBKIZUUEJHUWBUGGZUWBCFGZJZJUWGUWBL
-    UWAUWTUUEUXCYTUWTUVTYTYOCYSYRUUDYSYRJYOYSUWOUWPUWQYRUUOUVPUWRWMUKWNZYRCKIZY
-    SYRCUWKUKNZWOOYTUUEUVTYRUUEYSYRUUKUUEUULUUKCUVIWPPNOYTUVTUXCYRYSUVTUXCTZYRU
-    UKYSUXGTZUULUUHUUJUXHUUIYSUVDUUHUUJJZUXGUVEUXIUVDUXGUXIUVDJZUVTUXAUXBUXJUUM
-    UUNUXEUVTUXATZUVDUUMUXIUVBUUIUUMUVCBWQUMZOUXIUUNUVDUUHUUNUUJUUQNZNUVDUXEUXI
-    UUIUVBUXEUVCCWQZUROZUUMUUNUXEMZUVTCYOUGGZUXAUXPUXQUVTUXPCYOUUMUUNUXEWSZUUMU
-    UNUUDUXEUURWRZWTZXAUXPYOCUXSUXRXBZXCXDUXJUXBYOCCDEFGZUXJUUMUUNJZUXEUXEJZJZU
-    VCUUJJZJZUYBUXJUYCUYDUYFUXIUUNUVDUUMUXMUXLXEUVDUYDUXIUUIUVBUYDUVCUUIUXEUXEU
-    XNUXNUSUROUXIUUJUVDUVCUUHUUJXFUVBUUIUVCWSZXEXGZUYEUYFUYBBACCXHXJZRUXJUUDUXE
-    UXEUXBUYBXIZUVDUUMUUNUUDUXIUXLUXMUURUPUXOUXOYOCCXKZXDXLXMXNXOXPPXJXQXGUWBCV
-    GRWKVOYTUUDUUEUVTUWCSIZUWFUUALUXDYRUUEYSYRUUKUUEUULUUSPNUYMUWAXRYLYOCUWCXSX
-    TWKVOUWAUWBYQIZUWBAQUWBUUBIUWAUWBUHIZUUIUXBUYNUWAUWBSIZUXAUYOYTUYPUVTYTYOCU
-    WSYRCSIYSUWKNYAOYTUVTUXAYTUUMUUNUXEUXKYSUUMYRUUPOYRUUNYSYRAUVPUKNUXFUXPUVTU
-    XQUXAUXTUXPUXAUXQUYAXAYBXDXQUWBYCVTYTUUIUVTUVJOYTUXBUVTYTUXBUYBYTUYGUYBYRYS
-    UYGYRUUKYSUYGTZUULUUHUUJUYQUUIYSUXIUYGYSUVDUXIUYGTUVEUXIUVDUYGUYIYDPYEXPPXJ
-    UYJRYTUUDUXEUXEMZUYKYRYSUYRYRUUKYSUYRTZUULUUHUUIUYSUUJUUHUUIJZYSUYRUYTYSJUU
-    DUXEUXEYSUUMUUNUUDUYTUUPUUHUUNUUIUUQNUURUPUYTUXEYSUUIUXEUUHUXNONZVUAYFXNWRP
-    XJUYLRXLOUWBCUOVJUWABCWCEZADEZUVKUWBAUWAVUBHAYTVUBVPIZUVTYSVUDYRYSUVDVUDUVE
-    UVBUUIVUDUVCUVBUVLUWJVUDUUIBYMCYMBCYGWMWRPOOUWAVQYTUVOUVTUVQOZYTVUBHQZUVTYS
-    VUFYRYSBCUVMYSCBUBCWFVKYSUVDBCQUVEUVDBCUXLUYHYHPYIOOVMUWAUVLUVOUWJMZUWBVUCL
-    YTVUGUVTYTUVLUVOUWJUVNUVQUWLYFOBACYJRUWAUVKAUWAUVOUVKALVUEUVSRVOYKUWBYQAVSV
-    TWAYN $.
+    nn0addcl modid syl12anc simp2 syl3anbrc zcnd 0cnd addneintr2d addid2 eqcomd
+    cc nnne0 neeqtrrd eldifsn sylanbrc eqeltrd cmin cneg elfzoel2 mulm1d oveq2d
+    wn cmul zaddcl negsub eqtrd oveq1d syl2an resubcld nnrpd nnre simp3 3adant3
+    ancoms lenltd biimprd subge0d sylibrd syl3anc anim12ci simpr jca31 ltsubadd
+    lt2add imp wb mpbird jctird ex syl5bi 3adant2 impcom a1i syl2an23an zsubcld
+    neg1z modcyc sylbird elnn0z expcom com12 subcl ltned subne0d addsub 3netr4d
+    3jca nncn pm2.61ian ) BADEZCFGZAHCUAEZIZBUBCUAEIZJZYOCUCEZYQAUDUEZIYPYTJZUU
+    AYOUUBUUCYOKIZCUFIZJZHYOUGGYPUUAYOLYTUUFYPYRAUHIZCUIIZACFGZMZYSUUFACUOZUUJY
+    SJUUDUUEYSBKIZAKIZUUDUUJYSBBUBCUJZUKZUUGUUHUUMUUIAULZUMBAUNZUPUUJUUEYSUUHUU
+    GUUEUUICUQURZNUSUTOUUCYOYTYOUHIZYPYSBUHIZUUGUUSYRYSBUIIZUUHBCFGZMZUUTCBVAZU
+    VAUUHUUTUVBBVBUMPACVCBAVFUPOZVDYPYTVEZYOCVGVHUUCYOYQIZYOAQYOUUBIUUCUUSUUHYP
+    UVGUVEYTUUHYPYRUUHYSYRUUJUUHUUKUUGUUHUUIVIZPNZOUVFYOCUOVJUUCYOHADEZAYTYOUVJ
+    QYPYTBHAYSBVPIZYRYSBUUNVKZOZYTVLYRAVPIZYSYRAAHCUJZVKNZYSBHQZYRYSUVCUVQUVDUV
+    AUUHUVQUVBBVQUMPOVMOUUCUVNAUVJLYTUVNYPUVPOUVNUVJAAVNZVORVRYOYQAVSVTWAYPWGZY
+    TJZUUAYOCWBEZUUBUVTUWAUUAUVTUWAYOUBWCZCWHEZDEZCUCEZUUAUVTUWEUWAUVTUWEUWACUC
+    EZUWAUVTUWDUWACUCUVTUWDYOCWCZDEZUWAUVTUWCUWGYODUVTCYTCVPIZUVSYRUWIYSYRCAHCW
+    DZVKNZOWEWFUVTYOVPIZUWIJZUWHUWALYTUWMUVSYTUWLUWIYTYOYSBSIZASIZYOSIZYRUUNUVO
+    BAWIZUPZVKUWKUSOYOCWJRWKWLUVTUWAKIZUUEJHUWAUGGZUWACFGZJZJUWFUWALUVTUWSUUEUX
+    BYTUWSUVSYTYOCYSYRUUDYSYRJYOYSUWNUWOUWPYRUUNUVOUWQWMUKWSZYRCKIZYSYRCUWJUKNZ
+    WNOYTUUEUVSYRUUEYSYRUUJUUEUUKUUJCUVHWOPNOYTUVSUXBYRYSUVSUXBTZYRUUJYSUXFTZUU
+    KUUGUUIUXGUUHYSUVCUUGUUIJZUXFUVDUXHUVCUXFUXHUVCJZUVSUWTUXAUXIUULUUMUXDUVSUW
+    TTZUVCUULUXHUVAUUHUULUVBBWPUMZOUXHUUMUVCUUGUUMUUIUUPNZNUVCUXDUXHUUHUVAUXDUV
+    BCWPZUROZUULUUMUXDMZUVSCYOUGGZUWTUXOUXPUVSUXOCYOUULUUMUXDWQZUULUUMUUDUXDUUQ
+    WRZWTZXAUXOYOCUXRUXQXBZXCXDUXIUXAYOCCDEFGZUXIUULUUMJZUXDUXDJZJZUVBUUIJZJZUY
+    AUXIUYBUYCUYEUXHUUMUVCUULUXLUXKXEUVCUYCUXHUUHUVAUYCUVBUUHUXDUXDUXMUXMUSUROU
+    XHUUIUVCUVBUUGUUIXFUVAUUHUVBWQZXEXGZUYDUYEUYABACCXIXJZRUXIUUDUXDUXDUXAUYAXK
+    ZUVCUULUUMUUDUXHUXKUXLUUQUPUXNUXNYOCCXHZXDXLXMXNXOXPPXJXQXGUWACVGRWKVOYTUUD
+    UUEUVSUWBSIZUWEUUALUXCYRUUEYSYRUUJUUEUUKUURPNUYLUVTYAXRYOCUWBYBXSWKVOUVTUWA
+    YQIZUWAAQUWAUUBIUVTUWAUHIZUUHUXAUYMUVTUWASIZUWTUYNYTUYOUVSYTYOCUWRYRCSIYSUW
+    JNXTOYTUVSUWTYTUULUUMUXDUXJYSUULYRUUOOYRUUMYSYRAUVOUKNUXEUXOUVSUXPUWTUXSUXO
+    UWTUXPUXTXAYCXDXQUWAYDVTYTUUHUVSUVIOYTUXAUVSYTUXAUYAYTUYFUYAYRYSUYFYRUUJYSU
+    YFTZUUKUUGUUIUYPUUHYSUXHUYFYSUVCUXHUYFTUVDUXHUVCUYFUYHYEPYFXPPXJUYIRYTUUDUX
+    DUXDMZUYJYRYSUYQYRUUJYSUYQTZUUKUUGUUHUYRUUIUUGUUHJZYSUYQUYSYSJUUDUXDUXDYSUU
+    LUUMUUDUYSUUOUUGUUMUUHUUPNUUQUPUYSUXDYSUUHUXDUUGUXMONZUYTYLXNWRPXJUYKRXLOUW
+    ACUOVJUVTBCWBEZADEZUVJUWAAUVTVUAHAYTVUAVPIZUVSYSVUCYRYSUVCVUCUVDUVAUUHVUCUV
+    BUVAUVKUWIVUCUUHBYMCYMBCYGWMWRPOOUVTVLYTUVNUVSUVPOZYTVUAHQZUVSYSVUEYRYSBCUV
+    LYSCBUBCWDVKYSUVCBCQUVDUVCBCUXKUYGYHPYIOOVMUVTUVKUVNUWIMZUWAVUBLYTVUFUVSYTU
+    VKUVNUWIUVMUVPUWKYLOBACYJRUVTUVJAUVTUVNUVJALVUDUVRRVOYKUWAYQAVSVTWAYN $.
 
   $( Two nonnegative integers less than the modulus are equal iff they are
      equal modulo the modulus.  (Contributed by AV, 14-Mar-2021.) $)