let L be Liouville; :: thesis: L is transcendental
assume L is algebraic ; :: thesis: contradiction
then consider f being INT -valued non-zero Polynomial of F_Complex such that
A1: In (L,F_Complex) is_a_root_of f by Th26;
reconsider g = f as INT -valued non-zero Polynomial of F_Real by Th4, Th13, Th22;
L is irrational Element of F_Real by XREAL_0:def 1;
then ex A being positive Real st
for p being Integer
for q being positive Nat holds |.(L - (p / q)).| > A / (q |^ (len g)) by A1, Th4, Th18, Th28;
hence contradiction by Lm4; :: thesis: verum