On Saturday, July 9, 2022 at 6:41:27 PM UTC+2 Alexander van der Vekens wrote:
> But this is only the expanded form of ~2rp, and looking at proofs using `2 > e. RR` and `0 < 2` (i.e., ~2re and ~2pos), such proofs can be shortened > more elegantly making use of `2 e. RR*`. > Sorry, I mean `2 e. RR+` of course. -- 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/4fa07ac1-f767-4766-bb93-0032515ca138n%40googlegroups.com.
