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 <ludwig.m...@gmail.com> 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 metamath+unsubscr...@googlegroups.com. > 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsFZqgNo26-h_Qayc28SBj_7zSohkt%3DQ1maKupE6hT4dw%40mail.gmail.com.
