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 On Wednesday, April 19, 2023 at 5:17:38 AM UTC+2 [email protected] wrote: > 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 . > > On Tue, Apr 18, 2023 at 11:11 PM LM <[email protected]> wrote: > >> 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. >> >> -- >> 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/7a3251c5-87bd-4d95-9db0-6198cad47f43n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/7a3251c5-87bd-4d95-9db0-6198cad47f43n%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/c4112688-66bc-42b1-a558-6297c0513b77n%40googlegroups.com.
