how to deduce a positive integer is a natural number? (slowly getting familiar with set.mm style)

[LM]

what is most set.mm-fitting way to prove:

( ( A e. ZZ /\ 1 <_ A ) -> A e. NN )

?

Grepping through set.mm I only find " e. NN " on antecedent side, never on consequent side.

[Mario Carneiro]

The most relevant theorem appears to be https://us.metamath.org/mpeuni/elnnz1.html . In general, you should try to look for biconditional statements as well, because we try to prove biconditionals when possible, and instead rely on versions of modus ponens that build in some kind of biconditional elimination to make them easy to use. You would apply it using something like https://us.metamath.org/mpeuni/sylibr.html or https://us.metamath.org/mpeuni/sylanbrc.html .

--
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/7a3251c5-87bd-4d95-9db0-6198cad47f43n%40googlegroups.com.

[Igor Ieskov]

It could be proved with https://us.metamath.org/mpeuni/biimpri.html , for example:

--------------------------------------------------------------------------------------------
1 | : elnnz1    | |- ( A e. NN <-> ( A e. ZZ /\ 1 <_ A ) )
2 | 1 : biimpri | |- ( ( A e. ZZ /\ 1 <_ A ) -> A e. NN )
--------------------------------------------------------------------------------------------

aenn $p |- ( ( A e. ZZ /\ 1 <_ A ) -> A e. NN ) $= ( cn wcel cz c1 cle wbr wa elnnz1 biimpri ) ABCADCEAFGHAIJ $.

-

Igor

[LM]

Thank you both!

Op woensdag 19 april 2023 om 10:11:17 UTC+2 schreef igori...@gmail.com:

[Jim Kingdon]

We already have the biconditionalized version of this at https://us.metamath.org/mpeuni/elnnz1.html

There's a general rule here, which is written down in https://us.metamath.org/mpeuni/conventions.html in the paragraph starting "There are basically two ways to maximize the effectiveness of biconditional"