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.
