status of nnne0ALT

[Zheng Fan]

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.

[Mario Carneiro]

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 <fanzhe...@outlook.com> 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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/65b3f52c-17c8-42c5-8349-582f2ff86bd8n%40googlegroups.com.

[heiph...@wilsonb.com]

For what it's worth, here's some git history:

$ git log -L '/nnne0ALT \$p/,+1:set.mm'

commit df12e3e7168f44afd3771b5aba5286a66f1ae8f6
Author: Steven Nguyen <nguye...@students.garlandisd.net>
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 <n...@alum.mit.edu>
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 <n...@alum.mit.edu>
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 <n...@alum.mit.edu>
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 <n...@alum.mit.edu>
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 ) $=

> > <https://groups.google.com/d/msgid/metamath/65b3f52c-17c8-42c5-8349-582f2ff86bd8n%40googlegroups.com?utm_medium=email&utm_source=footer>
> > .
> >

[Benoit]

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

[Benoit]

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