Transcendental numbers and the metamath 100.

[Jon P]

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 :)

[savask]

>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?

It would be interesting to hear opinions of people who formalized theorems about transcendental numbers in metamath, but I think the proofs you referenced will be difficult to formalize not because they are proofs by contradiction, but because they implicitly use a lot of background material not present in set.mm.

For example, both proofs use symmetric polynomials and some Galois theory (alg. conjugates in the first proof and embeddings of the field Q(d1, ..., ds) in the second). If I'm not mistaken, we don't even have a theorem proving that algebraic numbers form a ring in set.mm!