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/7bdaf14b-957e-4f95-a927-615e1d5f7ce6n%40googlegroups.com.
