It is really a strange theorem: both sides of the biconditional are wrong ( x=y is wrong, because 0 <_ x and y < 0; and 2x = -2y+1would mean that an even number is equal to an odd number.
Therefore, this theorem can be deprecated and removed later. On Thursday, September 1, 2022 at 6:13:11 PM UTC+2 Benoit wrote: > Good catch. I vote for removing (that is, deprecating) > https://us.metamath.org/mpeuni/znnenlem.html > > Benoît > > > On Thursday, September 1, 2022 at 5:43:32 PM UTC+2 [email protected] > wrote: > >> Should znnenlem be removed from set.mm or moved to a mathbox? It claims >> to be a lemma for znnen, but it's no longer used, and while lines 16 and 28 >> prove moderately interesting things, it then turns A -> B and C -> D into >> (A /\ B) -> (C <-> D). So maybe splittable into three theorems? >> > -- 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/06a5254e-d84f-4b4a-9f22-c9234af86af5n%40googlegroups.com.
