Arithmetic shortenings + Prove 5ne0 to 9ne0 (#5078)

* move subrecd up and shorten

* move 2halves, halfthird up and shorten

* shorten/add 1-9ne0, shorten lsubswap23d

Author: icecream17

set.mm

@@ -135274,13 +135274,25 @@ Ordering on reals (cont.)
       ( cr wcel cc0 wne cdiv co redivcl syl3anc ) ABGHCGHCIJBCKLGHDEFBCMN $.
   $}
 
+  ${
+    subrecd.1 $e |- ( ph -> A e. CC ) $.
+    subrecd.2 $e |- ( ph -> B e. CC ) $.
+    subrecd.3 $e |- ( ph -> A =/= 0 ) $.
+    subrecd.4 $e |- ( ph -> B =/= 0 ) $.
+    $( Subtraction of reciprocals.  (Contributed by Scott Fenton,
+       9-Jan-2017.) $)
+    subrecd $p |- ( ph ->
+      ( ( 1 / A ) - ( 1 / B ) ) = ( ( B - A ) / ( A x. B ) ) ) $=
+      ( c1 cdiv co cmin cmul 1cnd divsubdivd mullidd oveq12d oveq1d eqtrd ) AHB
+      IJHCIJKJHCLJZHBLJZKJZBCLJZIJCBKJZUBIJAHBHCAMZDUDEFGNAUAUCUBIASCTBKACEOABD
+      OPQR $.
+  $}
+
   $( Subtraction of reciprocals.  (Contributed by Scott Fenton, 9-Jul-2015.) $)
   subrec $p |- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) ->
     ( ( 1 / A ) - ( 1 / B ) ) = ( ( B - A ) / ( A x. B ) ) ) $=
-    ( cc wcel cc0 wne wa c1 cdiv cmin cmul 1cnd simpll simprl simplr divsubdivd
-    co simprr mullidd oveq12d oveq1d eqtrd ) ACDZAEFZGZBCDZBEFZGZGZHAIQHBIQJQHB
-    KQZHAKQZJQZABKQZIQBAJQZUMIQUIHAHBUILZUCUDUHMZUOUEUFUGNZUCUDUHOUEUFUGRPUIULU
-    NUMIUIUJBUKAJUIBUQSUIAUPSTUAUB $.
+    ( cc wcel cc0 wne wa simpll simprl simplr simprr subrecd ) ACDZAEFZGZBCDZBE
+    FZGZGABMNRHOPQIMNRJOPQKL $.
 
   ${
     subreci.1 $e |- A e. CC $.
@@ -135294,19 +135306,6 @@ Ordering on reals (cont.)
       LMKBLMNMBANMABOMLMPCEDFABQR $.
   $}
 
-  ${
-    subrecd.1 $e |- ( ph -> A e. CC ) $.
-    subrecd.2 $e |- ( ph -> B e. CC ) $.
-    subrecd.3 $e |- ( ph -> A =/= 0 ) $.
-    subrecd.4 $e |- ( ph -> B =/= 0 ) $.
-    $( Subtraction of reciprocals.  (Contributed by Scott Fenton,
-       9-Jan-2017.) $)
-    subrecd $p |- ( ph ->
-      ( ( 1 / A ) - ( 1 / B ) ) = ( ( B - A ) / ( A x. B ) ) ) $=
-      ( cc wcel cc0 wne c1 cdiv co cmin cmul wceq subrec syl22anc ) ABHIBJKCHIC
-      JKLBMNLCMNONCBONBCPNMNQDFEGBCRS $.
-  $}
-
   ${
     mvllmuld.1 $e |- ( ph -> A e. CC ) $.
     mvllmuld.2 $e |- ( ph -> B e. CC ) $.
@@ -138118,7 +138117,7 @@ of the complex number axiom system (see ~ df-0 and ~ df-1 ).
 
   $( The number 2 is nonzero.  (Contributed by NM, 9-Nov-2007.) $)
   2ne0 $p |- 2 =/= 0 $=
-    ( c2 2re 2pos gt0ne0ii ) ABCD $.
+    ( c2 2nn nnne0i ) ABC $.
 
   $( The number 3 is positive.  (Contributed by NM, 27-May-1999.) $)
   3pos $p |- 0 < 3 $=
@@ -138128,7 +138127,7 @@ of the complex number axiom system (see ~ df-0 and ~ df-1 ).
   $( The number 3 is nonzero.  (Contributed by FL, 17-Oct-2010.)  (Proof
      shortened by Andrew Salmon, 7-May-2011.) $)
   3ne0 $p |- 3 =/= 0 $=
-    ( c3 3re 3pos gt0ne0ii ) ABCD $.
+    ( c3 3nn nnne0i ) ABC $.
 
   $( The number 4 is positive.  (Contributed by NM, 27-May-1999.) $)
   4pos $p |- 0 < 4 $=
@@ -138138,7 +138137,7 @@ of the complex number axiom system (see ~ df-0 and ~ df-1 ).
   $( The number 4 is nonzero.  (Contributed by David A. Wheeler,
      5-Dec-2018.) $)
   4ne0 $p |- 4 =/= 0 $=
-    ( c4 4re 4pos gt0ne0ii ) ABCD $.
+    ( c4 4nn nnne0i ) ABC $.
 
   $( The number 5 is positive.  (Contributed by NM, 27-May-1999.) $)
   5pos $p |- 0 < 5 $=
@@ -138672,12 +138671,17 @@ ordinal natural numbers (finite integers starting at 0), so that proof
     ( c1 cdiv co clt wbr 1div1e1 1lt2 eqbrtri 1re 2re 0lt1 2pos ltdiv23ii mpbi
     c2 ) AABCZODEAOBCADEPAODFGHAAOIIJKLMN $.
 
-  $( Prove that 1 - 1/2 = 1/2.  (Contributed by David A. Wheeler,
-     4-Jan-2017.) $)
+  $( Two halves make a whole.  (Contributed by NM, 11-Apr-2005.) $)
+  2halves $p |- ( A e. CC -> ( ( A / 2 ) + ( A / 2 ) ) = A ) $=
+    ( cc wcel c2 cmul co cdiv caddc 2times oveq1d cc0 wne wceq 2cn 2ne0 divcan3
+    mp3an23 wa 2cnne0 divdir mp3an3 anidms 3eqtr3rd ) ABCZDAEFZDGFZAAHFZDGFZAAD
+    GFZUIHFZUDUEUGDGAIJUDDBCZDKLZUFAMNOADPQUDUHUJMZUDUDUKULRUMSAADTUAUBUC $.
+
+  $( Prove that 1 - 1/2 = 1/2.  (Contributed by David A. Wheeler, 4-Jan-2017.)
+     (Proof shortened by SN, 22-Oct-2025.) $)
   1mhlfehlf $p |- ( 1 - ( 1 / 2 ) ) = ( 1 / 2 ) $=
-    ( c2 c1 cmin co cdiv cc wcel cc0 wne wceq 2cn ax-1cn 2cnne0 divsubdir mp3an
-    wa 2m1e1 oveq1i 2div2e1 3eqtr3ri ) ABCDZAEDZAAEDZBAEDZCDZUDBUDCDAFGZBFGUFAH
-    IPUBUEJKLMABANOUABAEQRUCBUDCSRT $.
+    ( c1 c2 cdiv co ax-1cn halfcn cc wcel caddc wceq 2halves ax-mp subaddrii )
+    AABCDZNEFFAGHNNIDAJEAKLM $.
 
   $( An eighth of four thirds is a sixth.  (Contributed by Paul Chapman,
      24-Nov-2007.) $)
@@ -138689,20 +138693,23 @@ ordinal natural numbers (finite integers starting at 0), so that proof
     VHEFNGDZGDZVDEFGDNGDZVHVJENGDZFGDVKVHENFLRQUCVLBFGUDUEOEFNLQRUFOVIHEGUGUHPU
     KPHSTZHULUMZESTZEULUMZVEVFUNZHUOKHUOUPMLUQASTVMVNURVOVPURVQIAHEUSUTVAP $.
 
+  $( Half minus a third.  (Contributed by Scott Fenton, 8-Jul-2015.) $)
+  halfthird $p |- ( ( 1 / 2 ) - ( 1 / 3 ) ) = ( 1 / 6 ) $=
+    ( c1 c2 cdiv co c3 cmin cmul c6 2cn 3cn 2ne0 subreci ax-1cn 2p1e3 subaddrii
+    3ne0 3t2e6 mulcomli oveq12i eqtri ) ABCDAECDFDEBFDZBEGDZCDAHCDBEIJKPLUAAUBH
+    CEBAJIMNOEBHJIQRST $.
+
   $( One half plus or minus one sixth.  (Contributed by Paul Chapman,
-     17-Jan-2008.) $)
+     17-Jan-2008.)  (Proof shortened by SN, 22-Oct-2025.) $)
   halfpm6th $p |- ( ( ( 1 / 2 ) - ( 1 / 6 ) ) = ( 1 / 3 ) /\
                        ( ( 1 / 2 ) + ( 1 / 6 ) ) = ( 2 / 3 ) ) $=
-    ( c1 c2 cdiv co c6 cmin wceq caddc cmul 3cn ax-1cn 2cn 3ne0 2ne0 divmuldivi
-    c3 oveq1i mulridi 3t2e6 oveq12i dividi halfcn mullidi eqtri 3eqtr3i cc wcel
-    cc0 wne wa 6cn 6re 6pos gt0ne0ii pm3.2i divsubdir mp3an 3m1e2 oveq2i reccli
-    3eqtr2i c4 divdiri df-4 3eqtr4ri 2t2e4 divcli ) ABCDZAECDZFDZAPCDZGVHVIHDZB
-    PCDZGVJPECDZVIFDZPAFDZECDZVKVHVNVIFPPCDZVHIDZPAIDZPBIDZCDVHVNPPABJJKLMNOVSA
-    VHIDVHVRAVHIPJMUAQVHUBUCUDVTPWAECPJRSTUEZQPUFUGAUFUGEUFUGZEUHUIZUJVQVOGJKWC
-    WDUKEULUMUNZUOPAEUPUQVQBECDABIDZWACDZVKVPBECURQWFBWAECBLUCSTVKBBCDZIDVKAIDW
-    GVKWHAVKIBLNUAZUSAPBBKJLLMNOVKPJMUTRUEVAVAVLVBECDZBBIDZWACDZVMPAHDZECDVNVIH
-    DWJVLPAEJKUKWEVCVBWMECVDQVHVNVIHWBQVEWKVBWAECVFSTVMWHIDVMAIDWLVMWHAVMIWIUSB
-    PBBLJLLMNOVMBPLJMVGRUEVAUO $.
+    ( c1 c2 cdiv co c6 cmin c3 wceq 3cn 3ne0 reccli 6cn halfcn halfthird oveq2i
+    caddc eqtr3i mvrraddi 2cn ax-1cn 6pos gt0ne0ii pncan3i addsubassi divcli cc
+    6re wcel 2halves ax-mp 2p1e3 oveq1i dividi eqtri divdiri 3eqtr2i pm3.2i ) A
+    BCDZAECDZFDAGCDZHURUSPDZBGCDZHURUTUSGIJKZELEUGUAUBKUTURUTFDZPDURUTUSPDUTURV
+    CMUCVDUSUTPNOQRURVDPDZVAVBVDUSURPNOURURPDZUTFDVEVBURURUTMMVCUDVFVBUTBGSIJUE
+    VCVFABAPDZGCDZVBUTPDAUFUHVFAHTAUIUJVHGGCDAVGGGCUKULGIJUMUNBAGSTIJUOUPRQQUQ
+    $.
 
   $( i times 0 equals 0.  (Contributed by David A. Wheeler, 8-Dec-2018.) $)
   it0e0 $p |- ( _i x. 0 ) = 0 $=
@@ -138739,12 +138746,6 @@ ordinal natural numbers (finite integers starting at 0), so that proof
     ( cc wcel c2 cc0 wne cdiv co wceq wb 2cn 2ne0 diveq0 mp3an23 ) ABCDBCDEFADG
     HEIAEIJKLADMN $.
 
-  $( Two halves make a whole.  (Contributed by NM, 11-Apr-2005.) $)
-  2halves $p |- ( A e. CC -> ( ( A / 2 ) + ( A / 2 ) ) = A ) $=
-    ( cc wcel c2 cmul co cdiv caddc 2times oveq1d cc0 wne wceq 2cn 2ne0 divcan3
-    mp3an23 wa 2cnne0 divdir mp3an3 anidms 3eqtr3rd ) ABCZDAEFZDGFZAAHFZDGFZAAD
-    GFZUIHFZUDUEUGDGAIJUDDBCZDKLZUFAMNOADPQUDUHUJMZUDUDUKULRUMSAADTUAUBUC $.
-
   $( A number is positive iff its half is positive.  (Contributed by NM,
      10-Apr-2005.) $)
   halfpos2 $p |- ( A e. RR -> ( 0 < A <-> 0 < ( A / 2 ) ) ) $=
@@ -142066,12 +142067,6 @@ nonnegative integers (cont.)". $)
       FGEDEZFGEHADEZIGEACIHPJBKLQCGEPABMNON $.
   $}
 
-  $( Half minus a third.  (Contributed by Scott Fenton, 8-Jul-2015.) $)
-  halfthird $p |- ( ( 1 / 2 ) - ( 1 / 3 ) ) = ( 1 / 6 ) $=
-    ( c1 c2 cdiv co c3 cmin cmul c6 2cn 3cn 2ne0 subreci ax-1cn 2p1e3 subaddrii
-    3ne0 3t2e6 mulcomli oveq12i eqtri ) ABCDAECDFDEBFDZBEGDZCDAHCDBEIJKPLUAAUBH
-    CEBAJIMNOEBHJIQRST $.
-
   $( One fifth minus one sixth.  (Contributed by Scott Fenton, 9-Jan-2017.) $)
   5recm6rec $p |- ( ( 1 / 5 ) - ( 1 / 6 ) ) = ( 1 / ; 3 0 ) $=
     ( c1 c5 cdiv co c6 cmin cmul cc0 cdc 5cn 6cn 5re 5pos gt0ne0ii 6pos subreci
@@ -699148,6 +699143,26 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
       UJUKTUFBDUOUPUAUPUNUGDCUBUCUD $.
   $}
 
+  $( The number 5 is nonzero.  (Contributed by SN, 22-Oct-2025.) $)
+  5ne0 $p |- 5 =/= 0 $=
+    ( c5 5nn nnne0i ) ABC $.
+
+  $( The number 6 is nonzero.  (Contributed by SN, 22-Oct-2025.) $)
+  6ne0 $p |- 6 =/= 0 $=
+    ( c6 6nn nnne0i ) ABC $.
+
+  $( The number 7 is nonzero.  (Contributed by SN, 22-Oct-2025.) $)
+  7ne0 $p |- 7 =/= 0 $=
+    ( c7 7nn nnne0i ) ABC $.
+
+  $( The number 8 is nonzero.  (Contributed by SN, 22-Oct-2025.) $)
+  8ne0 $p |- 8 =/= 0 $=
+    ( c8 8nn nnne0i ) ABC $.
+
+  $( The number 9 is nonzero.  (Contributed by SN, 22-Oct-2025.) $)
+  9ne0 $p |- 9 =/= 0 $=
+    ( c9 9nn nnne0i ) ABC $.
+
   $( A proof of ~ 1ne2 without using ~ ax-mulcom , ~ ax-mulass ,
      ~ ax-pre-mulgt0 .  Based on ~ mul02lem2 .  (Contributed by SN,
      13-Dec-2023.) $)
@@ -699365,9 +699380,8 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
        until it would have 7 uses: current additional uses:  (none).
        (Contributed by SN, 23-Aug-2024.) $)
     lsubswap23d $p |- ( ph -> ( A - C ) = B ) $=
-      ( cmin co cc subcld eqeltrrd cc0 subeq0bd sub32d subidd 3eqtr4d subcan2d
-      ) ABDHIZCCABDEABCHIZDJGABCEFKZLZKFFATDHIMSCHICCHIATDUAGNABDCEUBFOACFPQR
-      $.
+      ( cmin co cc subcld eqeltrrd caddc lsubrotld eqcomd mvrraddd ) ABCDFABCHI
+      DJGABCEFKLACDMIBABCDEFGNOP $.
   $}
 
   $( Relation between sums and differences.  (Contributed by Steven Nguyen,