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"
On 4/18/23 19:40, LM 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/7344c693-644d-4eaa-0e31-06065ce25af7%40panix.com.
