zaddcom, shorten zmulcom

metamath · Feb 2, 2025 · 0f706de · 0f706de
1 parent cbdf352
commit 0f706de
Showing 1 changed file with 70 additions and 35 deletions.
diff --git a/set.mm b/set.mm
@@ -662578,6 +662578,54 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
     $( $j usage 'sn-nnne0' avoids 'ax-mulcom'; $)
   $}
 
+  $( ~ elznn0nn restated using ~ df-resub .  (Contributed by SN,
+     25-Jan-2025.) $)
+  reelznn0nn $p |-
+    ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ ( 0 -R N ) e. NN ) ) ) $=
+    ( cz wcel cn0 cr cneg cn wa cc0 cresub elznn0nn cmin df-neg wceq resubeqsub
+    wo co 0re mpan eqtr4id eleq1d pm5.32i orbi2i bitri ) ABCADCZAECZAFZGCZHZPUE
+    UFIAJQZGCZHZPAKUIULUEUFUHUKUFUGUJGUFUGIALQZUJAMIECUFUJUMNRIAOSTUAUBUCUD $.
+
+  $( Addition is commutative for nonnegative integers.  Proven without
+     ~ ax-mulcom .  (Contributed by SN, 1-Feb-2025.) $)
+  nn0addcom $p |- ( ( A e. NN0 /\ B e. NN0 ) -> ( A + B ) = ( B + A ) ) $=
+    ( cn0 wcel cn cc0 wceq wo caddc co elnn0 readdid2 readdid1 eqtr4d syl oveq1
+    cr oveq2 eqeq12d syl5ibrcom nnaddcom nnre impcom jaoian sylanb nn0re jaodan
+    imp sylan2b ) BCDACDZBEDZBFGZHABIJZBAIJZGZBKUJUKUOULUJAEDZAFGZHUKUOAKUPUKUO
+    UQABUAUKUQUOUKUOUQFBIJZBFIJZGZUKBQDZUTBUBVAURBUSBLBMNOUQUMURUNUSAFBIPAFBIRS
+    TUCUDUEUJULUOUJUOULAFIJZFAIJZGZUJAQDZVDAUFVEVBAVCAMALNOULUMVBUNVCBFAIRBFAIP
+    STUHUGUI $.
+  $( $j usage 'nn0addcom' avoids 'ax-mulcom'; $)
+
+  $( Lemma for ~ zaddcom .  (Contributed by SN, 1-Feb-2025.) $)
+  zaddcomlem $p |- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) ->
+                     ( A + B ) = ( B + A ) ) $=
+    ( cr wcel cc0 cresub co cn wa cn0 caddc simpr nn0cnd ad2antrr recnd addassd
+    wceq syl oveq1d addcld rernegcl simpll renegid2 oveq2d nn0re adantl 3eqtrrd
+    readdid1 readdid2 sylan9eq nnnn0 nn0addcom sylan adantll 3eqtr4d sn-addcand
+    adantr 3eqtr3d mpbid ) ACDZEAFGZHDZIZBJDZIZVAABKGZKGZVABAKGZKGZQVFVHQVEVAAK
+    GZBKGZVABKGZAKGZVGVIVEBBVAKGZAKGZVKVMVEVOBVJKGBEKGZBVEBVAAVEBVCVDLMZVEVAUTV
+    ACDVBVDAUANOZVEAUTVBVDUBOZPVEVJEBKUTVJEQVBVDAUCZNUDVDVPBQZVCVDBCDZWABUEZBUH
+    RUFUGVCVDVKEBKGZBUTVKWDQVBUTVJEBKVTSUQVDWBWDBQWCBUIRUJVEVLVNAKVBVDVLVNQZUTV
+    BVAJDVDWEVAUKVABULUMUNSUOVEVAABVRVSVQPVEVABAVRVQVSPURVEVAVFVHVRVEABVSVQTVEB
+    AVQVSTUPUS $.
+
+  $( Addition is commutative for integers.  Proven without ~ ax-mulcom .
+     (Contributed by SN, 25-Jan-2025.) $)
+  zaddcom $p |- ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) = ( B + A ) ) $=
+    ( cz wcel cn0 cr cresub co cn wa wo caddc wceq reelznn0nn zaddcomlem oveq1d
+    cc0 nncnd addassd 3eqtr4d nn0addcom eqcomd renegid2 ad2antrl ad2antrr recnd
+    ancoms simplr simpll simprl readdid2 oveq2d simprr addcld nnaddcom ad2ant2l
+    3eqtr3d nnaddcld sn-addcand mpbid ccase syl2anb ) ACDAEDZAFDZQAGHZIDZJZKBED
+    ZBFDZQBGHZIDZJZKABLHZBALHZMZBCDANBNVCVHVGVLVOABUAABOVLVCVOVLVCJVNVMBAOUBUGV
+    GVLJZVEVJLHZVMLHZVQVNLHZMVOVPVJVELHZVMLHZVEVJVNLHZLHZVRVSVPVJVEVMLHZLHZVEAL
+    HZWAWCVPVJBLHZQWEWFVIWGQMVGVKBUCUDZVPWDBVJLVPWFBLHQBLHZWDBVPWFQBLVDWFQMVFVL
+    AUCUEZPVPVEABVPVEVDVFVLUHZRZVPAVDVFVLUIUFZVPBVGVIVKUJUFZSVIWIBMVGVKBUKUDUQU
+    LWJTVPVJVEVMVPVJVGVIVKUMZRZWLVPABWMWNUNZSVPWBAVELVPWGALHQALHZWBAVPWGQALWHPV
+    PVJBAWPWNWMSVDWRAMVFVLAUKUEUQULTVPVQVTVMLVFVKVQVTMVDVIVEVJUOUPPVPVEVJVNWLWP
+    VPBAWNWMUNZSTVPVQVMVNVPVQVPVEVJWKWOURRWQWSUSUTVAVB $.
+  $( $j usage 'zaddcom' avoids 'ax-mulcom'; $)
+
   ${
     $d A x y $.  $d N x y $.  $d ph x y $.
     renegmulnnass.a $e |- ( ph -> A e. RR ) $.
@@ -662602,14 +662650,6 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
       DYCVGOUTVIVJ $.
   $}
 
-  $( ~ elznn0nn restated using ~ df-resub .  (Contributed by SN,
-     25-Jan-2025.) $)
-  reelznn0nn $p |-
-    ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ ( 0 -R N ) e. NN ) ) ) $=
-    ( cz wcel cn0 cr cneg cn wa cc0 cresub elznn0nn cmin df-neg wceq resubeqsub
-    wo co 0re mpan eqtr4id eleq1d pm5.32i orbi2i bitri ) ABCADCZAECZAFZGCZHZPUE
-    UFIAJQZGCZHZPAKUIULUEUFUHUKUFUGUJGUFUGIALQZUJAMIECUFUJUMNRIAOSTUAUBUCUD $.
-
   $( Multiplication is commutative for nonnegative integers.  Proven without
      ~ ax-mulcom .  (Contributed by SN, 25-Jan-2025.) $)
   nn0mulcom $p |- ( ( A e. NN0 /\ B e. NN0 ) -> ( A x. B ) = ( B x. A ) ) $=
@@ -662622,39 +662662,34 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
   $( $j usage 'nn0mulcom' avoids 'ax-mulcom'; $)
 
   $( Lemma for ~ zmulcom .  (Contributed by SN, 25-Jan-2025.) $)
-  zmulcomlem $p |- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN ) ->
+  zmulcomlem $p |- ( ( ( A e. RR /\ ( 0 -R A ) e. NN ) /\ B e. NN0 ) ->
                      ( A x. B ) = ( B x. A ) ) $=
-    ( cr wcel cresub co cn wa cmul wceq renegneg oveq1d ad2antrr rernegcl simpr
-    cc0 renegmulnnass oveq2d adantl 3eqtr3d adantll resubdi syl3anc remul01 syl
-    nnmulcom nnre 0red eqtrd 3eqtr2d ) ACDZPAEFZGDZHZBGDZHZPULEFZBIFZABIFZUSBAI
-    FZUKURUSJUMUOUKUQABIAKZLMZVBUPURPULBIFZEFZUSUTUPULBUKULCDZUMUOANMZUNUOOQVBU
-    PVDPBULIFZEFZBUQIFZUTUPVCVGPEUMUOVCVGJUKULBUFUARUPVIBPIFZVGEFZVHUPBCDZPCDVE
-    VIVKJUOVLUNBUGZSUPUHVFBPULUBUCUPVJPVGEUOVJPJZUNUOVLVNVMBUDUESLUIUPUQABIUKUQ
-    AJUMUOVAMRUJTT $.
+    ( cn0 wcel cr cc0 cresub co cn wa wceq wo cmul elnn0 oveq1d ad2antrr oveq2d
+    adantl remul01 3eqtr3d renegneg rernegcl renegmulnnass adantll nnre resubdi
+    simpr nnmulcom 0red syl3anc eqtrd 3eqtr2d remul02 eqtr4d adantr oveq2 oveq1
+    syl eqeq12d syl5ibrcom imp jaodan sylan2b ) BCDAEDZFAGHZIDZJZBIDZBFKZLABMHZ
+    BAMHZKZBNVGVHVLVIVGVHJZFVEGHZBMHZVJVJVKVDVOVJKVFVHVDVNABMAUAZOPZVQVMVOFVEBM
+    HZGHZVJVKVMVEBVDVEEDZVFVHAUBPZVGVHUGUCVQVMVSFBVEMHZGHZBVNMHZVKVMVRWBFGVFVHV
+    RWBKVDVEBUHUDQVMWDBFMHZWBGHZWCVMBEDZFEDVTWDWFKVHWGVGBUEZRVMUIWABFVEUFUJVMWE
+    FWBGVHWEFKZVGVHWGWIWHBSURROUKVMVNABMVDVNAKVFVHVPPQULTTVGVIVLVGVLVIAFMHZFAMH
+    ZKZVDWLVFVDWJFWKASAUMUNUOVIVJWJVKWKBFAMUPBFAMUQUSUTVAVBVC $.
 
   $( Multiplication is commutative for integers.  Proven without ~ ax-mulcom .
-     (Contributed by SN, 25-Jan-2025.) $)
+     From this result and ~ grpcominv1 , we can show that rationals commute
+     under multiplication without using ~ ax-mulcom .  (Contributed by SN,
+     25-Jan-2025.) $)
   zmulcom $p |- ( ( A e. ZZ /\ B e. ZZ ) -> ( A x. B ) = ( B x. A ) ) $=
-    ( cz wcel cn0 cr cc0 cresub co cn wa wo cmul wceq reelznn0nn elnn0 rernegcl
-    zmulcomlem ad2antrr ad2antrl nn0mulcom remul01 remul02 eqtr4d oveq2 eqeq12d
-    adantr oveq1 syl5ibrcom jaodan sylan2b eqcomd ancoms impcom jaoian nnmulcom
-    imp sylanb ad2ant2l oveq2d simprr renegmulnnass simplr 3eqtr4d syl renegneg
-    remulneg2d oveq12d 3eqtr3d ccase syl2anb ) ACDAEDZAFDZGAHIZJDZKZLBEDZBFDZGB
-    HIZJDZKZLABMIZBAMIZNZBCDAOBOVLVQVPWAWDABUAVQVPBJDZBGNZLWDBPVPWEWDWFABRVPWFW
-    DVPWDWFAGMIZGAMIZNZVMWIVOVMWGGWHAUBAUCUDUGWFWBWGWCWHBGAMUEBGAMUHUFUIUQUJUKV
-    LAJDZAGNZLWAWDAPWJWAWDWKWAWJWDWAWJKWCWBBARULUMWAWKWDWAWDWKGBMIZBGMIZNZVRWNV
-    TVRWLGWMBUCBUBUDUGWKWBWLWCWMAGBMUHAGBMUEUFUIUNUOURVPWAKZGVNHIZGVSHIZMIZWQWP
-    MIZWBWCWOGWPVSMIZHIGWQVNMIZHIWRWSWOWTXAGHWOGVNVSMIZHIGVSVNMIZHIWTXAWOXBXCGH
-    VOVTXBXCNVMVRVNVSUPUSUTWOVNVSVMVNFDZVOWAAQZSZVPVRVTVAVBWOVSVNVRVSFDZVPVTBQZ
-    TZVMVOWAVCVBVDUTWOWPVSVMWPFDZVOWAVMXDXJXEVNQVESXIVGWOWQVNVRWQFDZVPVTVRXGXKX
-    HVSQVETXFVGVDWOWPAWQBMVMWPANVOWAAVFSZVRWQBNVPVTBVFTZVHWOWQBWPAMXMXLVHVIVJVK
-    $.
+    ( cz wcel cn0 cr cresub co cn wa wo cmul wceq reelznn0nn zmulcomlem oveq2d
+    cc0 rernegcl ad2antrr ad2antrl nn0mulcom eqcomd ancoms simprr renegmulnnass
+    nnmulcom ad2ant2l simplr 3eqtr4d syl renegneg oveq12d 3eqtr3d ccase syl2anb
+    remulneg2d ) ACDAEDZAFDZQAGHZIDZJZKBEDZBFDZQBGHZIDZJZKABLHZBALHZMZBCDANBNUQ
+    VBVAVFVIABUAABOVFUQVIVFUQJVHVGBAOUBUCVAVFJZQUSGHZQVDGHZLHZVLVKLHZVGVHVJQVKV
+    DLHZGHQVLUSLHZGHVMVNVJVOVPQGVJQUSVDLHZGHQVDUSLHZGHVOVPVJVQVRQGUTVEVQVRMURVC
+    USVDUFUGPVJUSVDURUSFDZUTVFARZSZVAVCVEUDUEVJVDUSVCVDFDZVAVEBRZTZURUTVFUHUEUI
+    PVJVKVDURVKFDZUTVFURVSWEVTUSRUJSWDUPVJVLUSVCVLFDZVAVEVCWBWFWCVDRUJTWAUPUIVJ
+    VKAVLBLURVKAMUTVFAUKSZVCVLBMVAVEBUKTZULVJVLBVKALWHWGULUMUNUO $.
   $( $j usage 'zmulcom' avoids 'ax-mulcom'; $)
 
-  $( From ~ grpcominv1 , ~ nnaddcom , and ~ zmulcom , we can show that integers
-     commute under addition and rationals commute under multiplication
-     without using ~ ax-mulcom . $)
-
   ${
     mulgt0con1dlem.a $e |- ( ph -> A e. RR ) $.
     mulgt0con1dlem.b $e |- ( ph -> B e. RR ) $.