add negsid and negnegs

metamath · Feb 3, 2025 · f9df8d3 · f9df8d3
1 parent 33c134c
commit f9df8d3
Showing 1 changed file with 74 additions and 9 deletions.
diff --git a/set.mm b/set.mm
@@ -543219,15 +543219,15 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
     $( The surreals are closed under negation.  (Contributed by Scott Fenton,
        3-Feb-2025.) $)
     negscld $p |- ( ph -> ( -us ` A ) e. No ) $=
-       ( csur wcel cnegs cfv negscl syl ) ABDEBFGDECBHI $.
+      ( csur wcel cnegs cfv negscl syl ) ABDEBFGDECBHI $.
   $}
 
   $( The forward direction of the ordering properties of negation.
      (Contributed by Scott Fenton, 3-Feb-2025.) $)
   sltnegim $p |- ( ( A e. No /\ B e. No ) -> ( A <s B ->
    ( -us ` B ) <s ( -us ` A ) ) ) $=
-     ( csur wcel wa cnegs cfv cslt wbr wi negsprop simprd ) ACDBCDEAFGZCDABHIBF
-     GMHIJABKL $.
+    ( csur wcel wa cnegs cfv cslt wbr wi negsprop simprd ) ACDBCDEAFGZCDABHIBFG
+    MHIJABKL $.
 
   ${
     $d A x y $.
@@ -543236,18 +543236,83 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
     negscut $p |- ( A e. No -> ( ( -us ` A ) e. No /\
       ( -us " ( _R ` A ) ) <<s { ( -us ` A ) } /\
       { ( -us ` A ) } <<s ( -us " ( _L ` A ) ) ) ) $=
-        ( vx vy csur wcel c0s cv cbday cfv cun cnegs cslt wbr wral negsprop a1d
-        wi wa rgen2 a1i id negsproplem3 ) ADEZBCAFBGZHICGZHIJAHIFHIJEZUDKIZDEUD
-        UELMUEKIUGLMQRZQZCDNBDNUCUIBCDDUDDEUEDERUHUFUDUEOPSTUCUAUB $.
+      ( vx vy csur wcel c0s cv cbday cfv cun cnegs cslt wbr wi wa wral negsprop
+      a1d rgen2 a1i id negsproplem3 ) ADEZBCAFBGZHICGZHIJAHIFHIJEZUDKIZDEUDUELM
+      UEKIUGLMNOZNZCDPBDPUCUIBCDDUDDEUEDEOUHUFUDUEQRSTUCUAUB $.
   $}
 
   $( The cut that defines surreal negation is legitimate.  (Contributed by
      Scott Fenton, 3-Feb-2025.) $)
   negscut2 $p |- ( A e. No ->
    ( -us " ( _R ` A ) ) <<s ( -us " ( _L ` A ) ) ) $=
-     ( csur wcel cnegs cright cfv cima csn csslt cleft negscut simp2d simp3d c0
-     wbr wne fvex snnz sslttr mp3an3 syl2anc ) ABCZDAEFGZADFZHZIOZUEDAJFGZIOZUC
-     UGIOZUBUDBCZUFUHAKZLUBUJUFUHUKMUFUHUENPUIUDADQRUCUEUGSTUA $.
+    ( csur wcel cnegs cright cfv cima csn csslt wbr cleft negscut simp2d simp3d
+    c0 wne fvex snnz sslttr mp3an3 syl2anc ) ABCZDAEFGZADFZHZIJZUEDAKFGZIJZUCUG
+    IJZUBUDBCZUFUHALZMUBUJUFUHUKNUFUHUEOPUIUDADQRUCUEUGSTUA $.
+
+  ${
+    $d A a b c d p q x xL xR xO $.
+    $( Surreal addition of a number and its negative.  (Contributed by Scott
+       Fenton, 3-Feb-2025.) $)
+    negsid $p |- ( A e. No -> ( A +s ( -us ` A ) ) = 0s ) $=
+      ( vxl vb vp vxr vd vq cv cnegs cfv cadds co c0s wceq csur wcel syl5ibrcom
+      wrex wbr cslt vx vxo va vc weq fveq2 oveq12d eqeq1d cleft cright cun wral
+      id wa cab cima cscut csslt lltropt adantr negscut2 lrcut negsval addsunif
+      eqcomd wfn wss negsfn rightssno oveq2 eqeq2d imaeqsexv mp2an abbii uneq2i
+      leftssno oveq12i csn cvv fvex abrexex unex a1i snex adantl simpll negscld
+      wb sseli addscld eleq1 rexlimdva abssdv unssd 0sno snssi mp1i wo elun vex
+      eqeq1 rexbidv elab orbi12i bitri velsn anbi12i cbday cold leftval rabeq2i
+      simprbi sltnegim syl2anc mpd sltadd2 syl3anc mpbid simplr rspcdva breqtrd
+      wi elun1 breq1 rightval sltadd1 elun2 jaodan breq2 expimpd biimtrid ssltd
+      imp 3impib eqbrtrrd ex impcomd cuteq0 eqtrid eqtrd noinds ) UAHZUUBIJZKLZ
+      MNZUBHZUUFIJZKLZMNZAAIJZKLZMNUAUBAUAUBUEZUUDUUHMUULUUBUUFUUCUUGKUULUMUUBU
+      UFIUFUGUHUUBANZUUDUUKMUUMUUBAUUCUUJKUUMUMUUBAIUFUGUHUUBOPZUUIUBUUBUIJZUUB
+      UJJZUKZULZUUEUUNUURUNZUUDUCHZBHZUUCKLZNZBUUORZUCUOZCHZUUBDHZKLZNZDIUUPUPZ
+      RZCUOZUKZUDHZEHZUUCKLZNZEUUPRZUDUOZFHZUUBGHZKLZNZGIUUOUPZRZFUOZUKZUQLZMUU
+      SUCCUDFUUBUUCUUPUWDDUUOUVJGEBUUNUUOUUPURSUURUUBUSUTUUNUVJUWDURSUURUUBVAUT
+      UUSUUOUUPUQLZUUBUUNUWIUUBNUURUUBVBUTVEUUNUUCUVJUWDUQLNUURUUBVCUTVDUUSUWHU
+      VEUVFUUBUVOIJZKLZNZEUUPRZCUOZUKZUVSUVTUUBUVAIJZKLZNZBUUORZFUOZUKZUQLMUVMU
+      WOUWGUXAUQUVLUWNUVEUVKUWMCIOVFZUUPOVGUVKUWMWHVHUUBVIZUVIUWLDEOUUPIUVGUWJN
+      UVHUWKUVFUVGUWJUUBKVJVKVLVMVNVOUWFUWTUVSUWEUWSFUXBUUOOVGUWEUWSWHVHUUBVPZU
+      WCUWRGBOUUOIUWAUWPNUWBUWQUVTUWAUWPUUBKVJVKVLVMVNVOVQUUSUWOUXAUUSDGUWOMVRZ
+      VSVSUWOVSPUUSUVEUWNBUCUUOUVBUUBUIVTZWAECUUPUWKUUBUJVTZWAWBWCUXEVSPUUSMWDW
+      CZUUSUVEUWNOUUSUVDUCOUUSUVCUUTOPZBUUOUUSUVAUUOPZUNZUXIUVCUVBOPUXKUVAUUCUX
+      JUVAOPZUUSUUOOUVAUXDWIWEZUXKUUBUUNUURUXJWFZWGZWJUUTUVBOWKQWLWMUUSUWMCOUUS
+      UWLUVFOPZEUUPUUSUVOUUPPZUNZUXPUWLUWKOPUXRUUBUWJUUNUURUXQWFZUXRUVOUXQUVOOP
+      ZUUSUUPOUVOUXCWIWEZWGZWJUVFUWKOWKQWLWMWNMOPUXEOVGUUSWOMOWPWQZUUSUVGUWOPZU
+      WAUXEPZUVGUWATSZUYDUYEUNUVGUVBNZBUUORZUVGUWKNZEUUPRZWRZUWAMNZUNUUSUYFUYDU
+      YKUYEUYLUYDUVGUVEPZUVGUWNPZWRUYKUVGUVEUWNWSUYMUYHUYNUYJUVDUYHUCUVGDWTZUCD
+      UEUVCUYGBUUOUUTUVGUVBXAXBXCUWMUYJCUVGUYOCDUEUWLUYIEUUPUVFUVGUWKXAXBXCXDXE
+      GMXFXGUUSUYKUYLUYFUUSUYKUNUYFUYLUVGMTSZUUSUYHUYPUYJUUSUYHUYPUUSUYGUYPBUUO
+      UXKUYPUYGUVBMTSUXKUVBUVAUWPKLZMTUXKUUCUWPTSZUVBUYQTSZUXKUVAUUBTSZUYRUXJUY
+      TUUSUXJUVAUUBXHJXIJZPUYTUYTBUUOVUABUUBXJXKXLWEZUXKUXLUUNUYTUYRYBUXMUXNUVA
+      UUBXMXNXOUXKUUCOPZUWPOPZUXLUYRUYSWHUXOUXKUVAUXMWGZUXMUUCUWPUVAXPXQXRUXKUU
+      IUYQMNUBUUQUVAUBBUEZUUHUYQMVUFUUFUVAUUGUWPKVUFUMUUFUVAIUFUGUHUUNUURUXJXSU
+      XJUVAUUQPUUSUVAUUOUUPYCWEXTZYAUVGUVBMTYDQWLYMUUSUYJUYPUUSUYIUYPEUUPUXRUYP
+      UYIUWKMTSUXRUWKUVOUWJKLZMTUXRUUBUVOTSZUWKVUHTSZUXQVUIUUSUXQUVOVUAPVUIVUIE
+      UUPVUAEUUBYEXKXLWEZUXRUUNUXTUWJOPZVUIVUJWHUXSUYAUYBUUBUVOUWJYFXQXRUXRUUIV
+      UHMNUBUUQUVOUBEUEZUUHVUHMVUMUUFUVOUUGUWJKVUMUMUUFUVOIUFUGUHUUNUURUXQXSUXQ
+      UVOUUQPUUSUVOUUPUUOYGWEXTZYAUVGUWKMTYDQWLYMYHUWAMUVGTYIQYJYKYNYLUUSDGUXEU
+      XAVSVSUXHUXAVSPUUSUVSUWTEUDUUPUVPUXGWABFUUOUWQUXFWAWBWCUYCUUSUVSUWTOUUSUV
+      RUDOUUSUVQUVNOPZEUUPUXRVUOUVQUVPOPUXRUVOUUCUYAUXRUUBUXSWGZWJUVNUVPOWKQWLW
+      MUUSUWSFOUUSUWRUVTOPZBUUOUXKVUQUWRUWQOPUXKUUBUWPUXNVUEWJUVTUWQOWKQWLWMWNU
+      USUVGUXEPZUWAUXAPZUYFVURVUSUNUVGMNZUWAUVPNZEUUPRZUWAUWQNZBUUORZWRZUNUUSUY
+      FVURVUTVUSVVEDMXFVUSUWAUVSPZUWAUWTPZWRVVEUWAUVSUWTWSVVFVVBVVGVVDUVRVVBUDU
+      WAGWTZUDGUEUVQVVAEUUPUVNUWAUVPXAXBXCUWSVVDFUWAVVHFGUEUWRVVCBUUOUVTUWAUWQX
+      AXBXCXDXEXGUUSVVEVUTUYFUUSVVEVUTUYFYBUUSVVEUNUYFVUTMUWATSZUUSVVBVVIVVDUUS
+      VVBVVIUUSVVAVVIEUUPUXRVVIVVAMUVPTSUXRVUHMUVPTVUNUXRUWJUUCTSZVUHUVPTSZUXRV
+      UIVVJVUKUXRUUNUXTVUIVVJYBUXSUYAUUBUVOXMXNXOUXRVULVUCUXTVVJVVKWHUYBVUPUYAU
+      WJUUCUVOXPXQXRYOUWAUVPMTYIQWLYMUUSVVDVVIUUSVVCVVIBUUOUXKVVIVVCMUWQTSUXKUY
+      QMUWQTVUGUXKUYTUYQUWQTSZVUBUXKUXLUUNVUDUYTVVLWHUXMUXNVUEUVAUUBUWPYFXQXRYO
+      UWAUWQMTYIQWLYMYHUVGMUWATYDQYPYQYKYNYLYRYSYTYPUUA $.
+  $}
+
+  $( A surreal is equal to the negative of its negative.  (Contributed by Scott
+     Fenton, 3-Feb-2025.) $)
+  negnegs $p |- ( A e. No -> ( -us ` ( -us ` A ) ) = A ) $=
+    ( csur wcel cnegs cfv cadds wceq c0s negscl negsid negscld addscomd 3eqtr4d
+    co syl wb id addscan2 syl3anc mpbid ) ABCZADEZDEZUBFNZAUBFNZGZUCAGZUAUBUCFN
+    ZHUDUEUAUBBCZUHHGAIZUBJOUAUCUBUAUBUJKZUJLAJMUAUCBCUAUIUFUGPUKUAQUJUCAUBRST
+    $.
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=