Done in https://github.com/metamath/set.mm/pull/3027 That proof had actually been deprecated to 0nnnOLD so I converted it to 0nnnALT to be able to use it in nnne0ALT.
Benoît On Saturday, February 4, 2023 at 12:47:21 PM UTC+1 Benoit wrote: > The original proof is: > > !SHOW PROOF 0nnn > 8 mt2.1=0lt1 $p |- 0 < 1 > 10 mt2.2=nnnlt1 $p |- ( 0 e. NN -> -. 0 < 1 ) > 11 0nnn=mt2 $p |- -. 0 e. NN > > so I'm going to add it as 0nnnALT and use 0nnnALT in nnne0ALT. > > Benoît > > On Thursday, February 2, 2023 at 2:33:36 AM UTC+1 [email protected] > wrote: > >> For what it's worth, here's some git history: >> >> $ git log -L '/nnne0ALT \$p/,+1:set.mm' >> >> commit df12e3e7168f44afd3771b5aba5286a66f1ae8f6 >> Author: Steven Nguyen <[email protected]> >> Date: Tue Jan 31 14:18:36 2023 -0600 >> >> rename equsb3lem et al to equsb3v et al, rmv ax-mulgt0 from 0nnn (#3018) >> >> * rename equsb3lem et al to equsb3v et al, rmv ax-mulgt0 from nnnn0 >> also reduces ax-13 from the renamed elsb3v and elsb4v >> >> I wonder how many of these improvements to set.mm transfer to iset.mm >> >> * rewrap >> >> * rmv elsb3vOLD + elsb4vOLD >> tag drift >> >> diff --git a/set.mm b/set.mm >> --- a/set.mm >> +++ b/set.mm >> @@ -121870,2 +121896,1 @@ >> - $( A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) $) >> - nnne0 $p |- ( A e. NN -> A =/= 0 ) $= >> + nnne0ALT $p |- ( A e. NN -> A =/= 0 ) $= >> >> commit 98e1d43acb1e96b6ca2010bd83fa2894032074ee >> Author: nmegill <[email protected]> >> Date: Mon Oct 15 19:55:51 2018 -0400 >> >> set.mm - change 'natural number' to 'positive integer' in NN comments >> >> diff --git a/set.mm b/set.mm >> --- a/set.mm >> +++ b/set.mm >> @@ -119172,2 +119173,2 @@ >> - $( A natural number is nonzero. (Contributed by NM, 27-Sep-1999.) $) >> + $( A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) $) >> nnne0 $p |- ( A e. NN -> A =/= 0 ) $= >> >> commit c5fe509062dcca53a4d0572a71c953d5bd27d4a1 >> Author: Norm <[email protected]> >> Date: Thu Nov 5 13:08:37 2015 -0500 >> >> Handed to Mario to identify missing contributors >> >> diff --git a/set.mm b/set.mm >> --- a/set.mm >> +++ b/set.mm >> @@ -112270,2 +116100,2 @@ >> - $( A natural number is nonzero. $) >> + $( A natural number is nonzero. (Contributed by NM, 27-Sep-1999.) $) >> nnne0 $p |- ( A e. NN -> A =/= 0 ) $= >> >> commit 0d2cf5049823b116baad01ff6be6481219113d8e >> Author: Norm <[email protected]> >> Date: Tue May 12 09:14:21 2015 -0400 >> >> stable release, archive name set.mm.2011-06-27 >> >> diff --git a/set.mm b/set.mm >> --- a/set.mm >> +++ b/set.mm >> @@ -69477,2 +71839,2 @@ >> - $( A natural number is non-zero. $) >> + $( A natural number is nonzero. $) >> nnne0 $p |- ( A e. NN -> A =/= 0 ) $= >> >> commit 45f6474f112a5cf2d76cd1aaf659be990bff61c5 >> Author: Norm <[email protected]> >> Date: Tue May 12 09:14:16 2015 -0400 >> >> stable release, archive name set.mm.2010-08-29 >> >> diff --git a/set.mm b/set.mm >> --- a/set.mm >> +++ b/set.mm >> @@ -67129,0 +69477,2 @@ >> + $( A natural number is non-zero. $) >> + nnne0 $p |- ( A e. NN -> A =/= 0 ) $= >> >> Mario Carneiro <[email protected]> wrote: >> > It sounds like we were unable to prevent a proof modification in this >> case. >> > We'll have to go back through the history to find out what the original >> > proof was and how it degenerated. >> > >> > On Wed, Feb 1, 2023 at 12:54 PM Zheng Fan <[email protected]> >> wrote: >> > >> > > The proof of nnne0ALT is a thin wrapper of 0nnn, which is in turn a >> thin >> > > wrapper of nnne0, which makes me think why this alternative proof is >> kept. >> > > The caption says that it is supposed to be a shorter proof using more >> > > axioms, but it seems not the case, at least for the current version >> of >> > > set.mm. >> > > >> > > -- >> > > You received this message because you are subscribed to the Google >> Groups >> > > "Metamath" group. >> > > To unsubscribe from this group and stop receiving emails from it, >> send an >> > > email to [email protected]. >> > > To view this discussion on the web visit >> > > >> https://groups.google.com/d/msgid/metamath/65b3f52c-17c8-42c5-8349-582f2ff86bd8n%40googlegroups.com >> >> > > < >> https://groups.google.com/d/msgid/metamath/65b3f52c-17c8-42c5-8349-582f2ff86bd8n%40googlegroups.com?utm_medium=email&utm_source=footer> >> >> >> > > . >> > > >> >> >> -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9cb2ce8a-052c-4ef3-90fc-bfb339de4396n%40googlegroups.com.
