In order to prove a counterexample, I recently wrote a couple of simple theorems, proving that plus infinity and minus infinity are not complex numbers.
Before submitting the PR, a script warned me that I was using ~ df-pnf and ~ df-mnf , for which new use is discouraged. I understand that the theory requires that plus infinity is not a real number, and df-pnf is built in such a way to ensure it ( ~ pnfnre ). But the comment says: " We use ` ~P U. CC ` to make it independent of the construction of ` CC ` , and Cantor's Theorem will show that it is different from any member of ` CC ` and therefore ` RR ` . " And in fact, the proof of ~ pnfnre proves (step 4) that plus infinity is not a complex number. But it looks like we don't have such assertion as a standalone theorem (on purpose, I presume) In conclusion, which of the following three statements holds? 1. the "standard" theory works perfectly fine without assuming plus infinity not being a complex number. Thus, |- -. +oo e. CC should NOT be a theorem in set.mm 2. the "standard" theory assumes that plus infinity is not a complex number and +oo has to be defined so that |- -. +oo e. CC can be "directly" proven from the definition(if this is the case, the discouraged clause should be relaxed and allow for a "direct" proof of |- -. +oo e. CC ) 3. the "standard" theory assumes that plus infinity is not a complex number, but it does not depend on a particular definition of +oo, it can be proven from the standard axiomatization of the extended reals and complex numbers (if this is the case, can anybody reference a textbook proof?) Thanks Glauco p.s. the comment in ~ df-mnf seems to confirm statement 1. , I guess -- 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/4e11a1c1-81ab-46be-baba-ba120471cb0fn%40googlegroups.com.
