Thank you both! Op woensdag 19 april 2023 om 10:11:17 UTC+2 schreef [email protected]:
> 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/23566d12-1d4b-4bb1-94c0-36ad0d307f86n%40googlegroups.com.
