Is it ok to ask about where things are at re transcendental numbers? I see there is Liouville's approximation theorem:
http://us.metamath.org/mpeuni/aaliou.html And it seems like on the wikipedia page for it there are some other things that can be proven about Liouville numbers, such as them being transcendental, uncountable and there's more examples of them too. Is this something which it is interesting to add? How hard would it be to add these corollaries on? https://en.wikipedia.org/wiki/Liouville_number More than that I notice that two of the remaining 100 theorems, - 53. *π* is Transcendental - 56. The Hermite-Lindemann Transcendence Theorem are connected to this. In the book Transcendental Numbers by M. Ram Murty, Purusottam Rath, Springer. They have relatively simple proofs of both these things relatively early on, how possible would it be to formalise these? Are proofs by contradiction difficult or impossible in metamath, are there any examples to copy? Here are a few images of the pages with the proofs. https://imgur.com/a/hTbtJ8C Though maybe this second proof is different from Hermite-Lindemann? I think it has the same result and H L and W are the people involved so maybe it has two different names? I see others have done some cool work on transcendental numbers already which is really cool so maybe there is some more stuff in the mathboxes etc? Thanks :) -- 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/fa32ad33-554f-4bc7-939b-045edc742cd7n%40googlegroups.com.
